如何获得从Frama-c的解析语句到原始c语句的映射？

Question

我正在尝试在原始代码的语句级别使用frama-c获取程序依赖图（PDG）。但是，frama-c中的'pdg'插件会在已解析代码的节点级别上打印PDG。

由于frama-c-gui可以突出显示原始语句对应于已解析代码中的节点，因此，我很确定在解析代码中的节点与原始代码的语句之间存在映射。如何获得此映射？只需原始代码中的行号也可以。

Answer 1

CIL代码（C中间语言），通常称为

规范化的源代码，它对应于顶部中间面板中的Frama AST的精美印刷；
1. 以及原始源代码，在右上方的面板上。

我假设通过[[解析的代码您正在谈论

CIL（规范化）代码。

Frama-C AST中的每个元素都包含一个位置，它是一对位置：原始代码中的第一个和最后一个坐标

（行，行，列）”到该元素（减去一些例外，例如生成的元素，宏扩展等）。大多数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插件没有特定的手册，但是可以从Frama-C API archive获得一些Ocamldoc生成的HTML页面。
但是，大多数Frama-C插件开发人员更喜欢在他们喜欢的编辑器（emacs，vim等）中使用OCaml Merlin插件来浏览代码并阅读源注释（在.mli中。文件）。
例如，在Emacs上，模块/变量名称上的C-c C-l跳到其定义，C-c C-a在.ml和.mli文件之间交替（实现-文档）。结合用于模块/功能发现的自动完成功能，这提供了许多OCaml开发人员都喜欢的交互式文档形式。