Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001461Frama-CPlug-in > wppublic2013-07-24 18:362014-06-17 15:02
Reportervirgile 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusacknowledgedResolutionopen 
PlatformOSOS Version
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

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

-  Notes
(0004012)
correnson (manager)
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 (manager)
2013-07-30 09:51

Feature wish: infer workaround.
(0004499)
correnson (manager)
2014-02-05 14:30

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


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker