Frama-C Bug Tracking System - Frama-C
View Issue Details
0001776Frama-CPlug-in > wppublic2014-05-07 14:142015-03-17 22:17
Anne 
correnson 
normalmajorhave not tried
closedfixed 
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

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