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

  • Subject: [Frama-c-discuss] Problem with array type in Frama-C
  • From: tienhm at (Tien Hoang Minh)
  • Date: Tue, 21 Jul 2009 10:40:06 -0400
  • In-reply-to: <20090721085610.4835b7a1@is005115>
  • References: <> <20090721085610.4835b7a1@is005115>

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

2009/7/21 Virgile Prevosto <virgile.prevosto at>:
> Hello,
> Le lun. 20 juil. 2009 14:35:31 CEST,
> Tien Hoang Minh <tienhm at> 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