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



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>