Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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