Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001776Frama-CPlug-in > wppublic2014-05-07 14:142015-03-17 22:17
ReporterAnne 
Assigned Tocorrenson 
PrioritynormalSeveritymajorReproducibilityhave not tried
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Neon-20140301 
Target VersionFixed in VersionFrama-C Sodium 
Summary0001776: Assert erroneously proved valid
DescriptionThe assertion of the following example is proved valid by QED, but it is not since the call to g modifies X. If the [x++] statement is added after the assertion, the problem disappear.
Steps To Reproduce$ frama-c -wp test.c
Additional Informationextern int X;
void g (void) {
  X ++;
}
void f (int x, int y) {
  if (x > X) {
    g ();
    //@ assert ax2: x > X;
    // x++;
    }
}
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0005127)
correnson (manager)
2014-05-22 15:05

This a problem with the assigns of g().
Seems that default assigns is \nothing in this case...
(0005130)
Anne (reporter)
2014-05-22 15:27

Thank you Loïc to have look at the problem.

I thought that the default assigns is "everything" for defined function if there is no assigns property, isn't it ?

And why the behavior is changing when adding a statement AFTER the property ?...
(0005134)
correnson (manager)
2014-05-23 11:24

Fix committed to master branch.
(0005135)
correnson (manager)
2014-05-23 11:29

The problem is tricky to explain (and was so to debug).
The variable X was properly assigned by the inferred 'assigns everything' of function g(), but it magically goes back since there is no other reference to X afterwards, from the 'else' branch. There was actually a bug in the implementation of 'assigns everything' in function calls in such a case...
Not really harmful in practice, hopefully.

- Issue History
Date Modified Username Field Change
2014-05-07 14:14 Anne New Issue
2014-05-07 14:14 Anne Status new => assigned
2014-05-07 14:14 Anne Assigned To => correnson
2014-05-22 15:05 correnson Note Added: 0005127
2014-05-22 15:27 Anne Note Added: 0005130
2014-05-23 11:24 correnson Note Added: 0005134
2014-05-23 11:24 correnson Status assigned => resolved
2014-05-23 11:24 correnson Resolution open => fixed
2014-05-23 11:29 correnson Note Added: 0005135
2015-03-17 22:17 signoles Fixed in Version => Frama-C Sodium
2015-03-17 22:17 signoles Status resolved => closed


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker