Locations.valid_enumerate_bits enumerate invalid bits

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

---

Id	Project	Category	View	Due Date	Updated
ID0001264	Frama-C	Plug-in > Eva	public	2012-08-08	2013-04-19

Reporter	yakobowski	Assigned To	yakobowski	Resolution	fixed
Priority	low	Severity	tweak	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Nitrogen-20111001	Target Version	-	Fixed in Version	Frama-C Fluorine-20130401

Description :

The program below shows that valid_enumerate_bits can return Top intervals, even on bases where the validity is completely known. This defeats the purpose of the function, and can cause very subtle bugs with the "default" flag in Offsetmap_bitwise.

---------- many.c ---------------- struct s { int f1; int f2; };

struct s t[10][10];

void main() { for (int i=0; i<10; i++) { for (int j=0; j<10; j++) { t[i][j].f1 = 1; } } }

Command-line: frama-c -val many.c -out -plevel 80 -slevel 50

This combination of slevel/plevel will result in only one " more than foo elements to enumerate. Approximating." message, caused by the Out plugin.

---

Output:

[inout] Out (internal) for function main: t[..]; i; j

The expected output is t[0..9][0..9]; i; j

Additional Information :

The problem lies either in valid_enumerate_bits itself, or in Lattice_Interval_Set.from_ival_int