Frama-C Bug Tracking System - Frama-C
View Issue Details
0000876Frama-CPlug-in > Evapublic2011-07-04 15:502016-01-26 08:52
yakobowski 
yakobowski 
normalminoralways
closedfixed 
Frama-C Carbon-20110201 
Frama-C Magnesium 
0000876: Widen hints for a variable should not influence the values for other variables
With the widen hint below, Value finds the range i ? [30..127] for i. Without the hint, the completely precise value {30} is found. The hint for 'next' should not degrade the results for 'i'. int max = 25; int next = 0; void main () { /*@ loop pragma WIDEN_HINTS next, 24; */ for (int i=0;i<30;i++) { int vsize = max; int vnext = next; if(vsize > vnext) next++; } }
No tags attached.
Issue History
2011-07-04 15:50yakobowskiNew Issue
2011-07-04 15:50yakobowskiStatusnew => assigned
2011-07-04 15:50yakobowskiAssigned To => pascal
2011-07-04 19:36pascalNote Added: 0002006
2011-07-04 20:05yakobowskiNote Added: 0002007
2011-07-04 20:17pascalNote Added: 0002008
2011-07-04 20:43yakobowskiNote Added: 0002009
2011-07-06 14:17pascalStatusassigned => closed
2011-07-06 14:17pascalResolutionopen => won't fix
2015-01-07 18:56yakobowskiAssigned Topascal => yakobowski
2015-01-07 18:56yakobowskiStatusclosed => assigned
2015-08-03 22:08yakobowskiNote Added: 0005997
2015-08-03 22:08yakobowskiStatusassigned => resolved
2015-08-03 22:08yakobowskiResolutionwon't fix => fixed
2016-01-26 08:51signolesFixed in Version => Frama-C Magnesium
2016-01-26 08:52signolesStatusresolved => closed
2018-01-12 14:26signolesCategoryPlug-in > value analysis => Plug-in > Eva

Notes
(0002006)
pascal   
2011-07-04 19:36   
I would say that the user providing a loop widen hint worse than the automatically inferred hint is an indication that the user wishes to have imprecise results for the loop. You can see with the authors of src/memory_state/widen.ml if you don't like it. If I was in your place, though, I would save myself the anguish and just write: /*@ loop pragma WIDEN_HINTS next, 24, i, 29 ; */ It is not difficult to provide hints that are at least as good as the algorithm there.
(0002007)
yakobowski   
2011-07-04 20:05   
The user is trying to prove that next=25 (or at least that next \in [0..25]), and is not actually really interested in i. He was just surprised that widen hints are used for variables that are not specified, which can make the analysis needlessly slower. (Admittedly, the user should have used 25 as his first hint, but got confused when writing his example.)
(0002008)
pascal   
2011-07-04 20:17   
> The user is trying to prove that next=25 (or at least that next \in [0..25]) This is not possible without unrolling the loop, and while this limitation may be considered a bug, it is not one that will get fixed. > widen hints are used for variables that are not specified, which can make the analysis needlessly slower. The automatically inferred bounds for typical for-loop programming patterns give very good results in practice and, in the rare cases they do not work, only add a couple of steps in staged widenings that have many of them.
(0002009)
yakobowski   
2011-07-04 20:43   
> This is not possible without unrolling the loop, and while this limitation may be considered a bug, it is not one that will get fixed. I'm aware of this, and do not necessarily consider it to be a bug. A single ACSL annotation '//@ assert next == vnext;' before next++ is sufficient to obtain what I want, and the assertion can be easily proven using the WP plugin. However, this only works if the value analysis widens to the good values, with my help or without. Since every iteration of the loop takes 4-5 minutes in my case, I'm very interested in reaching the fixpoint as fast as possible.
(0005997)
yakobowski   
2015-08-03 22:08   
Fix committed to master branch.