Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002384Frama-CKernelpublic2018-07-04 09:302018-10-18 10:33
Reporterevdenis 
Assigned Tovalentin.perrelle 
PrioritynormalSeverityminorReproducibilityalways
StatusresolvedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C 17 Chlorine 
Target VersionFixed in VersionFrama-C 18 Argon 
Summary0002384: user error: scalar value (of type int) initialized by compound initializer
DescriptionExample:
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
TagsNo tags attached.
Attached Filesc file icon test.c [^] (101 bytes) 2018-07-04 09:30 [Show Content]
patch file icon restore-initializers.patch [^] (5,453 bytes) 2018-07-06 19:18 [Show Content]

- Relationships

-  Notes
(0006572)
maroneze (developer)
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 (developer)
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 (developer)
2018-10-18 10:33

Fix will be available in the next release

- Issue History
Date Modified Username Field Change
2018-07-04 09:30 evdenis New Issue
2018-07-04 09:30 evdenis File Added: test.c
2018-07-04 16:53 yakobowski Assigned To => maroneze
2018-07-04 16:53 yakobowski Status new => assigned
2018-07-06 19:17 maroneze Note Added: 0006572
2018-07-06 19:17 maroneze Status assigned => confirmed
2018-07-06 19:18 maroneze File Added: restore-initializers.patch
2018-07-06 19:21 maroneze Note Added: 0006573
2018-07-06 19:22 maroneze Product Version Frama-C GIT, precise the release id => Frama-C 17 Chlorine
2018-07-12 14:13 signoles Assigned To maroneze => virgile
2018-07-12 14:13 signoles Assigned To virgile => valentin.perrelle
2018-07-12 14:13 signoles Status confirmed => assigned
2018-10-18 10:33 virgile Note Added: 0006665
2018-10-18 10:33 virgile Status assigned => resolved
2018-10-18 10:33 virgile Fixed in Version => Frama-C 18 Argon
2018-10-18 10:33 virgile Resolution open => fixed


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker