--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on May 2018 ---
Hello Frama-C community, Iâm trying to prove the following program, assign.c, with Frama-C/WP : /*@ requires n>=0; @ requires \valid(a+(0..n-1)); @ assigns \nothing; @*/ void f(int *a, int n) { /*@ loop invariant i1: 0<=i<=n; @ loop assigns i; @*/ for (int i=0; i<n; i++) { if (a[i]==2) { a[i]=1; a[i]=2; } } } My understanding of the semantics of âassignsâ is that every variable not listed in the assigns clause has the same value in the post-state that it had in the pre-state. Similarly for âloop assignsâ. Therefore the contract should be valid. However, I canât find any combination of additional assertions or loop invariants that will prove the program. Maybe I am missing something or have the semantics wrong? -Steve