CODEWITHSUNDEEP
frama-c
MEE
MEE

Reputation: 2412

Frama-c syntax error on macro expansion

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?

Upvotes: 2

Views: 189

Answers (1)

MEE
MEE

Reputation: 2412

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

Upvotes: 3

Related Questions