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

[Frama-c-discuss] Unable to prove assigns clause for array



Hello,

I'm trying to verify the following code:


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

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


However, I'm unable to prove assigns a[0..aLength-2]. I recall that David Mentre had a similar problem proving an assigns clause on arrays.

In addition, Simplify (but not Alt-Ergo) is unable to check  x = a[aLength-1] for arithmetic overflow.

Any suggestions?

- Boris