Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000876Frama-CPlug-in > value analysispublic2011-07-04 15:502016-01-26 08:52
Reporteryakobowski 
Assigned Toyakobowski 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Carbon-20110201 
Target VersionFixed in VersionFrama-C Magnesium 
Summary0000876: Widen hints for a variable should not influence the values for other variables
DescriptionWith 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++;
  }
}
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0002006)
pascal (reporter)
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 (manager)
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 (reporter)
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 (manager)
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 (manager)
2015-08-03 22:08

Fix committed to master branch.

- Issue History
Date Modified Username Field Change
2011-07-04 15:50 yakobowski New Issue
2011-07-04 15:50 yakobowski Status new => assigned
2011-07-04 15:50 yakobowski Assigned To => pascal
2011-07-04 19:36 pascal Note Added: 0002006
2011-07-04 20:05 yakobowski Note Added: 0002007
2011-07-04 20:17 pascal Note Added: 0002008
2011-07-04 20:43 yakobowski Note Added: 0002009
2011-07-06 14:17 pascal Status assigned => closed
2011-07-06 14:17 pascal Resolution open => won't fix
2015-01-07 18:56 yakobowski Assigned To pascal => yakobowski
2015-01-07 18:56 yakobowski Status closed => assigned
2015-08-03 22:08 yakobowski Note Added: 0005997
2015-08-03 22:08 yakobowski Status assigned => resolved
2015-08-03 22:08 yakobowski Resolution won't fix => fixed
2016-01-26 08:51 signoles Fixed in Version => Frama-C Magnesium
2016-01-26 08:52 signoles Status resolved => closed


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker