--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on May 2018 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] proving assigns



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