--- layout: fc_discuss_archives title: Message 26 from Frama-C-discuss on February 2011 ---
"only basic support for ghost code is provided (section 2.12);" (page 12) The sentence that you quote, "Logical types, such as integer or real are authorized in ghost code", is colored in red in the ACSL implementation manual.