--- layout: fc_discuss_archives title: Message 21 from Frama-C-discuss on July 2009 ---
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