--- layout: fc_discuss_archives title: Message 20 from Frama-C-discuss on June 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Separation of local variables



Hello,

I am using the wp plugin, and attempting to find the best way of dealing 
with separation logic. One situation I have come across is when using 
local variables. In the example below, the assertion is unknown, but I 
expect it to be valid since 'one' is valid prior to the function.

/*@
     requires \valid(one);
*/
void f(int *one){
     int two;
     //@ assert one != &two;
}

Thanks for your time,
Ian