--- layout: fc_discuss_archives title: Message 54 from Frama-C-discuss on February 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Type of ghost variables



The ACSL manual states "Logical types, such as integer or real are
authorized in ghost code." However, the spec

//@ ghost integer var;

gives

[kernel] user error: syntax error

So there's a bug in the manual or in frama-c.

Regards,
Boris