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] proving assigns

Thanks, Virgile, for the explanation and fix — it verifies immediately with frama-c -wp.

I actually tried something like that but with an extra assertion (see below, assertion a7).
I was never able to prove this assertion, so gave up.
Just out of curiosity, do you know how to prove it or why it cannot be proved?  It clearly follows from the loop invariant; I just want to tell some prover “please instantiate that \forall expression with k=i.”

-Steve



/*@ requires n>=0;
    requires \valid(a+(0..n-1));
    assigns a[0 .. n-1];
    ensures \forall integer k; 0<= k < n ==> a[k] == \at(a[k],Pre);
*/
void f(int *a, int n) {
  /*@ loop invariant i1: 0<=i<=n;
      loop assigns i, a[0 .. n-1];
      loop invariant \forall integer k; 0<= k < n ==> a[k] == \at(a[k],Pre);
  */
  for (int i=0; i<n; i++) {
    //@ assert a7: a[i]==\at(a[i],Pre);
    if (a[i]==2) {
      a[i]=1;
      a[i]=2;
    }
  }
}

> On May 18, 2018, at 10:07 AM, Virgile Prevosto <virgile.prevosto at m4x.org> wrote:
> 
> /*@ requires n>=0;
>     requires \valid(a+(0..n-1));
>     assigns a[0 .. n-1];
>     ensures \forall integer k; 0<= k < n ==> a[k] == \at(a[k],Pre);
> */
> void f(int *a, int n) {
>   /*@ loop invariant i1: 0<=i<=n;
>       loop assigns i, a[0 .. n-1];
>       loop invariant \forall integer k; 0<= k < n ==> a[k] == \at(a[k],Pre);
>   */
>   for (int i=0; i<n; i++) {
>     if (a[i]==2) {
>       a[i]=1;
>       a[i]=2;
>     }
>   }
> }

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20180518/497e72e7/attachment-0001.html>