--- layout: fc_discuss_archives title: Message 62 from Frama-C-discuss on October 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Logic types and Ghost code



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