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: virgile.prevosto at cea.fr (Virgile Prevosto)
- Date: Tue, 21 Jul 2009 08:56:10 +0200
- In-reply-to: <e8a66d940907201135l65cd669ak92effb91e89e61ac@mail.gmail.com>
- References: <e8a66d940907201135l65cd669ak92effb91e89e61ac@mail.gmail.com>
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
- Follow-Ups:
- [Frama-c-discuss] Problem with array type in Frama-C
- From: tienhm at gmail.com (Tien Hoang Minh)
- [Frama-c-discuss] Problem with array type in Frama-C
- References:
- [Frama-c-discuss] Problem with array type in Frama-C
- From: tienhm at gmail.com (Tien Hoang Minh)
- [Frama-c-discuss] Problem with array type in Frama-C
- Prev by Date: [Frama-c-discuss] Problem with array type in Frama-C
- Next by Date: [Frama-c-discuss] Specifying function monotonicity in ACSL
- Previous by thread: [Frama-c-discuss] Problem with array type in Frama-C
- Next by thread: [Frama-c-discuss] Problem with array type in Frama-C
- Index(es):