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