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

Question

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

该项目可以在这里找到

我正在使用 Ubuntu 19.10 和 Frama-C 版本 20.0 (Calcium) 运行 VM。

我执行的步骤如下：

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

我是否需要单独对所有文件进行分析，还是可以像使用 cppcheck 一样投入整个项目？

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

要提供给 Frama-C 的源文件列表可以从 compile_commands.json 文件中获得。但是，通常情况下，被分析的软件包含多个二进制文件，每个文件都需要一组不同的源。JSON 编译数据库不会映射用于生成每个二进制文件的源，因此并不总是可以完全自动化该过程。

您的情况的关键点是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-脚本

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

完成此列表步骤后，您至少会遇到三个问题：

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

做完这一切，你应该可以走了。