使用Frama-C做切片时报struct iphdr不存在saddr字段如何解决？

1. 执行命令的cpp-extra-args参数写法错误：多个包含路径之间使用逗号分隔，会导致逗号被识别为路径的一部分，预处理器无法找到正确的头文件目录。
2. Frama-C默认会加载自身携带的精简libc头文件，且默认开启-nostdinc参数禁用系统头文件搜索，即使传入正确的系统头文件路径，也可能出现自带头文件和系统头文件的定义冲突，导致struct iphdr的字段定义不完整，无法识别saddr成员。
3. 预处理默认使用32位x86架构配置，和常见64位系统的头文件结构体布局、字节对齐规则不匹配，也可能导致字段识别错误。

• 调整命令参数写法，删除路径之间的逗号，同时添加-no-frama-c-stdlib参数关闭Frama-C自带libc的加载，优先使用系统头文件：

frama-c iphdr_issue.c -no-frama-c-stdlib -cpp-extra-args="-I/usr/include -I/usr/include/x86_64-linux-gnu/" -kernel-msg-key pp -slice-value addr -then-on 'Slicing export' -print

• 如果当前使用的是64位系统，可额外添加-machdep x86_64参数指定架构匹配，避免结构体布局不兼容：

frama-c iphdr_issue.c -machdep x86_64 -no-frama-c-stdlib -cpp-extra-args="-I/usr/include -I/usr/include/x86_64-linux-gnu/" -kernel-msg-key pp -slice-value addr -then-on 'Slicing export' -print

• 如果修改命令后仍然报错，可以直接在代码中手动补全struct iphdr的标准定义，避免依赖系统头文件的隐式声明：

// 放在现有include语句之后即可
struct iphdr {
#if __BYTE_ORDER__ == __ORDER_LITTLE_ENDIAN__
    uint8_t ihl:4,
            version:4;
#elif __BYTE_ORDER__ == __ORDER_BIG_ENDIAN__
    uint8_t version:4,
            ihl:4;
#endif
    uint8_t tos;
    uint16_t tot_len;
    uint16_t id;
    uint16_t frag_off;
    uint8_t ttl;
    uint8_t protocol;
    uint16_t check;
    uint32_t saddr;
    uint32_t daddr;
};

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