ratt
ratt

Reputation: 125

Frama-c kernel user error: invalid global initializer tmp?

During frama-c kernel parsing, got "User Eror: invalid global intializer tmp". The source compile fine with gcc. It has something to do with frama-c using 'tmp' variable for conditional operator with memory location. Any idea on how to get around this error without changing the source code? The streamline version of the code is copy below.

If I hard code the conditional expression as in FILL_OK macro then it's okay. If I move lines 8-15 into main() then it's okay.

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

Copy of command line and error output:

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.

Upvotes: 0

Views: 70

Answers (1)

byako
byako

Reputation: 3422

There is currently no way to make this code accepted as is by Frama-C, as the "language" for expressions inside initializers requires each initializer to be a constant. The less invasive code modification that I can find would be to transform flag into a macro.

Upvotes: 1

Related Questions