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

Question

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

可以找到项目here

我是运行具有 Ubuntu 19.10 和 Frama-C 20.0 版（钙）的虚拟机。

我执行的步骤如下：

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/

哪个returns:

[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，第 "Setting sources and testing parsing" 段：

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 如何解析每个文件，但你仍然必须提供你想要自己解析的文件。对于当前的 command-line，Frama-C 尝试将 /path/to/open62541/src/ 解释为文件（但失败），并且没有其他文件可解析。这就是您收到错误 User Error: cannot find entry point 'main'.

的原因

因此，您必须在 command-line 上指定要解析的文件。这可以通过两种方式完成：

手动，通过提取 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 对开始第一个分析非常有帮助。

完成这个上市步骤后，您至少还会遇到三个问题：

Frama-C 将在 # include <sys/param.h> 上阻塞，因为此文件不存在于与 Frama-C 捆绑在一起的标准 C 库中。要么在源文件中删除这个包含，要么在某处添加一个空的 sys/param.h
一些 .c 文件引用了生成的 headers，它们不存在于 open62541 的 git 存储库中。因此，在启动 Frama-C.

编译

Frama-C 也会在 architecture_definitions.h 中定义宏 UA_STATIC_ASSERT 时阻塞。我没有调查其中一个定义是否被接受，我只是将其定义为空宏。

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

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

How do i analyse a complex project like open62541?

frama-c