Frama-C Bug Tracking System - Frama-C
View Issue Details
0000662Frama-CPlug-in > wppublic2011-01-07 16:232011-04-13 15:28
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
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

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.
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.
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.
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...
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
2011-01-31 09:18   
I let Anne conclude if this bts has to be closed, since for Store it is out of scope.
2011-02-01 17:04   
In Revision 11223.
2011-04-13 15:28   
Fixed in WP 0.3 compatible with Frama-C Carbon.