--- layout: fc_discuss_archives title: Message 24 from Frama-C-discuss on January 2015 ---
Dear All, when analyzing the following C source (from http://www3.di.uminho.pt/~jsp/RSD-book/Frama-c-safety.pdf) with frama-c-Neon/WP in the typed model with split /*@ requires \valid(t) && \valid(t+i) && \valid(t+j); @*/ void swap(int t[], int i, int j) { int tmp = t[i]; t[i] = t[j]; t[j] = tmp; } /*@ requires 0 <= p <= r && \valid_range(A,p,r); @*/ int partition (int A[], int p, int r) { int x = A[r]; int tmp, j, i = p-1; /*@ loop invariant p <= j <= r && p-1 <= i < j && \valid(A+j) && \valid(A+i+1); @ loop variant (r-j); @*/ for (j=p; j<r; j++) if (A[j] <= x) { i++; swap(A,i,j); } swap(A,i+1,r); return i+1; } there are 3 POs from the invariant that are not discharged. For example: Goal Preservation of Invariant (file ../../frama-c/partition-10.3.c, line 14) (5/12): Tags: Then Then. Let x_1 = 1+j_1. Let x_2 = 1+i_1. Let a_0 = (shift A_0 j_1). Let x_3 = Mint_0[a_0]. Assume { (* Domain *) Type: (is_sint32 i_1) /\ (is_sint32 j_1) /\ (is_sint32 p_0) /\ (is_sint32 p_1) /\ (is_sint32 r_0) /\ (is_sint32 r_3) /\ (is_sint32 x_0) /\ (is_sint32 x_2) /\ (is_sint32 x_1) /\ (is_sint32 x_3). (* Heap *) Have: (linked Malloc_5). (* Pre-condition (file ../../frama-c/partition-10.3.c, line 8) in 'partition' *) (* Pre-condition: *) Have: (0<=p_1) /\ (p_1<=r_3) /\ (valid_rw Malloc_5 (shift A_3 p_1) (1+r_3-p_1)). (* Assertion 'rte,mem_access' (file ../../frama-c/partition-10.3.c, line 12) *) (* ../../frama-c/partition-10.3.c:12: Assertion 'rte,mem_access': *) Have: (valid_rd Malloc_5 (shift A_3 r_3) 1). (* Assertion 'rte,signed_overflow' (file ../../frama-c/partition-10.3.c, line 13) *) (* ../../frama-c/partition-10.3.c:13: Assertion 'rte,signed_overflow': *) Have: -2147483647<=p_1. (* Invariant (file ../../frama-c/partition-10.3.c, line 14) *) (* ../../frama-c/partition-10.3.c:17: Invariant: *) Have: (i_1<j_1) /\ (j_1<=r_0) /\ (p_0<=j_1) /\ (p_0<=x_2) /\ (valid_rw Malloc_1 a_0 1) /\ (valid_rw Malloc_1 (shift (shift A_0 i_1) 1) 1). (* ../../frama-c/partition-10.3.c:17: Then *) Have: j_1<r_0. (* Assertion 'rte,mem_access' (file ../../frama-c/partition-10.3.c, line 18) *) (* ../../frama-c/partition-10.3.c:18: Assertion 'rte,mem_access': *) Have: (valid_rd Malloc_1 a_0 1). (* ../../frama-c/partition-10.3.c:18: Then *) Have: x_3<=x_0. (* Assertion 'rte,signed_overflow' (file ../../frama-c/partition-10.3.c, line 19) *) (* ../../frama-c/partition-10.3.c:19: Assertion 'rte,signed_overflow': *) Have: i_1<=2147483646. (* ../../frama-c/partition-10.3.c:20: Call 'swap' *) Have: (valid_rw Malloc_1 A_0 1) /\ (valid_rw Malloc_1 (shift A_0 x_2) 1). (* Assertion 'rte,signed_overflow' (file ../../frama-c/partition-10.3.c, line 17) *) (* ../../frama-c/partition-10.3.c:17: Assertion 'rte,signed_overflow': *) Have: j_1<=2147483646. } Prove: (valid_rw Malloc_0 (shift A_0 x_1) 1). Prover Alt-Ergo returns Unknown (Qed:3ms) (1s) I fail to see why this PO is not automatically discharged. Also, how are the _0, _1, etc suffixes supposed to be read? Thanks in advance and best regards, Marko -------------- next part -------------- A non-text attachment was scrubbed... Name: not available Type: application/pgp-signature Size: 181 bytes Desc: OpenPGP Digital Signature URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150128/6cd07b8d/attachment.sig>