--- layout: fc_discuss_archives title: Message 20 from Frama-C-discuss on January 2010 ---
Hello Guillaume, thanks for your answer but I do not see where an overflow could occur. 1.) inside the predicate we have 0 <= i < n-1 and thus 1 <= i+1 < n 2.) the first loop invariant says: loop invariant 0 <= i < n; thus the i+1 in loop invariant !have_equal_neighbours(a, i+1); should be fine as well. Regards Jens Am 16.01.2010 um 12:13 schrieb Guillaume Melquiond: > 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 > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss -- Dr.-Ing. Jens Gerlach Eingebettete Systeme - EST Tel.: +49 (0)30 6392 1841 Fax.: +49 (0)30 6392 1805 E-Mail: jens.gerlach at first.fraunhofer.de Fraunhofer-Institut f?r Rechnerarchitektur und Softwaretechnik, FIRST Kekul?stra?e 7 12489 Berlin Germany http://www.first.fraunhofer.de -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100116/442e61b7/attachment.htm