--- layout: fc_discuss_archives title: Message 54 from Frama-C-discuss on February 2011 ---
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