时间戳

首页 > 解决方案 > 如何使用 Frama-C 将变量类型保存到文件中

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

问题描述

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

标签： cstatic-analysisframa-c

解决方案

命令行没有直接的解决方案。然而，这可以很容易地用一个简单的脚本来完成，比如（未测试）

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 脚本的更多信息（包括详尽的教程）。

推荐阅读