Frama-c syntax error on macro expansion

Question

I am getting the following syntax error:

../stat-time.h:58:[kernel] user error: Cannot find field st_atim

This is in the gnu stat-time.h by Paul Eggert. Here's the snippet causing the error:

#define STAT_TIMESPEC(st, st_xtim) ((st)->st_xtim)

long int get_stat_atime_ns(struct stat const *st) {
  ...
  // 58:
  return STAT_TIMESPEC(st, st_atim).tv_nsec;
  ...
}

I tried to preprocess the file first, then run frama-c on the preprocessed file, but that didn't help. Frama-c still reported the same error at the same location, even though the file was preprocessed correctly and the macro was correctly expanded! I invoked gcc as follows, for preprocessing:

gcc -E -C -I. -dD -nostdinc -D__FC_MACHDEP_X86_32 -I/usr/local/share/frama-c/libc

Any ideas?

MEE MEE · Accepted Answer · 2015-05-14T17:42:19

I figured out the solution. Apparently, the frama-c headers in /usr/local/share/frama-c/libc/__fc_define_stat.h lacked the nsec granularity fields in struct stat. I added the following fields to struct stat to fix the problem:


    unsigned long int st_atimensec;
    unsigned long int st_mtimensec;
    unsigned long int st_ctimensec;

Also, make sure to use the frama-c headers while configuring, e.g., configure CPP='gcc -E -C -dD -nostdinc -I/usr/local/share/frama-c/libc. If not, you will need to undefine the following two macros: HAVE_STRUCT_STAT_ST_ATIM_TV_NSEC, HAVE_STRUCT_STAT_ST_ATIMESPEC_TV_NSEC, and define the following macro: HAVE_STRUCT_STAT_ST_ATIMENSEC in a header file, and include it in config.h or in __fc_define_stat.h

Frama-c syntax error on macro expansion

1 Answers