Frama-c生成图形对象而不是点文件

Question

我试图找出两个程序是否伽马同构或不是，我正在使用Jgrapht库的帮助。现在，我必须生成程序的程序依赖图，并将其捕获为图形对象。使用frama-c，我们可以生成pdg。我用frama-c -pdg -pdg-dot graph -pdg-print program.c生成程序的pdg，输出是点格式的。我必须解析点格式才能得到图形。作为替代，我将能够像图形对象而不是点文件那样获得图形数据结构。

Answer 1

从技术上讲，您应该能够使用Frama-C的Db.Pdg模块中导出的函数来提取所需的信息。特别是，Db.Pdg.iter_nodes允许您对由Pdg生成的所有节点(针对所有函数)执行iter，并且Db.Pdg.direct_*dpds系列函数将为您提供给定节点的直接子节点的列表，可以是所有节点，也可以是给定类型的节点。Frama-C源代码中的db.mli文件中提供了更多信息。

也就是说，我不得不问你为什么要这么做。就我的搜索引擎所能告诉我的，JGraphT是一个Java库，我最后一次检查，OCaml/Java绑定的实现并不是很容易实现，如果可能的话。此外，在我看来，JGraphT的DOTImporter类应该允许您或多或少地直接使用pdg的输出。