如何使用frama-c命令处理printf(& quot;和)和scanf(& amp;")?

如何使用frama-c命令处理printf(& quot;和)和scanf(& amp;")?

问题描述:

我正在使用此代码生成C程序的控制流程图.对于除 printf scanf 之类的内置功能以外的所有功能,它都可以正常工作.我可以在此代码中进行哪些更改以按原样输出内置函数?

I am using this code to generate the control flow graph of a C program. It is working fine for all the function except built-in function like printf and scanf. What can I change in this code to output the built in function as it is?

open Cil
open Cil_types
let print_stmt out =
function
| Instr i -> !Ast_printer.d_instr out i
| Return _ -> Format.pp_print_string out "<return>"
| Goto _ -> Format.pp_print_string out "<goto>"
| Break _ -> Format.pp_print_string out "<break>"
| Continue _ -> Format.pp_print_string out "<continue>"
| If (e,_,_,_) -> Format.fprintf out "if %a" !Ast_printer.d_exp e
| Switch(e,_,_,_) -> Format.fprintf out "switch %a" !Ast_printer.d_exp e
| Loop _ -> Format.fprintf out "<loop>"
| Block _ -> Format.fprintf out "<enter block>"
| UnspecifiedSequence _ -> Format.fprintf out "<enter unspecified sequence>"
| TryFinally _ | TryExcept _ -> Format.fprintf out "<try>"

class print_cfg out =
object
inherit Visitor.frama_c_inplace

method vstmt_aux s =
Format.fprintf out "s%d@[[label=\"%a\"]@];@\n" s.sid print_stmt s.skind;
List.iter 
  (fun succ -> Format.fprintf out "s%d -> s%d;@\n" s.sid succ.sid)
  s.succs;
DoChildren
method vglob_aux g =
match g with
  | GFun(f,loc) ->
      Format.fprintf out "@[<hov 2>subgraph cluster_%a {@\n\
                         graph [label=\"%a\"];@\n" 
        Cil_datatype.Varinfo.pretty f.svar
        Cil_datatype.Varinfo.pretty f.svar;
      ChangeDoChildrenPost([g], fun g -> Format.fprintf out "}@\n@]"; g)
  | _ -> SkipChildren

 method vfile f =
 Format.fprintf out "@[<hov 2>digraph cfg {@\n";
 ChangeDoChildrenPost (f,fun f -> Format.fprintf out "}@."; f)
 end

 let run () =
 let chan = open_out "cfg.out" in
 let fmt = Format.formatter_of_out_channel chan in
 Visitor.visitFramacFileSameGlobals (new print_cfg fmt) (Ast.get())

 let () = Db.Main.extend run

该问题本身与可变参数函数无关,而与文字字符串有关.您必须引用它们,否则 dot 会认为标签已结束.尝试更换

The problem is not related to variadic functions per se, but instead to literal strings. You must quote them, as otherwise dot thinks the label has ended. Try replacing

Format.fprintf out "s%d@[[label=\"%a\"]@];@\n" s.sid print_stmt s.skind;

作者

Format.fprintf out "s%d@[[label=%S]@];@\n" s.sid (Pretty_utils.to_string print_stmt s.skind);

(请注意%S ,它会输出带引号的字符串.)

(Notice the %S, that outputs a quoted string.)