--- layout: fc_discuss_archives title: Message 30 from Frama-C-discuss on January 2015 ---
At Thu, 29 Jan 2015 19:47:52 +0100, Claude Marche wrote: > > > > On 01/29/2015 07:03 PM, Marko Sch?tz Schmuck wrote: > > /*@ requires \valid(t) > > && \valid(t+i) && \valid(t+j); > > @*/ > > Why adding \valid(t) here ??? Thanks for your help. That was one of the mutations I tried when getting all the POs of the initial version discharged automatically. Even when I go back to that original version /*@ requires \valid_index(t,i) && \valid_index(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); @ assigns A[p..r]; @*/ int partition (int A[], int p, int r) { int x = A[r]; int j, i = p-1; /*@ loop invariant p <= j <= r && p-1 <= i < j; @ loop variant (r-j); @*/ for (j=p; j<r; j++) if (A[j] <= x) { swap(A,i,j); i++; } swap(A,i+1,r); return i+1; } the POs for the pre-condition of swap are not automatically discharged and I'm left with e.g. Goal swap_pre_4: Pre-condition (file ../../frama-c/partition-10.3.c, line 1) in 'partition' at call 'swap' (file ../../frama-c/partition-10.3.c, line 20): Let a_0 = (shift A_0 j_0). Let x_1 = Mint_0[a_0]. Assume { (* Domain *) Type: (is_sint32 i_0) /\ (is_sint32 j_0) /\ (is_sint32 p_0) /\ (is_sint32 p_1) /\ (is_sint32 r_0) /\ (is_sint32 r_1) /\ (is_sint32 x_0) /\ (is_sint32 x_1). (* Heap *) Have: (linked Malloc_3). (* Pre-condition (file ../../frama-c/partition-10.3.c, line 8) in 'partition' *) (* Pre-condition: *) Have: (0<=p_1) /\ (p_1<=r_1) /\ (valid_rw Malloc_3 (shift A_3 p_1) (1+r_1-p_1)). (* Invariant (file ../../frama-c/partition-10.3.c, line 15) *) (* ../../frama-c/partition-10.3.c:18: Invariant: *) Have: (i_0<j_0) /\ (j_0<=r_0) /\ (p_0<=j_0) /\ (p_0<=(1+i_0)). (* ../../frama-c/partition-10.3.c:18: Then *) Have: j_0<r_0. (* ../../frama-c/partition-10.3.c:19: Then *) Have: x_1<=x_0. } Prove: (valid_rw Malloc_0 (shift A_0 i_0) 1) /\ (valid_rw Malloc_0 a_0 1). Prover Alt-Ergo returns Unknown (Qed:1ms) Is there some documentation about how to read this output? Specifically, what do the _1, _3 etc mean? Do they stand for specific program states? What does "linked" mean? 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/20150130/44610807/attachment.sig>