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] Separation of local variables

  • Subject: [Frama-c-discuss] Separation of local variables
  • From: iblissard at grammatech.com (Ian Blissard)
  • Date: Tue, 10 Jun 2014 11:29:42 -0400
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