切片：在 struct iphdr 类型中找不到字段 saddr

Question

我正在尝试从这个示例程序中为变量 addr 创建一个切片：

#include <stdio.h>
#include <stdlib.h>
#include <net/ethernet.h>
#include <netinet/ip.h>

#define PKT_LEN 8192

int main (int argc, char *argv[]) {
    char *pkt = (char *)malloc(PKT_LEN);
    uint32_t addr;
    int unrelated_var;

    struct ethhdr *ehdr = (struct ethhdr *)pkt;
    struct iphdr *ihdr = (struct iphdr *)(pkt + sizeof(struct ethhdr));

    addr = ihdr->saddr;

    return 0;
}

这是我用来在终端中打印切片的命令：

frama-c iphdr_issue.c -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

它正在生成以下带有上述错误的输出：

[kernel:pp]
  preprocessing with "gcc -E -C -I.  -I/users/ashfaqur/.opam/system/share/frama-c/libc -D__FRAMAC__ -D__FC_MACHDEP_X86_32 -I/usr/include -I/usr/include/x86_64-linux-gnu/ -dD -nostdinc -m32 iphdr_issue.c"
[kernel] Parsing iphdr_issue.c (with preprocessing)
[kernel] iphdr_issue.c:16: User Error:
  Cannot find field saddr in type struct iphdr
  14        struct iphdr *ihdr = (struct iphdr *)(pkt + sizeof(struct ethhdr));
  15
  16        addr = ihdr->saddr;
        ^^^^^^^^^^^^^^^^^^^^^^^
  17
  18        return 0;
[kernel] User Error: stopping on file "iphdr_issue.c" that has errors.
[kernel] Frama-C aborted: invalid user input.

我该如何解决这个问题？

Answer 1

如果您想使用系统的标准 headers 而不是 Frama-C 的（注意但是绝对不能保证 Frama-C 将能够解析它们，尤其是那些重 architecture-dependent) 的，解决方案不是使用 -cpp-extra-args，而是 -no-frama-c-stdlib，如：

frama-c iphdr_issue.c -no-frama-c-stdlib -slice-value addr test.c -then-on "Slicing export" -print

顺便说一句，您提供的示例给出了一个空切片：

/* Generated by Frama-C */
void main(void)
{
  return;
}

因为 Eva 抱怨你正在从未初始化的位置尝试 ihdr->saddr（大概是因为示例被正确地减少以突出解析错误，但对于切片来说有点太小了没有意义）。

切片：在 struct iphdr 类型中找不到字段 saddr

slicing: Cannot find field saddr in type struct iphdr

frama-c