--- layout: fc_discuss_archives title: Message 22 from Frama-C-discuss on January 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] adjacent_find problem



> 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