slicing:在类型struct iphdr中找不到字段

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

如果你想使用你的系统的标准头而不是Frama-C的头(小心)然而，绝对不能保证Frama-C将能够解析它们，特别是那些严重依赖于架构的)，解决方案是不使用-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(可能是因为示例被正确地减少以突出解析错误，但对于切片来说有点太小而没有意义)。