--- layout: fc_discuss_archives title: Message 20 from Frama-C-discuss on October 2011 ---
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