--- layout: fc_discuss_archives title: Message 23 from Frama-C-discuss on January 2010 ---
Guillaume Melquiond wrote: > 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]; > */ > > /*@ predicate have_equal_neighbours{Label}(int* a, integer n) = \exists *integer* i; 0 <= i < n-1 && a[i] == a[i+1]; */ might even simplify the job of provers. I'd like to have a way to enforce the use of integer instead of int in annotations (when pertinent of course): any suggestion ? - Claude -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | mobile: +33 6 33 14 57 93 Parc Orsay Universit? | fax: +33 1 74 85 42 29 4, rue Jacques Monod - B?timent N | http://www.lri.fr/~marche/ F-91893 ORSAY Cedex |