frama-c - 我如何分析像 open62541 这样的复杂项目？

Question

我是一名学生，目前正在尝试使用 cppcheck 和 frama-c 分析 C 中 OPC Ua 协议(protocol)的引用实现。我的目标不是进行非常专门的测试，而是进行更多的一般/基本测试，以查看代码是否存在一些明显的问题。

可以找到项目here

我正在运行带有 Ubuntu 19.10 和 Frama-C 20.0 版 (Calcium) 的虚拟机。

我执行的步骤如下:

git clone https://github.com/open62541/open62541.git
cmake -DCMAKE_EXPORT_COMPILE_COMMANDS=1 /path/to/source
frama-c -json-compilation-database /path/to/compile_commands.json

到目前为止，一切都按预期工作，没有错误。

但是现在我无法理解如何继续。 我是否需要单独对所有文件进行分析，或者是否可以像使用 cppcheck 一样将整个项目放入其中？

一般情况下我会如何处理这个问题？我需要一步步分析所有文件吗？

例如我试过:

frama-c -json-compilation-database /path/to/compilation_commands.json -val /path/to/open62541/src/

返回:

[kernel] Parsing src (with preprocessing)
gcc: warning: /path/to/open62541/src/: linker input file unused because linking not done
[kernel] User Error: cannot find entry point `main'.
  Please use option `-main' for specifying a valid entry point.
[kernel] Frama-C aborted: invalid user input.

显然 frama-c 需要一个入口点，但我不知道我需要指定哪个入口点。

非常感谢任何与此相关的帮助。 我为我的不理解而道歉。这是我的第一个此类项目，我对 frama-c 和 open62541 项目的复杂性有点不知所措。

Answer 1

Do i need to do my analysis on all files separately or is it possible to throw in the whole project like with cppcheck?

Frama-C 实际上可以一次性分析整个项目前提是多个文件没有定义相同的符号。参见 http://blog.frama-c.com/index.php?post/2018/01/25/Analysis-scripts%3A-helping-automate-case-studies ，“设置源和测试解析”段落:

The list of source files to be given to Frama-C can be obtained from the compile_commands.json file. However, it is often the case that the software under analysis contains several binaries, each requiring a different set of sources. The JSON compilation database does not map the sources used to produce each binary, so it is not always possible to entirely automate the process.

您案例中的关键点是 compilation_commands.json指示 Frama-C 如何解析每个文件，但您仍然必须提供您希望自己解析的文件。使用您当前的命令行，Frama-C 会尝试解释 /path/to/open62541/src/作为一个文件(并且失败)，并且没有其他文件可以解析。这就是您收到错误 User Error: cannot find entry point 'main' 的原因.

因此，您必须在命令行中指定要解析的文件。这可以通过两种方式完成:

• 手动提取 compilation_commands.json 中引用的文件
• 自动使用frama-c-script助手，描述于 http://blog.frama-c.com/index.php?post/2019/01/16/Setting-up-an-analysis-with-the-help-of-frama-c-script

我使用了第一种方法，但我建议您使用第二种方法，如frama-c-script对开始第一次分析非常有帮助。

一旦完成了这个listing步骤，你至少还会遇到三个问题:

• Frama-C 会窒息 # include <sys/param.h> ，因为此文件不存在于与 Frama-C 捆绑在一起的标准 C 库中。要么删除源文件中的这个包含，要么添加一个空的 sys/param.h某处
• 一些.c文件引用生成的 header ，这些 header 不存在于 open62541 的 git 存储库中.因此，在启动 Frama-C 之前，您需要编译 repo 以获取这些 header 。
• Frama-C 也会在定义宏UA_STATIC_ASSERT 时卡住。在architecture_definitions.h .我没有调查其中一个定义是否被接受，我只是将它定义为空宏。

完成所有这些之后，您应该可以开始了。