--- layout: fc_discuss_archives title: Message 18 from Frama-C-discuss on October 2011 ---
Hello Sylvain, I have not an answer to your question but I would like to understand why you require that the arguments of swap are not zero. Is it not enough that they are valid pointers? At least, this is what we thought when we specified swap in section 6.2 of our "ACSL by Example" document http://www.first.fraunhofer.de/fileadmin/FIRST/ACSL-by-Example.pdf . Regards Jens On 17 Oct 2011, at 09:21, sylvain nahas wrote: > 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 > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss