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 14:39:31 +0200
  • In-reply-to: <20130809115707.GA5703@damazan>
  • References: <20130809093949.GA5295@damazan> <CA+yPOVjex===_cvHJEiYMRs=NSxXfevLxjgeyaAF3NObhxej6A@mail.gmail.com> <20130809115707.GA5703@damazan>
2013/8/9 Pierre-Lo?c Garoche <Pierre-Loic.Garoche at onera.fr>:

>
> Will additional requires/ensures clauses about the state of this global variable be the best way to handle this ?

If you're using WP, yes, you'll have to add requires to describe the
pre-state of in which your function is supposed to be called.

> 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) */;

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile