2021-01-25 14:13 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001776Frama-CPlug-in > wppublic2015-03-17 22:17
ReporterAnne 
Assigned Tocorrenson 
PrioritynormalSeveritymajorReproducibilityhave not tried
StatusclosedResolutionfixed 
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
+Relationships

-Notes

~0005127

correnson (manager)

This a problem with the assigns of g().
Seems that default assigns is \nothing in this case...

~0005130

Anne (reporter)

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)

Fix committed to master branch.

~0005135

correnson (manager)

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.
+Notes

-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 Source_changeset_attached => framac master 515dca69
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
+Issue History