使用Frama-C对大型项目做代码切片时遇变量解析错误求助

这些错误源于Frama-C系统库头文件依赖两个未定义的逻辑宏：__FC_MAX_OPEN_FILES和__FC_MAX_OPEN_SOCKETS，它们用于限定跟踪文件描述符、套接字状态的幽灵数组大小，必须显式定义才能通过内核的变量解析检查。

解决方法如下：

• 直接在预处理命令中定义宏
  修改Frama-C命令，在gcc预处理参数里添加两个宏定义，示例如下：

  frama-c -eva -slicing-verbose 8 -no-cpp-frama-c-compliant -cpp-command `gcc -D__FC_MAX_OPEN_FILES=1024 -D__FC_MAX_OPEN_SOCKETS=1024 ...` -kernel-warn-key annot-error=active -slice-calls some_call_in_a_function file.c
  

  其中...替换为你原有gcc命令中的其他参数，数值1024可根据系统实际的文件描述符限制（用ulimit -n查看）调整。

• 通过头文件统一定义
  创建一个头文件（比如frama-c-config.h），写入：

  #define __FC_MAX_OPEN_FILES 1024
  #define __FC_MAX_OPEN_SOCKETS 1024
  

  然后在预处理命令中加入-include frama-c-config.h，或者在待分析的源文件开头添加#include "frama-c-config.h"。

内容的提问来源于stack exchange，提问作者pengwinsurf