--- layout: fc_discuss_archives title: Message 54 from Frama-C-discuss on December 2008 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] green postcondition in spite of invalid loop invariant



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