# 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.

# [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>

```