Frama-C Bug Tracking System - Frama-C
View Issue Details
0000732Frama-CPlug-in > Evapublic2011-02-20 13:442014-02-12 16:59
yakobowski 
pascal 
normalmajoralways
closedfixed 
Frama-C Carbon-20110201 
Frama-C Nitrogen-20111001 
0000732: Incorrect states passed to value analysis callbacks in presence of slevel
Execute the following program with options '-val -slevel n' for n between 1 and 10001. int p[20000]; void main () { for (int j=0;j<10000;j++) p[j]=1; } Inspecting the values of the variable j in the gui reveals ranges of the form [n..10000], which is clearly incorrect. Also, there is a big gap in the execution time between a fully symbolic evaluation (-slevel 10001) and a partial one (eg. -slevel 10000). This seems to be related to superposing the states in the callbacks.
The bug appears between the svn revisions 11262 and 11385.
No tags attached.
png 5000.png (20,871) 2011-02-20 16:22
https://bts.frama-c.com/file_download.php?file_id=177&type=bug
png
Issue History
2011-02-20 13:44yakobowskiNew Issue
2011-02-20 13:44yakobowskiStatusnew => assigned
2011-02-20 13:44yakobowskiAssigned To => pascal
2011-02-20 16:21pascalNote Added: 0001520
2011-02-20 16:22pascalFile Added: 5000.png
2011-02-20 17:10yakobowskiNote Added: 0001521
2011-02-20 17:41svnCheckin
2011-02-20 17:41svnStatusassigned => resolved
2011-02-20 17:41svnResolutionopen => fixed
2011-02-20 18:12yakobowskiNote Added: 0001523
2011-02-20 18:12yakobowskiStatusresolved => feedback
2011-02-20 18:12yakobowskiResolutionfixed => reopened
2011-02-20 20:29svnCheckin
2011-02-20 20:29svnStatusfeedback => resolved
2011-02-20 20:29svnResolutionreopened => fixed
2011-10-10 14:13signolesFixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14signolesStatusresolved => closed
2014-02-12 16:59pascalNote Added: 0004830
2014-02-12 16:59pascalStatusclosed => resolved
2018-01-12 14:26signolesCategoryPlug-in > value analysis => Plug-in > Eva

Notes
(0001520)
pascal   
2011-02-20 16:21   
But fortunately the "After statement"s are correct.
(0001521)
yakobowski   
2011-02-20 17:10   
Yes, actually the summary of my bug may be wrong. I did not test the Record_Value callbacks, and the gui uses the global state table.
(0001523)
yakobowski   
2011-02-20 18:12   
Although the bug on the value of j is corrected, I believe we have lost precision. Previously, the final results were of the form p[0..n-1] ? {1; } [n..9990] ? {0; 1; } [10000..19999] ? {0; } j ? {1000; } again with n the slevel value. Now, if the slevel is not sufficient, the result is always p[0..9999] ? {0; 1; } [10000..19999] ? {0; } j ? {10000; }
(0004830)
pascal   
2014-02-12 16:59   
Fix committed to stable/neon branch.