Frama-C Bug Tracking System - Frama-C
View Issue Details
0000032Frama-CPlug-in > jessiepublic2009-04-07 15:192009-04-10 10:23
virgile 
cmarche 
normalminoralways
assignedopen 
Frama-C Lithium-20081201 
 
0000032: Internal error with assign specification on bi-dimensional arrays
[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.
Normalization of multi-dimensional array accesses in jessie plugin is not compatible with use of range.
No tags attached.
related to 0000185assigned cmarche Frama-C cannot process properly arrays of structures 
related to 0001093assigned cmarche Passing multi-dimensional arrays via reference fails 
Issue History
2009-04-07 15:19virgileNew Issue
2009-04-07 15:42signolesStatusnew => acknowledged
2009-04-10 10:23signolesStatusacknowledged => assigned
2009-04-10 10:23signolesAssigned To => cmarche
2009-07-17 11:40virgileRelationship addedrelated to 0000185
2012-02-14 09:05virgileRelationship addedrelated to 0001093

There are no notes attached to this issue.