如何使用Frama-C将变量类型保存到文件中

Question

我正在尝试使用Frama-C在C程序中打印变量类型。我发现该信息在GUI中表示，如下图所示。但是，我找不到将这些信息输出到文件的方法。您能否建议我用Frama-c执行此任务的方法？

Answer 1

没有从命令行直接解决。但是，可以使用简单的脚本（例如（未经测试）

）轻松完成此操作

let print_type () =
  Ast.compute();
  Globals.Vars.iter
   (fun v _ ->
     Format.printf "Variable %a: %a@."
     Cil_datatype.Varinfo.pretty v
     Cil_datatype.Typ.pretty v.vtype)

let () = Db.Main.extend print_type

可以用frama-c -load-script <my_script.ml> <other args including source files>启动

developer manual中提供了有关脚本Frama-C的更多信息（包括广泛的教程）。>