frama-c - 使用 Frama-C 分析大型项目

Question

我想分析一个大型项目的文件以使用 Frama-C 创建程序依赖图，但不断出现奇怪的错误，例如:

/usr/include/bits/fcntl-linux.h:305:[kernel] user error: Length of array is zero. This extension is unsupported

如果我尝试使用 frama-c 提供的 libc 实现，编译会因缺少头文件(例如 sys/file.h)而失败。

我正在尝试使用 GCC 4.8.1 版分析 Lynx 项目中的文件，特别是 src/WWW/Library/Implementation/HTTP.c 中的文件

我真正需要的是能够为这个源文件(当然有各种依赖关系)生成一个 PDG，但我认为如果我可以通过跳过未定义的函数来获得甚至有点不完整的图，那将是一个很好的选择第一步。

Answer 1

在预处理 Frama-C 时，您需要在 GCC 搜索路径中的任何位置的目录“sys”中提供您自己的“file.h”文件。

作为引用，这里是 sys/file.h on another system 的实现.您可能还对 this other StackOverflow question 感兴趣关于 sys/file.h.

对于 Frama-C 的值(value)分析，与原型(prototype)一起分配子句大有帮助:

/*@ assigns *f \from ui, s, *fo; */
void finit(struct file *f, u_int ui, short s, void *p, struct fileops *fo);

请注意，我不知道 finit() 的功能是什么，也不知道上面的 assigns 子句是否正确。事实上，这就是重点:Frama-C 也不是开箱即用的，并且由于在您希望分析的代码中使用了这个低级、可移植性差的系统调用，所以必须有人知道。恐怕必须是你。从好的方面来说，您只需提供您希望分析的代码使用的类型、宏和函数原型(prototype)。