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