Ошибка синтаксиса Frama-c при раскрытии макроса

Я получаю следующую синтаксическую ошибку:

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

Это в gnu stat-time.h Пола Эггерта. Вот фрагмент, вызывающий ошибку:

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

Я попытался сначала предварительно обработать файл, а затем запустить frama-c для предварительно обработанного файла, но это не помогло. Frama-c по-прежнему сообщал о той же ошибке в том же месте, даже несмотря на то, что файл был правильно предварительно обработан и макрос был правильно развернут! Я вызвал gcc для предварительной обработки следующим образом:

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

Любые идеи?


frama-c
person MEE    schedule 14.05.2015    source источник

Ответы (1)


arrow_upward
3
arrow_downward

Я нашел решение. Очевидно, в заголовках frama-c в /usr/local/share/frama-c/libc/__fc_define_stat.h не хватало nsec полей детализации в struct stat. Я добавил следующие поля в struct stat, чтобы устранить проблему:


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

Также не забудьте использовать заголовки frama-c при настройке, например, configure CPP='gcc -E -C -dD -nostdinc -I/usr/local/share/frama-c/libc. В противном случае вам потребуется отменить определение следующих двух макросов: HAVE_STRUCT_STAT_ST_ATIM_TV_NSEC, HAVE_STRUCT_STAT_ST_ATIMESPEC_TV_NSEC и определить следующий макрос: HAVE_STRUCT_STAT_ST_ATIMENSEC в файле заголовка и включить его в config.h или в __fc_define_stat.h

person MEE    schedule 14.05.2015