Frama-c kernel user error: invalid global initializer 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 接受此代码，因为 "language" 用于初始化器内部表达式的 "language" 要求每个初始化器都是常量。我能找到的侵入性较小的代码修改是将 flag 转换为宏。