--- layout: fc_discuss_archives title: Message 58 from Frama-C-discuss on November 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie: transpose_location_list => assert false



Hello,

Lanching: frama-c -jessie file.c

with file.c containing:

typedef struct { int a; int b; float c; } las;

//@ assigns *i,*j,*k;
static void g (int*i,int*j,float*k)
{	*i=1;*j=2;*k=1.0; }

void f (las *x)
{  g (&(x->a),&(x->b),&(x->c)); }


yields:

** Jc_interp_misc.transpose_location_list: TODO: parameters **
memory (mem-field(int_M),j_2)
in memory set (mem-field(float_M),k_3), (mem-field(int_M),i_1),
(mem-field(int_M),j_2)
File "jc/jc_interp_misc.ml", line 737, characters 1-1:
Uncaught exception: File "jc/jc_interp_misc.ml", line 737, characters
1-7: Assertion failed

Any advice to overcome this issue? (I'll add a BTS record on this point,
but in the mean time if anything can be done to get around this, it will
be welcome)
D.