--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on May 2018 ---
[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>