GitLab

ID0002384: This issue was created automatically from Mantis Issue 2384. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0002384	Frama-C	Kernel	public	2018-07-04	2018-11-30

Reporter	evdenis	Assigned To	valentin.perrelle	Resolution	fixed
Priority	normal	Severity	minor	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C 17-Chlorine	Target Version	-	Fixed in Version	Frama-C 18-Argon

Description :

Example:

struct test {
   union {
      int a;
      long b;
   };
};

static struct test t = { { .a = 0 } };

Run:

$ gcc -c test.c
$ echo $?
0
$ frama-c test.c

Error Log:

[kernel] Parsing test.c (with preprocessing)
[kernel] test.c:1: Warning:
  unnamed fields are a C11 extension (use -c11 to avoid this warning)
[kernel] test.c:8: User Error:
  scalar value (of type int) initialized by compound initializer
  6     };
  7
  8     static struct test t = { { .a = 0 } };
        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
[kernel] User Error: stopping on file "test.c" that has errors. Add '-kernel-msg-key pp'
  for preprocessing command.
[kernel] Frama-C aborted: invalid user input.

Frama-C Version:

$ frama-c -version
Chlorine-20180501

Attachments

• test.c
• restore-initializers.patch