--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on January 2010 ---
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