--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on April 2009 ---
Hello, Jessie is unable to prove assigns a[..] in this code: /*@ requires \valid(a+ (0..aLength-1)); assigns a[..]; */ void foo(int a[], int aLength) { int j; //@ loop invariant 0 <= j; for(j=0; j<aLength; j++) { a[j] = 0; } } I suppose that "assigns" is broken for arrays. - Boris