--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on August 2013 ---
> > Or is it available in the current implementation the addtional ghost parameters to functions ? Any example on how to use it? > > No. Basically, the current support of ghost is minimal: you can > declare ghost variables (but only with C types) and have ghost > statements, and there's no guarantee that ghost statements do not > modify "real" locations. But even if this was the case, I'm not > completely sure of what you could do with it in your example. Have you > something like that in mind? > > int x = 0; > > /*@ requires x == g_x; > requires g_x == 0; > requires y >= 0; > ensures \result > x; > */ > int f(int y) /*@ ghost (int g_x) */; No, but it is a good idea to try. However, your code is not good for my frama-c. I added a body for the function, removed the parentheis around (int g_x) and added the semicolon: /*@ requires x == g_x; requires g_x == 0; requires y >= 0; ensures \result > x; */ int f(int y) { /*@ ghost int g_x; */ return y +1; } ghost4.c:3:[kernel] user error: unbound logic variable g_x in annotation. Can we mention in function contract, variables that will be defined locally in the function itself? pl -- Pierre-Lo?c Garoche Research Scientist @ ONERA pierre-loic.garoche at onera.fr - pierre-loic-garoche at uiowa.edu http://www.onera.fr/staff/pierre-loic-garoche/ -------------- next part -------------- A non-text attachment was scrubbed... Name: signature.asc Type: application/pgp-signature Size: 198 bytes Desc: Digital signature URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130809/5de977e7/attachment-0001.pgp>