Frama-C-discuss mailing list archives
This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Frama-c-discuss] WP plugin / question about address of variable on stack
- Subject: [Frama-c-discuss] WP plugin / question about address of variable on stack
- From: sylvain.nahas at googlemail.com (sylvain nahas)
- Date: Mon, 17 Oct 2011 09:21:54 +0200
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
- Follow-Ups:
- [Frama-c-discuss] WP plugin / question about address of variable on stack
- From: jens.gerlach at first.fraunhofer.de (Jens Gerlach)
- [Frama-c-discuss] WP plugin / question about address of variable on stack
- Prev by Date: [Frama-c-discuss] Worst case path computation
- Next by Date: [Frama-c-discuss] WP plugin / question about address of variable on stack
- Previous by thread: [Frama-c-discuss] Frama-C Nitrogen-20111001
- Next by thread: [Frama-c-discuss] WP plugin / question about address of variable on stack
- Index(es):