2021-01-25 13:41 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000646Frama-CPlug-in > wppublic2011-04-13 15:28
Reportersduprat 
Assigned Todargaye 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Carbon-20101202-beta2 
Target VersionFixed in VersionFrama-C Carbon-20110201 
Summary0000646: [wp] warning: Stronger goal store_AppelerVerifier_post_6 (1 warning)
DescriptionIn the attached source-file, wp processing generates this warning and fails in the proof.

The problem disappears if I delete the "const" attribute of the second parameter in the VerifierSortie prototype (see s_ok.c)

extern T_RES VerifierSortie(const T_EP ep, T_ERREUR const * err);

Additional Informationcmd = frama-c -wp -pp-annot -wp-model Store -wp-proof alt-ergo -wp-split s_ko.c
TagsNo tags attached.
Attached Files
  • tar file icon s.tar (10,240 bytes) 2010-12-21 16:53

-Relationships
+Relationships

-Notes

~0001350

dargaye (developer)

resolved in rev : 11103

~0001765

signoles (manager)

Fixed in WP 0.3 compatible with Frama-C Carbon.
+Notes

-Issue History
Date Modified Username Field Change
2010-12-21 16:53 sduprat New Issue
2010-12-21 16:53 sduprat Status new => assigned
2010-12-21 16:53 sduprat Assigned To => dargaye
2010-12-21 16:53 sduprat File Added: s.tar
2010-12-22 09:35 dargaye Note Added: 0001350
2010-12-22 09:35 dargaye Status assigned => resolved
2010-12-22 09:35 dargaye Resolution open => fixed
2011-04-13 15:28 signoles Note Added: 0001765
2011-04-13 15:28 signoles Fixed in Version => Frama-C Carbon-20110201
2011-04-13 15:28 signoles Status resolved => closed
+Issue History