Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002145Frama-CPlug-in > wppublic2015-07-15 17:102015-07-17 17:33
ReporterIan 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSUbuntuOS Version
Product VersionFrama-C Sodium 
Target VersionFixed in Version 
Summary0002145: Error when struct has no members
DescriptionWP 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 ReproduceCreate 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)
TagsNo tags attached.
Attached Filesc file icon empty_struct.c [^] (70 bytes) 2015-07-15 17:10 [Show Content]
? file icon S_a.ergo [^] (252 bytes) 2015-07-15 17:10
? file icon S_a.why [^] (439 bytes) 2015-07-15 17:10

- Relationships

-  Notes
(0005978)
yakobowski (manager)
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 (reporter)
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 (manager)
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

- Issue History
Date Modified Username Field Change
2015-07-15 17:10 Ian New Issue
2015-07-15 17:10 Ian Status new => assigned
2015-07-15 17:10 Ian Assigned To => correnson
2015-07-15 17:10 Ian File Added: empty_struct.c
2015-07-15 17:10 Ian File Added: S_a.ergo
2015-07-15 17:10 Ian File Added: S_a.why
2015-07-16 14:59 yakobowski Note Added: 0005978
2015-07-16 15:15 Ian Note Added: 0005979
2015-07-17 17:33 yakobowski Note Added: 0005986


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker