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

【问题标题】：Use Frama-c to analyze a project with CMake build infrastructure使用 Frama-c 分析具有 CMake 构建基础架构的项目
【发布时间】：2016-02-17 07:27:27
【问题描述】：

我需要使用frama-c价值分析插件来分析一些项目。这些项目使用 CMake 构建基础架构作为构建系统。

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

我的问题是，有没有一种方法可以将整个项目作为一个整体（不是逐个文件）运行 frama-c？

【问题讨论】：

【解决方案1】：

Frama-C 在其命令行上接受多个文件。如果预处理器的配置（选项-cpp-extra-args，特别用于包含）在所有文件中都是相同的，这将起作用。

如果您需要为不同的文件设置不同的预处理器，您应该单独预处理每个文件（仅cpp，没有 Frama-C），并将每个结果保存为 .i 文件。然后，您可以同时将所有这些预处理文件提供给 Frama-C。通常，第一个操作可以通过调整构建过程来完成。

【讨论】：

感谢您的出色解决方案，它成功了！我只是有一个关于保存预处理文件的问题。当我使用命令“frama-c -cpp-command 'gcc -C -E -I. -o %2 %1' small.c small.i”时，frama-c 抱怨 small.i 不存在并认为它作为另一个输入，而不是输出文件名！现在，我能够使用 -print 选项获得预处理结果，但它也会打印一些额外的内核消息，这是不可取的。您对保存 .i 文件有什么建议？谢谢！ @byako
@MehrnooshEP 您不必在此设置中提供中间 .i 文件的名称，frama-c 会自行处理。只有当您选择在 frama-c 之外预处理 C 文件时，您才需要保存 .i 文件并将其作为 Frama-C 的输入。换句话说，您可以使用frama-c -cpp-command bla file.c 或cpp -o file.i file.c && frama-c file.i，但不能 frama-c -cpp-command bla file.c file.i
@Virgile 我明白了，我把两者混在一起了！谢谢你的解释。