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



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