Frama-C Bug Tracking System - Frama-C
View Issue Details
0001776Frama-CPlug-in > wppublic2014-05-07 14:142015-03-17 22:17
normalmajorhave not tried
Frama-C Neon-20140301 
Frama-C Sodium 
0001776: Assert erroneously proved valid
The 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.
$ frama-c -wp test.c
extern int X; void g (void) { X ++; } void f (int x, int y) { if (x > X) { g (); //@ assert ax2: x > X; // x++; } }
No tags attached.
Issue History
2014-05-07 14:14AnneNew Issue
2014-05-07 14:14AnneStatusnew => assigned
2014-05-07 14:14AnneAssigned To => correnson
2014-05-22 15:05corrensonNote Added: 0005127
2014-05-22 15:27AnneNote Added: 0005130
2014-05-23 11:24corrensonNote Added: 0005134
2014-05-23 11:24corrensonStatusassigned => resolved
2014-05-23 11:24corrensonResolutionopen => fixed
2014-05-23 11:29corrensonNote Added: 0005135
2015-03-17 22:17signolesFixed in Version => Frama-C Sodium
2015-03-17 22:17signolesStatusresolved => closed

2014-05-22 15:05   
This a problem with the assigns of g(). Seems that default assigns is \nothing in this case...
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 ?...
2014-05-23 11:24   
Fix committed to master branch.
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.