Frama-C Bug Tracking System - Frama-C
View Issue Details
0002145Frama-CPlug-in > wppublic2015-07-15 17:102015-07-17 17:33
Ian 
correnson 
normalminoralways
assignedopen 
Ubuntu
Frama-C Sodium 
 
0002145: Error when struct has no members
WP produces an invalid ergo file when there is a struct which contains no members. The failure was present using alt-ergo, why3:alt-ergo, and why3:z3-4.4.0
Create empty_struct.c: struct a{}; void foo() { struct a i,j; //@ assert i == j; } run: > frama-c empty_struct.c -wp -wp-out struct_out [kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing) [kernel] Parsing empty_struct.c (with preprocessing) [wp] Running WP plugin... [wp] Collecting axiomatic usage [wp] warning: Missing RTE guards [wp] 1 goal scheduled struct_out/typed/S_a.ergo:5:[wp] user error: Alt-Ergo error: characters 14-15:syntax error [wp] [Alt-Ergo] Goal typed_foo_assert : Failed Error: characters 14-15:syntax error [wp] Proved goals: 0 / 1 Alt-Ergo: 0 (failed: 1) > frama-c empty_struct.c -wp -wp-out struct_out -wp-prover why3:alt-ergo [kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing) [kernel] Parsing empty_struct.c (with preprocessing) [wp] Running WP plugin... [wp] Collecting axiomatic usage [wp] warning: Missing RTE guards [wp] 1 goal scheduled ------------------------------------------------------------ --- Why3 (stderr) : ------------------------------------------------------------ [Config] reading extra configuration file /usr/local/share/frama-c/wp/why3/why3.conf /usr/local/lib/why3/plugins/hypothesis_selection can't be loaded : Dynlink error : cannot find file /usr/local/lib/why3/plugins/hypothesis_selection.cmxs in search path File "struct_out/typed/S_a.why", line 13, characters 13-14: syntax error ------------------------------------------------------------ [wp] [alt-ergo] Goal typed_foo_assert : Failed Error: Why3 exits with status [1] [wp] Proved goals: 0 / 1 alt-ergo: 0 (failed: 1) > frama-c empty_struct.c -wp -wp-out struct_out -wp-prover why3:z3-4.4.0 [kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing) [kernel] Parsing empty_struct.c (with preprocessing) [wp] Running WP plugin... [wp] Collecting axiomatic usage [wp] warning: Missing RTE guards [wp] 1 goal scheduled ------------------------------------------------------------ --- Why3 (stderr) : ------------------------------------------------------------ [Config] reading extra configuration file /usr/local/share/frama-c/wp/why3/why3.conf /usr/local/lib/why3/plugins/hypothesis_selection can't be loaded : Dynlink error : cannot find file /usr/local/lib/why3/plugins/hypothesis_selection.cmxs in search path File "struct_out/typed/S_a.why", line 13, characters 13-14: syntax error ------------------------------------------------------------ [wp] [z3-4.4.0] Goal typed_foo_assert : Failed Error: Why3 exits with status [1] [wp] Proved goals: 0 / 1 z3-4.4.0: 0 (failed: 1)
No tags attached.
c empty_struct.c (70) 2015-07-15 17:10
https://bts.frama-c.com/file_download.php?file_id=1049&type=bug
? S_a.ergo (252) 2015-07-15 17:10
https://bts.frama-c.com/file_download.php?file_id=1050&type=bug
? S_a.why (439) 2015-07-15 17:10
https://bts.frama-c.com/file_download.php?file_id=1051&type=bug
Issue History
2015-07-15 17:10IanNew Issue
2015-07-15 17:10IanStatusnew => assigned
2015-07-15 17:10IanAssigned To => correnson
2015-07-15 17:10IanFile Added: empty_struct.c
2015-07-15 17:10IanFile Added: S_a.ergo
2015-07-15 17:10IanFile Added: S_a.why
2015-07-16 14:59yakobowskiNote Added: 0005978
2015-07-16 15:15IanNote Added: 0005979
2015-07-17 17:33yakobowskiNote Added: 0005986

Notes
(0005978)
yakobowski   
2015-07-16 14:59   
Empty struct are actually invalid in C. Furthermore, the == ACSL operators on aggregates is not very well-defined, so it is not even certain that the assertion holds.
(0005979)
Ian   
2015-07-16 15:15   
Since an empty struct is not allowed in C, should the Frama-c kernel not accept the program?
(0005986)
yakobowski   
2015-07-17 17:33   
Indeed... One reason we still parse them is that they are accepted by major compilers such as GCC, and are used in e.g. the Linux kernel. This works as they are used only in parts of the software that won't be analyzed