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
Assigned Tocorrenson 
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
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.
correnson (manager)
2013-07-30 09:51

Feature wish: infer workaround.
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 - 2020 MantisBT Team
Powered by Mantis Bugtracker