--- layout: fc_discuss_archives title: Message 23 from Frama-C-discuss on July 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Problem with array type in Frama-C



Thank you for the suggestion, that helps me a lot.

2009/7/21 Virgile Prevosto <virgile.prevosto at cea.fr>:
> Hello,
>
> Le lun. 20 juil. 2009 14:35:31 CEST,
> Tien Hoang Minh <tienhm at gmail.com> a ?crit :
>
>> /*@ logic integer getelem(integer t[], integer i) = t[i];
>> ? @*/
>>
>> The error message is "not a C type"
>> Please help me if there is an error in my annotation or if it is a
>
> The issue lies in the fact that you're trying to have an array of
> of a purely logical type (integer). This is currently not possible in
> ACSL: you can not "mix" C types (arrays, pointers) with logical types
> (integers, reals, abstract data types). Thus, you have to use an array
> of int (or long, or unsigned, or whatever). Note that the index and
> the result can still be integers on the other hand:
> - in the logical world, there is no out-of-bounds error. t[i] is a valid
> ?expression whatever the value of i is (in particular we have t[i] ==
> ?t[i]. On the other hand, if i is too large, you won't be able to tell
> ?much more about t[i] than such kind of trivial formulas)
> - t[i] gets automatically promoted to an integer when needed.
> Therefore, the you can use the following definition instead:
> /*@ logic integer getelem(int t[], integer i) = t[i]; @*/
>
> Best regards,
> --
> E tutto per oggi, a la prossima volta.
> Virgile
>
>
> _______________________________________________
> 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