Frama-C Bug Tracking System - Frama-C
View Issue Details
0001670Frama-CPlug-in > wppublic2014-03-04 09:362015-03-17 22:17
Anne 
correnson 
normalminoralways
closedfixed 
 
Frama-C Sodium 
0001670: WP ignores some goals when 'initialized' is used in hypotheses
The message: [wp] warning: Allocable, Freeable, Valid_read, Fresh and Initialized not yet implemented is perfectly clear, but I would have expected that annotations using these predicates would have been ignored. Instead of that, proof obligations of other annotations simply disappear.
Example: /*@ requires r1: \initialized(Y+(0 .. 99)); assigns X[0..99]; ensures X[0] == Y[0]; */ void cp( int *X, int *Y ); void f (int *A, int *B) { cp(B, A); /*@ assert a1: A[0] == B[0]; */ } Without the 'requires' property, the assertion is proved: $ frama-c -wp test.c -wp-prop a1 ... [wp] 1 goal scheduled [wp] [Qed] Goal typed_f_assert_a1 : Valid [wp] Proved goals: 1 / 1 Qed: 1 With the 'requires' property, the assertion is not even scheduled as a goal: $ frama-c -wp test.c -wp-prop a1 ... [wp] 0 goal scheduled [wp] Proved goals: 0 / 0
No tags attached.
Issue History
2014-03-04 09:36AnneNew Issue
2014-03-04 09:36AnneStatusnew => assigned
2014-03-04 09:36AnneAssigned To => correnson
2014-06-02 15:38corrensonNote Added: 0005180
2014-06-02 15:38corrensonStatusassigned => resolved
2014-06-02 15:38corrensonResolutionopen => fixed
2015-03-17 22:17signolesFixed in Version => Frama-C Sodium
2015-03-17 22:17signolesStatusresolved => closed

Notes
(0005180)
correnson   
2014-06-02 15:38   
Fix committed to master branch.