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] 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