Frama-C Bug Tracking System - Frama-C
View Issue Details
0000646Frama-CPlug-in > wppublic2010-12-21 16:532011-04-13 15:28
sduprat 
dargaye 
normalminoralways
closedfixed 
Frama-C Carbon-20101202-beta2 
Frama-C Carbon-20110201 
0000646: [wp] warning: Stronger goal store_AppelerVerifier_post_6 (1 warning)
In 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);
cmd = frama-c -wp -pp-annot -wp-model Store -wp-proof alt-ergo -wp-split s_ko.c
No tags attached.
tar s.tar (10,240) 2010-12-21 16:53
https://bts.frama-c.com/file_download.php?file_id=140&type=bug
Issue History
2010-12-21 16:53sdupratNew Issue
2010-12-21 16:53sdupratStatusnew => assigned
2010-12-21 16:53sdupratAssigned To => dargaye
2010-12-21 16:53sdupratFile Added: s.tar
2010-12-22 09:35dargayeNote Added: 0001350
2010-12-22 09:35dargayeStatusassigned => resolved
2010-12-22 09:35dargayeResolutionopen => fixed
2011-04-13 15:28signolesNote Added: 0001765
2011-04-13 15:28signolesFixed in Version => Frama-C Carbon-20110201
2011-04-13 15:28signolesStatusresolved => closed

Notes
(0001350)
dargaye   
2010-12-22 09:35   
resolved in rev : 11103
(0001765)
signoles   
2011-04-13 15:28   
Fixed in WP 0.3 compatible with Frama-C Carbon.