--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on October 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] WP plugin / question about address of variable on stack



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