--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on April 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Assigns broken for arrays?



Hello Virgile,

Now I've added a loop assigns clause but I'm still unable to verify the code. Jessie can't prove the assigns postcondition - neither with Alt-Ergo, nor with Simplify or Z3.

- Boris


/*@ requires \valid(a+ (0..aLength-1));
    assigns a[..];
*/
void foo(int a[], int aLength) {
  int j;

  /*@ loop invariant 0 <= j;
      loop assigns a[..];
  */
  for(j=0; j<aLength; j++) {
    a[j] = 0;
  }
}