--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on April 2009 ---
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; } }