我想分析一个大型项目中的文件以使用 Frama-C 创建程序依赖图，但不断收到奇怪的错误，例如：
/usr/include/bits/fcntl-linux.h:305:[kernel] 用户错误：数组长度为零。此扩展程序不受支持
如果我尝试使用 frama-c 提供的 libc 实现，由于缺少 sys/file.h 等头文件，编译会失败。
我正在尝试使用 GCC 版本 4.8.1 分析 Lynx 项目中的文件，特别是 src/WWW/Library/Implementation/HTTP.c 中的文件
我真正需要的是能够为这个源文件生成一个 PDG（它当然有各种依赖项），但我认为如果我可以通过跳过未定义的函数来获得一个有点不完整的图表，那将是一个很好的第一步。
在对 Frama-C 进行预处理时，您需要在 GCC 搜索的路径中任何位置的目录“sys”中提供自己的“file.h”文件。
作为参考，这里是sys/file.h 在另一个系统上的实现。您可能还对有关 sys/file.h的其他 StackOverflow 问题感兴趣。
对于 Frama-C 的价值分析，原型旁边的 assigns 子句有很长的路要走：
/*@ 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 也不是开箱即用的，而且由于在您要分析的代码中使用了这种低级、不那么便携的系统调用，因此必须有人知道。恐怕必须是你。从好的方面来说，您只需要提供您希望分析的代码使用的类型、宏和函数原型。