--- layout: fc_discuss_archives title: Message 28 from Frama-C-discuss on January 2015 ---
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 ??? > 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); These last two invariants cannot be what you want ... > @ loop variant (r-j); > there are 3 POs from the invariant that are not discharged. For > example: > > [...] > 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? I guess that when calling swap(A,i,j), there is no way to prove the extra pre-condition \valid(t) you added. Be careful with your annotations... - Claude > _______________________________________________ > 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 > -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | Universit? Paris-sud, Bat. 650 | http://www.lri.fr/~marche/ F-91405 ORSAY Cedex |