如何使用 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>

启动

有关编写 Frama-C 脚本的更多信息（包括详尽的教程）可在 developer manual.

中找到

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

How to save types of variables to a file using Frama-C

c

static-analysis

frama-c