Frama-C Bug Tracking System
Main | My View | View Issues | Change Log | Roadmap | Repositories
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000646Frama-CPlug-in > wppublic2010-12-21 16:532011-04-13 15:28
Reportersduprat 
Assigned Todargaye 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
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 Filestar file icon s.tar [^] (10,240 bytes) 2010-12-21 16:53

- Relationships

-  Notes
(0001350)
dargaye (developer)
2010-12-22 09:35

 resolved in rev : 11103
(0001765)
signoles (manager)
2011-04-13 15:28

 Fixed in WP 0.3 compatible with Frama-C Carbon.

- 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

Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker