--- layout: fc_discuss_archives title: Message 13 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



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