--- layout: fc_discuss_archives title: Message 54 from Frama-C-discuss on December 2008 ---
Hello, I have following annotated algorithm: /*@ requires 0 <= length; requires \valid_range (a, 0, length-1); requires \valid_range (dest, 0, length-1); requires disjoint_arrays(a, dest, length); ensures \result == length - nb_occ{Old}(a, 0, length, value); ensures \forall integer k; 0 <= k < \result ==> dest[k] != value; */ int remove_copy_array (int* a, int length, int* dest, int value ) { int index_a = 0; int index_dest = 0; /*@ loop invariant 0 <= index_a <= length; loop invariant index_dest <= index_a; loop invariant 0 <= index_dest <= length; loop invariant \forall integer k; 0 <= k < index_dest ==> dest[k] != value; loop invariant index_dest == index_a - nb_occ{Pre}(a, 0, index_a, value); */ for ( ; index_a != length; ++index_a) if (a[index_a] != value) { dest[index_dest] = a[index_a]; ++index_dest; } return index_dest; } The thing I am curious about is, that I get a green bullet for ensures \result == length - nb_occ{Old}(a, 0, length, value); while the related loop invariant gets stuck. Now I wonder why is that Cheers Christoph -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081217/282d93cf/attachment.htm