--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on August 2013 ---
2013/8/9 Pierre-Lo?c Garoche <Pierre-Loic.Garoche at onera.fr>: > > 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: Of course, since it is based on the false assumption that ghost formals are supported ;-) > 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? > No, as they do not exist outside of the function (neither in pre-, nor in post-state). Besides, a local variable must be initialized locally, it's very different from a formal instantiated by the caller. Best regards, -- E tutto per oggi, a la prossima volta Virgile