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

Question

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

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

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

Answer 1

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

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