Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000732Frama-CPlug-in > value analysispublic2011-02-20 13:442014-02-12 16:59
Reporteryakobowski 
Assigned Topascal 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
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 Filespng file icon 5000.png [^] (20,871 bytes) 2011-02-20 16:22

- Relationships

-  Notes
(0001520)
pascal (reporter)
2011-02-20 16:21

But fortunately the "After statement"s are correct.
(0001521)
yakobowski (manager)
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 (manager)
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 (reporter)
2014-02-12 16:59

Fix committed to stable/neon branch.

- 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 Checkin
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 Checkin
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
2014-02-12 16:59 pascal Note Added: 0004830
2014-02-12 16:59 pascal Status closed => resolved


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker