--- layout: fc_discuss_archives title: Message 23 from Frama-C-discuss on November 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Ghost structure fields.



Hello,

2014-11-12 16:48 GMT+01:00 Jean Karim Zinzindohou?
<jean-karim.zinzindohoue at inria.fr>:
> Hi,
>
> The Frama-C Neon implementation manual mentions some properties it ghost
> fields in structures, and the illustrative example in the appendix makes use
> of some.
> Yet I do not manage to get it running. I tried that for instance :
>
> typedef struct test{
> //@ ghost int lenght;
> //@ ghost char * msg;
> char hash[256];
> } test;
>
> I simply get a "[kernel] user error: syntax error" at the ghost field
> declaration line.
> Did it get the syntax wrong, or is it not supported by Frama-C ?
>

You're right, support of ghost code in Frama-C is currently minimal.
Basically, you can only add ghost statements and ghost globals, and no
verification of non-interference is done.

Best regards,

-- 
E tutto per oggi, a la prossima volta
Virgile