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



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                    |