--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on August 2013 ---
Thanks Virgile a quick follow-up: > > How do global variables interact with contracts? When used in ensures, it seems > > that the global variable appear as a typed free variable. No knwoledge at all > > about its value, even when it is just a constant. For example, the following > > ensures is not proved automatically. > > > > int x = 0; > > > > /*@ requires y >= 0; > > @ ensures \result > x; > > @*/ > > int f(int y) { return y +1; } > > Well, we don't have any information about the value of x when entering > function f: it can very well be modified between initialization and > call site. Admittedly, if x was declared const int, it could be said > to be 0, but since this is can easily be defeated by a cast, we chose > not to rely on it in Frama-C. > On the other hand, if you explicitly say that f is the main entry > point of your program, then we know that in the pre-state x is 0, and > the ensures is easily discharged, as you can see with frama-c -wp > -main f file.c Will additional requires/ensures clauses about the state of this global variable be the best way to handle this ? Or is it available in the current implementation the addtional ghost parameters to functions ? Any example on how to use it? thx pl -- Pierre-Lo?c Garoche Research Scientist @ ONERA pierre-loic.garoche at onera.fr - pierre-loic-garoche at uiowa.edu http://www.onera.fr/staff/pierre-loic-garoche/ -------------- next part -------------- A non-text attachment was scrubbed... Name: signature.asc Type: application/pgp-signature Size: 198 bytes Desc: Digital signature URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130809/dc2b157d/attachment.pgp>