Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000662Frama-CPlug-in > wppublic2011-01-07 16:232011-04-13 15:28
Reportersduprat 
Assigned Todargaye 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Carbon-20101202-beta2 
Target VersionFrama-C Carbon-20110201Fixed in VersionFrama-C Carbon-20110201 
Summary0000662: warning: Degenerated goal
Descriptionwarning degenerated goal is raised with this source example containing unions.
ensures are unproved.
Additional Informationframa-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
TagsNo tags attached.
Attached Filesc file icon source.c [^] (1,375 bytes) 2011-01-07 16:23 [Show Content]

- Relationships

-  Notes
(0001367)
dargaye (developer)
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 (reporter)
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 (reporter)
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 (reporter)
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 (reporter)
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 (developer)
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 (manager)
2011-02-01 17:04

In Revision 11223.
(0001762)
signoles (manager)
2011-04-13 15:28

Fixed in WP 0.3 compatible with Frama-C Carbon.

- Issue History
Date Modified Username Field Change
2011-01-07 16:23 sduprat New Issue
2011-01-07 16:23 sduprat Status new => assigned
2011-01-07 16:23 sduprat Assigned To => dargaye
2011-01-07 16:23 sduprat File Added: source.c
2011-01-07 16:35 dargaye Note Added: 0001367
2011-01-07 16:47 Anne Note Added: 0001368
2011-01-07 16:50 sduprat Note Added: 0001369
2011-01-07 17:20 Anne Note Added: 0001370
2011-01-10 14:43 Anne Note Added: 0001372
2011-01-28 11:42 correnson Target Version => Frama-C Carbon-20110201
2011-01-31 09:18 dargaye Note Added: 0001439
2011-02-01 17:04 correnson Note Added: 0001448
2011-02-01 17:04 correnson Status assigned => resolved
2011-02-01 17:04 correnson Fixed in Version => Frama-C Carbon-20110201
2011-02-01 17:04 correnson Resolution open => fixed
2011-04-13 15:28 signoles Note Added: 0001762
2011-04-13 15:28 signoles Status resolved => closed


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker