Widen hints for a variable should not influence the values for other variables

ID0000876: This issue was created automatically from Mantis Issue 876. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0000876	Frama-C	Plug-in > Eva	public	2011-07-04	2016-01-26

Reporter	yakobowski	Assigned To	yakobowski	Resolution	fixed
Priority	normal	Severity	minor	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Carbon-20110201	Target Version	-	Fixed in Version	Frama-C Magnesium

Description :

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++;

} }