--- layout: fc_discuss_archives title: Message 58 from Frama-C-discuss on February 2011 ---
Le 18/02/2011 12:46, Pascal Cuoq a ?crit : > 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. > > From http://frama-c.com/download/frama-c-acsl-implementation.pdf : > > "only basic support for ghost code is provided (section 2.12);" (page 12) As Pascal explains, that is not a bug, but an unimplemented feature. You can post a feature request on the BTS (bts.frama-c.com). -- Julien