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

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