--- layout: fc_discuss_archives title: Message 102 from Frama-C-discuss on March 2009 ---
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