Ошибка пользователя ядра Frama-c: неверный глобальный инициализатор tmp? - PullRequest
Новая
       28

Ошибка пользователя ядра Frama-c: неверный глобальный инициализатор tmp?

0 голосов
/ 22 декабря 2018

Во время синтаксического анализа ядра frama-c получено сообщение «Ошибка пользователя: недопустимый глобальный инициализатор tmp».Исходный код прекрасно компилируется с помощью gcc.Это как-то связано с frama-c, использующим переменную 'tmp' для условного оператора с расположением в памяти.Любая идея о том, как обойти эту ошибку без изменения исходного кода?Ниже приведена упрощенная версия кода.

Если я жестко закодирую условное выражение, как в макросе FILL_OK, тогда все в порядке.Если я перенесу строки 8-15 в main (), тогда все будет в порядке. 

#define FILL_OK() {.a = 0 == 0 ? 0 : 1 }
#define FILL_NOK() {.a = 0 == flag ? 0 : 1 }

typedef struct {
     int a;
} a_st;

int flag = 0;

a_st buff_b[] =
{
    FILL_OK(),
    FILL_NOK(),
};

int main()
{
    return(0);
}

Копирование командной строки и вывод ошибок: 

frama-c -val main0.c

[kernel] Parsing main0.c (with preprocessing)
[kernel] main0.c:10: User Error: 
  invalid global initializer tmp

                             {/*()  <- flag
                              Calls:

                              */

                              if (0 == flag) 
                                tmp = 0;
                              else 
                                tmp = 1;}
[kernel] User Error: stopping on file "main0.c" that has errors. Add '-kernel-msg-key pp'
  for preprocessing command.
[kernel] Frama-C aborted: invalid user input.

1 Ответ

0 голосов
/ 24 декабря 2018

В настоящее время нет способа сделать этот код принятым как есть Frama-C, так как «язык» для выражений внутри инициализаторов требует, чтобы каждый инициализатор был константой.Менее инвазивная модификация кода, которую я могу найти, состоит в преобразовании flag в макрос.

...