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



> > 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>