2021-03-03 03:35 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000732Frama-CPlug-in > Evapublic2014-02-12 16:59
Reporteryakobowski 
Assigned Topascal 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Carbon-20110201 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000732: Incorrect states passed to value analysis callbacks in presence of slevel
DescriptionExecute 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.
Additional InformationThe bug appears between the svn revisions 11262 and 11385.
TagsNo tags attached.
Attached Files
  • png file icon 5000.png (20,871 bytes) 2011-02-20 16:22 -
    png file icon 5000.png (20,871 bytes) 2011-02-20 16:22 +

-Relationships
+Relationships

-Notes

~0001520

pascal (reporter)

But fortunately the "After statement"s are correct.

~0001521

yakobowski (manager)

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 (manager)

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 (reporter)

Fix committed to stable/neon branch.
+Notes

-Issue History
Date Modified Username Field Change
2011-02-20 13:44 yakobowski New Issue
2011-02-20 13:44 yakobowski Status new => assigned
2011-02-20 13:44 yakobowski Assigned To => pascal
2011-02-20 16:21 pascal Note Added: 0001520
2011-02-20 16:22 pascal File Added: 5000.png
2011-02-20 17:10 yakobowski Note Added: 0001521
2011-02-20 17:41 svn
2011-02-20 17:41 svn Status assigned => resolved
2011-02-20 17:41 svn Resolution open => fixed
2011-02-20 18:12 yakobowski Note Added: 0001523
2011-02-20 18:12 yakobowski Status resolved => feedback
2011-02-20 18:12 yakobowski Resolution fixed => reopened
2011-02-20 20:29 svn
2011-02-20 20:29 svn Status feedback => resolved
2011-02-20 20:29 svn Resolution reopened => fixed
2011-10-10 14:13 signoles Fixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14 signoles Status resolved => closed
2013-12-19 01:12 pascal Source_changeset_attached => framac master 3fe35083
2013-12-19 01:12 pascal Source_changeset_attached => framac master 2560717e
2014-02-12 16:54 pascal Source_changeset_attached => framac stable/neon 3fe35083
2014-02-12 16:54 pascal Source_changeset_attached => framac stable/neon 2560717e
2014-02-12 16:59 pascal Note Added: 0004830
2014-02-12 16:59 pascal Status closed => resolved
2018-01-12 14:26 signoles Category Plug-in > value analysis => Plug-in > Eva
+Issue History