--- layout: fc_discuss_archives title: Message 19 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



Jens Gerlach a ?crit :
> then I obtain the error message 
> 
> adjacent_find.c:34:[kernel] user error: Error during annotations 
> analysis: invalid implicit conversion from integer to int 
> 
> which refers to the third loop invariant.
> I am not sure whether it's a bug or a feature,

It's a bug in your specification. Your predicate shouldn't use "int" as 
the type of "n" but "integer", so that it doesn't involve possibly 
overflowing arithmetic:

/*@
   predicate
     have_equal_neighbours{Label}(int* a, integer n) =
       \exists int i; 0 <= i < n-1 && a[i] == a[i+1];
*/

All the proof obligations are then proved.

Best regards,

Guillaume