--- layout: fc_discuss_archives title: Message 60 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



Thank you very much for that hint!
Yes it "locally" works for this simple example.
But for the whole real code, I'm afraid I need region separation.

After a quick check, it is an "old" bug already known in BTS (several 
times it seems #80,112,303,31,106,39?) ... I won't add another issue!

D.

Rousset Nicolas a ?crit :
> An ad hoc solution:
> 
> Looking at the source code, it seems it has to do with the 'region analysis' (which is done by default), so let's try the option -jessie-no-regions...
> Yep! It works :-)
> 
> Hope this help
> 
> - Nicolas
> 
> -----Original Message-----
> From: frama-c-discuss-bounces at lists.gforge.inria.fr [mailto:frama-c-discuss-bounces at lists.gforge.inria.fr] On Behalf Of Pariente Dillon
> Sent: jeudi 19 novembre 2009 14:57
> To: Frama-C public discussion
> Subject: [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.
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>