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 14:44:55 +0200
  • In-reply-to: <CA+yPOVjjJYOVZp=GgHNEEineMKRzTLbQ7hz1mNjRZv8ngGUD6Q@mail.gmail.com>
  • References: <20130809093949.GA5295@damazan> <CA+yPOVjex===_cvHJEiYMRs=NSxXfevLxjgeyaAF3NObhxej6A@mail.gmail.com> <20130809115707.GA5703@damazan> <CA+yPOVjjJYOVZp=GgHNEEineMKRzTLbQ7hz1mNjRZv8ngGUD6Q@mail.gmail.com>
> > 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) */;

No, but it is a good idea to try. However, your code is not good for my frama-c. I added a body for the function, removed the parentheis around (int g_x) and added the semicolon:

/*@ requires x == g_x;
   requires g_x == 0;
   requires  y >= 0;
  ensures \result > x;
 */
int f(int y) {
/*@ ghost int g_x; */
return y +1;
}

ghost4.c:3:[kernel] user error: unbound logic variable g_x in annotation.

Can we mention in function contract, variables that will be defined locally in the function itself?

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/5de977e7/attachment-0001.pgp>