2021-01-26 06:47 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001461Frama-CPlug-in > wppublic2014-06-17 15:02
Assigned Tocorrenson 
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in Version 
Summary0001461: assigns, loop assigns and loop invariant
DescriptionIn 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;
Steps To Reproduceframa-c -wp test.c
TagsNo tags attached.
Attached Files

related to 0001812acknowledgedcorrenson Assigns not respected in behaviors when using pointers to pointers 



correnson (manager)

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.


correnson (manager)

Feature wish: infer workaround.


correnson (manager)

Feature wish

-Issue History
Date Modified Username Field Change
2013-07-24 18:36 virgile New Issue
2013-07-24 18:36 virgile Status new => assigned
2013-07-24 18:36 virgile Assigned To => correnson
2013-07-30 09:50 correnson Note Added: 0004012
2013-07-30 09:51 correnson Note Added: 0004013
2013-07-30 09:51 correnson Status assigned => confirmed
2014-02-05 14:30 correnson Note Added: 0004499
2014-02-05 14:30 correnson Status confirmed => acknowledged
2014-06-17 11:02 correnson Relationship added related to 0001812
+Issue History