使用Frama-c分析具有CMake构建基础结构的项目

Question

我需要使用frama值分析插件来分析一些项目。这些项目使用CMake构建基础设施作为它们的构建系统。

我用frama-c分别分析了每个文件。这样，有关入口点的信息就会丢失。更准确地说，frama需要一个不包含“主”函数的文件的入口点，因此要覆盖所有函数并从项目中选择单个文件中的最佳入口点是很困难的。

我的问题是，我们是否可以在整个项目上运行frama作为一个整体(而不是逐个文件)？

Answer 1

Frama在其命令行上接受多个文件。如果预处理程序的配置( -cpp-extra-args选项，特别用于包含)的配置与所有文件的配置相同，这将有效。

如果对不同的文件需要不同的预处理设置，则应该单独对每个文件进行预处理(只有cpp，而不是Frama)，并将每个结果保存为一个.i文件。然后，您可以同时向Frama提供所有预处理文件。通常，第一个操作可以通过调整构建过程来完成。