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



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