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.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] proving assigns

  • Subject: [Frama-c-discuss] proving assigns
  • From: siegel at udel.edu (Stephen Siegel)
  • Date: Fri, 18 May 2018 09:01:31 -0400
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