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