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.