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] question about partition.c


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                    |