--- layout: fc_discuss_archives title: Message 56 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



On Fri, Feb 18, 2011 at 12:41 PM, Boris Hollas
<hollas at informatik.htw-dresden.de> wrote:
> 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.