Frama-C Bug Tracking System - Frama-C
View Issue Details
0000662Frama-CPlug-in > wppublic2011-01-07 16:232011-04-13 15:28
sduprat 
dargaye 
normalminoralways
closedfixed 
Frama-C Carbon-20101202-beta2 
Frama-C Carbon-20110201Frama-C Carbon-20110201 
0000662: warning: Degenerated goal
warning degenerated goal is raised with this source example containing unions. ensures are unproved.
frama-c -wp -pp-annot -wp-model Store -wp-proof alt-ergo -wp-split *.c [wp] warning: Degenerated goal store_f1_post_5_P1 (1 warning) [wp] warning: Degenerated goal store_f1_post_6_P2 (2 warnings) [wp] warning: Degenerated goal store_f1_post_7_P3 (3 warnings) [wp] [Alt-Ergo] Goal store_f1_post_7_P3 : Unknown [wp] [Alt-Ergo] Goal store_f1_post_6_P2 : Unknown [wp] [Alt-Ergo] Goal store_f1_post_5_P1 : Unknown
No tags attached.
c source.c (1,375) 2011-01-07 16:23
https://bts.frama-c.com/file_download.php?file_id=148&type=bug
Issue History
2011-01-07 16:23sdupratNew Issue
2011-01-07 16:23sdupratStatusnew => assigned
2011-01-07 16:23sdupratAssigned To => dargaye
2011-01-07 16:23sdupratFile Added: source.c
2011-01-07 16:35dargayeNote Added: 0001367
2011-01-07 16:47AnneNote Added: 0001368
2011-01-07 16:50sdupratNote Added: 0001369
2011-01-07 17:20AnneNote Added: 0001370
2011-01-10 14:43AnneNote Added: 0001372
2011-01-28 11:42corrensonTarget Version => Frama-C Carbon-20110201
2011-01-31 09:18dargayeNote Added: 0001439
2011-02-01 17:04corrensonNote Added: 0001448
2011-02-01 17:04corrensonStatusassigned => resolved
2011-02-01 17:04corrensonFixed in Version => Frama-C Carbon-20110201
2011-02-01 17:04corrensonResolutionopen => fixed
2011-04-13 15:28signolesNote Added: 0001762
2011-04-13 15:28signolesStatusresolved => closed

Notes
(0001367)
dargaye   
2011-01-07 16:35   
The memory model store does not support union. Using -wp-print, you can see the warning details. Instead of rejected the PO containing "union" feature, we produce a degenerated P0. Then, if the "union" part of the PO is not crucial to the PO, it can be proved. In this example, this is not the case.
(0001368)
Anne   
2011-01-07 16:47   
With -wp-model Hoare, it stops because : Reason: unsupported cast from pointer (T_CMD) to pointer (T_CMD const) I guess Hoare should be able to handle this kind of cast. I will have a look : probably something to do, here.
(0001369)
sduprat   
2011-01-07 16:50   
Well, It could be a feature. union is a little bit supported : if we comment call of ProgrammerSortie, we can prove P3.
(0001370)
Anne   
2011-01-07 17:20   
After a small fix about the cast in Hoare, I get : [wp] [Alt-Ergo] Goal hoare_f1_post_7_P3_part1 : Valid [wp] [Alt-Ergo] Goal hoare_f1_post_7_P3_part2 : Valid [wp] [Alt-Ergo] Goal hoare_f1_post_6_P2_part1 : Valid [wp] [Alt-Ergo] Goal hoare_f1_post_5_P1 : Valid [wp] [Alt-Ergo] Goal hoare_f1_post_6_P2_part2 : Unknown It seems that the last one should also be proved, but there is a problem in [union] comparison... I investigate further...
(0001372)
Anne   
2011-01-10 14:43   
Ok : I fixed the problem of union comparison in rev 11223... $ frama-c -wp -wp-model Hoare -wp-proof alt-ergo -wp-split source.c [wp] [Alt-Ergo] Goal hoare_f1_post_7_P3_part1 : Valid [wp] [Alt-Ergo] Goal hoare_f1_post_6_P2_part2 : Valid [wp] [Alt-Ergo] Goal hoare_f1_post_6_P2_part1 : Valid [wp] [Alt-Ergo] Goal hoare_f1_post_5_P1 : Valid [wp] [Alt-Ergo] Goal hoare_f1_post_7_P3_part2 : Valid
(0001439)
dargaye   
2011-01-31 09:18   
I let Anne conclude if this bts has to be closed, since for Store it is out of scope.
(0001448)
correnson   
2011-02-01 17:04   
In Revision 11223.
(0001762)
signoles   
2011-04-13 15:28   
Fixed in WP 0.3 compatible with Frama-C Carbon.