--- layout: fc_discuss_archives title: Message 22 from Frama-C-discuss on November 2014 ---
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>