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: Pierre-Loic.Garoche at onera.fr (Pierre-Loïc Garoche)
  • Date: Fri, 9 Aug 2013 13:57:07 +0200
  • In-reply-to: <CA+yPOVjex===_cvHJEiYMRs=NSxXfevLxjgeyaAF3NObhxej6A@mail.gmail.com>
  • References: <20130809093949.GA5295@damazan> <CA+yPOVjex===_cvHJEiYMRs=NSxXfevLxjgeyaAF3NObhxej6A@mail.gmail.com>
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>