--- layout: fc_discuss_archives title: Message 60 from Frama-C-discuss on November 2009 ---
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 >