Error when struct has no members
ID0002145: This issue was created automatically from Mantis Issue 2145. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002145 | Frama-C | Plug-in > wp | public | 2015-07-15 | 2015-07-17 |
| Reporter | Ian | Assigned To | correnson | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | Ubuntu | OS Version | - |
| Product Version | Frama-C Sodium | Target Version | - | Fixed in Version | - |
Description :
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
Steps To Reproduce :
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)