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