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] Problem with array type in Frama-C

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