小编Luk*_*kas的帖子

我是一名学生，目前正在尝试使用 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] …