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

you are right!

\valid(a) => a != 0.

------------------------------------------------------------------------------
/** @verbatim */
/*@ requires val1_valid: \valid(val1);
  @ requires val2_valid: \valid(val2);

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

  @ assigns *val1,*val2 ;
 @*/

/** @endverbatim */

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

/*@ assigns \nothing ; */
void call_swap()
{
	int a = 1;
	swap(&a, 0);
}
------------------------------------------------------------------------------

... does not validate.
Given that, the way to specify a pointer that may be valid at address
0 is to specifies it as an integer with the correct range.

Still, I would really like to know the actual definition of \valid in
the Frama-C framework.
Does it only cover positive non zero integers or is there other constraints?

Thanks for your hint, again.
Sylvain