slicing: Cannot find field saddr in type struct iphdr

Question

I am trying to create a slice for variable addr from this sample program:

#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;
}

Here is the command I have used to print the slice in the terminal:

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

It is generating following output with the mentioned error:

[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.

How can I solve this issue?

Answer 1

If you want to use your system's standard headers instead of Frama-C's ones (beware however that there's absolutely no guarantee that Frama-C will be able to parse them, especially the ones that are heavily architecture-dependent), the solution is not to use -cpp-extra-args, but -no-frama-c-stdlib, as in:

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

Incidentally, the example you provided gives an empty slice:

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

because Eva complains that you are trying from the uninitialized location ihdr->saddr (presumably because the example is correctly reduced to highlight the parsing error, but a bit too small for slicing to be meaningful).