如何使用 frama-c 命令处理 printf(" ", ) 和 scanf(" ") ？

我正在使用此代码生成 C 程序的控制流图。除了内置函数之外，它对所有函数都运行良好printf and scanf。我可以在此代码中更改什么来按原样输出内置函数？

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认为标签已经结束。尝试更换

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

by

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

（注意%S，输出带引号的字符串。）