--- layout: fc_discuss_archives title: Message 62 from Frama-C-discuss on October 2010 ---
Hello B?rbara, Le mer. 20 oct. 2010 11:13:32 CEST, Barbara Vieira <barbaraisabelvieira at gmail.com> a ?crit : > But it raises a syntax error when I include the declaration: > > //@ ghost int_list ghost_a = null; > > My question is: can we declare variables of a logic type in ACSL? How? Can > that variables be declared inside the ghost code? Ghost variables with logic types are not implemented yet. Please note that each frama-c distribution comes with an acsl manual ($FRAMAC_SHARE/manuals/acsl-implementation.pdf or for Boron http://frama-c.com/download/acsl-implementation-Boron-20100401.pdf) that details which features are supported in this particular version. Model variables, which would be useful, are also unsupported You can have //@ logic int_list ghost_a = null; but in this case, you'll end up with a logic constant which is probably not what you want. A possibility (largely untested, at least by me, use at your own risks) would be to use an axiomatic containing only one (logic) variable depending on an arbitrary C variable, and to use declared functions which assigns the C variable and have an ensures modifying the logic variable, as in: //@ ghost int a_seed; /*@ axiomatic logic_a { logic int_list logic_a{L} reads a_seed; } */ /*@ assigns a_seed; ensures logic_a == cons(hd,logic_a{Pre}); */ void cons(int hd); /*@ assigns a_seed; ensures logic_a == null; */ void init(void); Then you can use (ghost) calls to the relevant functions in places where you'd have modified the ghost variable. Hope this helps, -- E tutto per oggi, a la prossima volta. Virgile