完整文件的Frama-C图形

Question

我一直在试图使用pdg-dot插件来帮助创建我的软件的一个很好的图形。问题是不同的文件没有主要，所以Frama-C抱怨。当我使用-main标记并指定一个函数来启动它时，它只会为该函数及其内部的任何内容创建一个.dot文件。有没有办法让我有一个.c文件的.dot文件？

Answer 1

我不这么认为。每个生成的PDG仅代表一个功能。但是，您可以获取从入口点（主）可到达的所有功能的PDG。