Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] ACSL, globals and ghosts
  • From: virgile.prevosto at m4x.org (Virgile Prevosto)
  • Date: Fri, 9 Aug 2013 15:00:06 +0200
  • In-reply-to: <20130809124455.GB30145@damazan>
  • References: <20130809093949.GA5295@damazan> <CA+yPOVjex===_cvHJEiYMRs=NSxXfevLxjgeyaAF3NObhxej6A@mail.gmail.com> <20130809115707.GA5703@damazan> <CA+yPOVjjJYOVZp=GgHNEEineMKRzTLbQ7hz1mNjRZv8ngGUD6Q@mail.gmail.com> <20130809124455.GB30145@damazan>
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