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



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 ?

Thanks in advance,

Jean Karim Zinzindohou?
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20141112/1a670c73/attachment.html>