Frama-c内核用户错误：无效的全局初始化程序tmp？

Question

在frama-c内核解析期间，得到“User Eror：invalid global intializer 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.

Answer 1

目前没有办法使这个代码被Frama-C接受，因为初始化器中表达式的“语言”要求每个初始化器都是常量。我能找到的侵入性较小的代码修改方法是将flag转换为宏。