--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on August 2013 ---
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