--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on January 2016 ---
Hi, The memory model used by Frama-C/WP has been largely improved since Neon ; especially, some known problem regarding framing and structures have been fixed. You are strongly encouraged to shift to the newly released Magnesium version ! Cdlt, L. PS: your code is entirely proved with the last version of frama-c -wp > Le 26 janv. 2016 à 09:38, John Eriksson <john.eriksson.16 at gmail.com> a écrit : > > I have been experimenting with Frama-C for a research project, and I'm > confused by some aliasing issues. It seems that Frama-C believes that > a local variable aliases with a struct that the function has a pointer > to, as shown in the code example. When I try to prove the function > annotations with WP for the "test" function in the code given below, > one of the assertions stop being valid after a local variable > assignment. Are there any fixes or workarounds to convince Frama-C > that local variables and the content pointed to by the pointer does > not overlap? > > I'm running a slightly older version of Frama-C (Neon-20140301) since > it's the one I have managed to get to work on Windows so far. > > > > typedef struct { > int i1; > char c1; > } struct1; > > typedef struct { > int i2; > > } struct2; > > //@assigns \nothing; > struct1 getStruct1(){ > struct1 temp1; > temp1.i1 = 7; > temp1.c1 = 'c'; > return temp1; > } > > /*@ > requires \valid(t1); > assigns \nothing; > ensures \valid(t1); > */ > void stuff(int *t1){ > } > > /*@ > requires \valid(s2p); > requires s2p->i2 == 1 || s2p->i2 == 2; > ensures s2p->i2 == 1 || s2p->i2 == 2; > */ > void test(struct2 *s2p){ > int localInt; > > //@assert s2p->i2 == 1 || s2p->i2 == 2; > struct1 s1 = getStruct1(); > > //@assert s2p->i2 == 1 || s2p->i2 == 2; > localInt = s1.i1; > // Suddenly the assert is no longer valid. > // Can be "fixed" though by removing the statement that takes the > address of the local variable. > //@assert s2p->i2 == 1 || s2p->i2 == 2; > stuff(&localInt); > } > > // John Eriksson > // KTH > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss