Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] Aliasing issues with local variables
  • From: john.eriksson.16 at gmail.com (John Eriksson)
  • Date: Tue, 26 Jan 2016 09:38:59 +0100
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