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] WP plugin / question about address of variable on stack

  • Subject: [Frama-c-discuss] WP plugin / question about address of variable on stack
  • From: sylvain.nahas at googlemail.com (sylvain nahas)
  • Date: Mon, 17 Oct 2011 09:21:54 +0200
Hi,

I am exercising the WP Frama-C plugin, and stumbled onto the following problem.

Consider:

------------------------------------------------------------------------------
/*@ requires val1_valid: \valid(val1) && ( val1 != \null );
  @ requires val2_valid: \valid(val2) && ( val2 != \null );

  @ ensures C: *val1 == \old(*val2) ;
  @ ensures D: *val2 == \old(*val1) ;

  @ assigns *val1,*val2 ;
 @*/

void swap(int *val1,int *val2)
{
	int tmp = *val1;
	*val1 = *val2;
	*val2 = tmp;
}

/*@ assigns \nothing ; */
void call_swap()
{
	int a = 1;
	int b = 2;
	/*@ assert A_is_valid: \valid(&a); */
	/*@ assert A_is_not_null: &a != \null; */
	/*@ assert B_is_valid: \valid(&b); */
	/*@ assert B_is_not_null: &b != \null; */
	swap(&a, &b);
}
------------------------------------------------------------------------------
[ Partial ] Pre-condition 'val1_valid' in 'swap' at call 'swap' (file
swap.c, line 38)
            By WP-Store, with pending:
             - Assertion 'A_is_not_null' (file swap.c, line 35)
             - Assertion 'B_is_not_null' (file swap.c, line 37)
------------------------------------------------------------------------------

I can get only a partial proof of the code above, whereas IMO it could
be completely validated.

As I understand the issue, the WP plugin can not deduce from the fact
a variable is declared on the function's stack that a pointer that
references its address is not null.

Is it so? What are the recommended practice in this case to get a full
certification of the code?

BTW, I could not find in the ACSL doc. a clear/formal description of
what \valid means. Is there one?

Thanks much in advance,
Sylvain Nahas