--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on January 2016 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Aliasing issues with local variables



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