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.
issue