--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on January 2016 ---
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