--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on August 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] ACSL, globals and ghosts



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