如何将 frama-c CLI 代码映射到原始的 c 语句?以及如何找到 frama-c 的 api 的文档?

How can I map frama-c CLI code to the original c statement? And how can I find the documentation of the api of the frama-c?

我正在尝试在原始代码的语句级别使用 frama-c 获取程序依赖图 (PDG)。然而,'pdg' frama-c 中的插件在解析代码的节点级别打印 PDG。

由于frama-c-gui可以高亮显示原语句对应于解析代码中的节点,我很确定解析代码中的节点与原始代码语句之间存在映射关系。我怎样才能得到这个映射?原始代码中的行号也可以。

Frama-C 的 GUI 显示代码的两个视图:

  1. CIL 代码(C 中间语言),通常称为规范化源代码,对应于顶部中间面板中 Frama 的 AST 的漂亮打印;
  2. 和原始源代码,在右上面板。

我假设 解析代码 你在谈论 CIL(规范化)代码.

Frama-C的AST中的每个元素都包含一个location,这是一对positions:第一个和最后一个坐标(line, row, column) 在对应于该元素的原始代码中(减去一些例外,例如生成的元素、宏扩展等)。大多数 AST 元素都有检索该位置的方法。

在PDG节点的情况下,你可以获取相关语句(如果有的话)然后打印它们的位置,如下面的代码(运行和frama-c -pdg -load-module print_pdg.ml <file>):

(* print_pdg.ml *)
let () = Db.Main.extend (fun () ->
    Globals.Functions.iter (fun kf ->
        let pdg = !Db.Pdg.get kf in
        !Db.Pdg.iter_nodes (fun n ->
            match PdgTypes.Node.stmt n with
            | None -> ()
            | Some st ->
              Format.printf "%a: %a@."
                Printer.pp_location (Cil_datatype.Stmt.loc st) Printer.pp_stmt st
          ) pdg
      )
  )

请注意,如果有多个 PDG 节点关联到同一语句,我的示例脚本将多次打印每个语句。

默认情况下,Printer.pp_location 仅打印文件名和起始字符所在的行,但您可以制作自定义漂亮打印机以包括该列或最后一个字符的坐标。

API 和插件文档(来自评论中的问题)

一些 Frama-C 插件(Eva、WP、E-ACSL 等)有自己的手册,可在 Frama-C download page.

Pdg插件没有具体的手册,但是一些Ocamldoc生成的HTML页面可以从Frama-C API archive.

获取

然而,大多数 Frama-C 插件开发人员更喜欢在他们最喜欢的编辑器(emacs、vim 等)中使用 OCaml Merlin 插件来导航代码和阅读源注释(例如在 .mli 文件中)。

例如,在 Emacs 上,module/variable 名称上的 C-c C-l 跳转到其定义,C-c C-a.ml.mli 文件之间交替(实施 - 文档)。结合 module/function 发现的自动完成,这提供了一种许多 OCaml 开发人员都喜欢的交互式文档形式。