--- layout: fc_discuss_archives title: Message 8 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>:

>
> 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