Frama-C Bug Tracking System - Frama-C
View Issue Details
0001461Frama-CPlug-in > wppublic2013-07-24 18:362014-06-17 15:02
virgile 
correnson 
normalminoralways
acknowledgedopen 
Frama-C GIT, precise the release id 
 
0001461: assigns, loop assigns and loop invariant
In the following (admittedly contrived) example, the assigns of g is not proved by WP (in fact it is reduced to false by Qed), although it is correct from ACSL semantics: as long as the loop invariant states that x still has its old value, the fact that it is mentioned in the loop assigns should not impede its absence in the assigns. --- test.c int x; /*@ assigns \nothing; */ int g() { /*@ loop assigns i,x; loop invariant x == \at(x,Pre); */ for (int i = 0; i<2; i++); return x; }
frama-c -wp test.c
No tags attached.
related to 0001812acknowledged correnson Assigns not respected in behaviors when using pointers to pointers 
Issue History
2013-07-24 18:36virgileNew Issue
2013-07-24 18:36virgileStatusnew => assigned
2013-07-24 18:36virgileAssigned To => correnson
2013-07-30 09:50corrensonNote Added: 0004012
2013-07-30 09:51corrensonNote Added: 0004013
2013-07-30 09:51corrensonStatusassigned => confirmed
2014-02-05 14:30corrensonNote Added: 0004499
2014-02-05 14:30corrensonStatusconfirmed => acknowledged
2014-06-17 11:02corrensonRelationship addedrelated to 0001812

Notes
(0004012)
correnson   
2013-07-30 09:50   
This is known limitation of the WP. Assigns are verified with a stronger method than necessary: WP checks that all effects are included in the assigns specified, which is sufficient but not necessary. The workaround is to modify the contract with: /*@ assigns x; ensures x ==\old(x); */ int g() { /*@ loop assigns i,x; loop invariant x == \at(x,Pre); */ for (int i = 0; i<2; i++); return x; } An evolution of the WP may infer automatically this workaround.
(0004013)
correnson   
2013-07-30 09:51   
Feature wish: infer workaround.
(0004499)
correnson   
2014-02-05 14:30   
Feature wish