frama-c - 数据流图

Question

是否有一个 frama-c 插件来输出过程间数据流/指向图？

我知道切片器插件中的 -pdg 将包​​含此信息，但想知道我是否可以单独获取它。

Answer 1

PDG 不是切片插件的一部分，如果您愿意，可以单独使用它。看 ：

$ frama-c -pdg-help

（简短）选项列表，以及 Db.Pdg 模块（在 src/kernel/db.mli 中）中的 API，以便在您自己的程序中使用它。