Internal error with assign specification on bi-dimensional arrays

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

---

Id	Project	Category	View	Due Date	Updated
ID0000032	Frama-C	Plug-in > jessie	public	2009-04-07	2009-04-10

Reporter	virgile	Assigned To	cmarche	Resolution	open
Priority	normal	Severity	minor	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Lithium-20081201	Target Version	-	Fixed in Version	-

Description :

[bug 7435 from old bts, reported by David Mentré] Hello,

Using this code: === bidim_array.c int a[12][45] = {0, };

//@ assigns a[..][..]; void f(void) { a[1][3] = 42; }

void main(void) { f(); }

The assigns clause triggers an internal error in Jessie.

$ frama-c -jessie-analysis -jessie-gen-only bidim_array.c Parsing [preprocessing] running gcc -C -E -I. -include /usr/local/stow/frama-c-lithium-2008-12-01/share/frama-c/jessie/jessie_prolog.h -dD bidim_array.c Cleaning unused parts Symbolic link Starting semantical analysis Starting Jessie translation Fatal error: exception Assert_failure("src/jessie/interp.ml", 807, 33)

Yours, d.

Additional Information :

Normalization of multi-dimensional array accesses in jessie plugin is not compatible with use of range.