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

Question

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

这个项目可以找到这里

我使用Ubuntu19.10和Frama版本20.0 (钙)运行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非常需要一个入口点，但是我不知道需要指定哪个入口点。

在这方面的任何帮助都是非常感谢的。我为我缺乏理解而道歉。这是我的第一个这样的项目，我有点被frama和open62541项目的复杂性所淹没。

Answer 1

我是否需要对所有文件分别进行分析，还是可以像cppcheck那样提交整个项目？

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

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

在您的情况下，关键是compilation_commands.json指示Frama如何解析每个文件，但是您仍然必须提供您希望自己解析的文件。使用当前的命令行，Frama尝试将/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对于开始第一种分析非常有帮助。

完成这个清单步骤之后，您将至少会遇到三个问题：

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

在这一切之后，你该走了。