--- layout: fc_discuss_archives title: Message 22 from Frama-C-discuss on January 2010 ---
> By typing your predicate as accepting an int, you forced a > cast to be applied to its argument each time the argument is > of type integer. To clarify, "i+1" is of type "integer" because "+" takes two integers and returns an integer. The int "i" it silently promoted to "integer" in order to apply "+" to it, but the type-checker refuses to convert the result to the int expected by have_equal_neighbours because this could lose information. /*@ predicate have_equal_neighbours{Label}(int* a, int n) = ... */ ... loop invariant !have_equal_neighbours(a, i+1); ... Pascal