Frama-C Bug Tracking System - Frama-C
View Issue Details
0002384Frama-CKernelpublic2018-07-04 09:302018-11-30 10:07
evdenis 
valentin.perrelle 
normalminoralways
closedfixed 
Frama-C 17-Chlorine 
Frama-C 18-Argon 
0002384: user error: scalar value (of type int) initialized by compound initializer
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
No tags attached.
c test.c (101) 2018-07-04 09:30
https://bts.frama-c.com/file_download.php?file_id=1269&type=bug
patch restore-initializers.patch (5,453) 2018-07-06 19:18
https://bts.frama-c.com/file_download.php?file_id=1272&type=bug
Issue History
2018-07-04 09:30evdenisNew Issue
2018-07-04 09:30evdenisFile Added: test.c
2018-07-04 16:53yakobowskiAssigned To => maroneze
2018-07-04 16:53yakobowskiStatusnew => assigned
2018-07-06 19:17maronezeNote Added: 0006572
2018-07-06 19:17maronezeStatusassigned => confirmed
2018-07-06 19:18maronezeFile Added: restore-initializers.patch
2018-07-06 19:21maronezeNote Added: 0006573
2018-07-06 19:22maronezeProduct VersionFrama-C GIT, precise the release id => Frama-C 17-Chlorine
2018-07-12 14:13signolesAssigned Tomaroneze => virgile
2018-07-12 14:13signolesAssigned Tovirgile => valentin.perrelle
2018-07-12 14:13signolesStatusconfirmed => assigned
2018-10-18 10:33virgileNote Added: 0006665
2018-10-18 10:33virgileStatusassigned => resolved
2018-10-18 10:33virgileFixed in Version => Frama-C 18-Argon
2018-10-18 10:33virgileResolutionopen => fixed
2018-11-30 10:07signolesStatusresolved => closed

Notes
(0006572)
maroneze   
2018-07-06 19:17   
Thank you for the report. Indeed this is a regression w.r.t. Frama-C 16 and it must be fixed.

In the meanwhile, reverting to the previous Frama-C version might help. I'll upload a patch that should be applicable to Frama-C 17, in case it might be useful.
(0006573)
maroneze   
2018-07-06 19:21   
The attached 'restore-initializers.patch' should hopefully allow parsing to behave as before, at least for this example. I didn't test it extensively though, so it's possible that it will not restore it in all cases.
(0006665)
virgile   
2018-10-18 10:33   
Fix will be available in the next release