--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on November 2017 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Does WP support declare ghost variables of logic types ?



To complement virgile’s response, there is a known trick to implement ghost logic variables in Frama-C/ACSL.
You can declare a logic function with no formal parameters and one label-parameter to hold the value of your ghost variable.
This logic function is declared to read a fake ghost C variable to make it really depending on something that can be assigned during the execution of C code.

ghost int _world ; // Fake

axiomatic GhostVariable {

// Your logic variable is here:
logic integer a{L} reads _world ;

}


Then, in your ACSL annotations, you can write either `a{L}` or `\at(a,L)` to refer to the value of `a` at some program point `L`.
To update the value, simply call a (ghost) function that `assigns _world` to make the value of `a` really changed.
For instance :

//@ assigns _world ; ensures a == \old(a) + v ;
ghost void add_to_a(int v) ;

And here it is !
	L.


> Le 31 oct. 2017 à 17:39, Virgile Prevosto <virgile.prevosto at m4x.org> a écrit :
> 
> Hello,
> 
> 2017-10-31 16:59 GMT+01:00 Ziqing Luo <ziqing at udel.edu <mailto:ziqing at udel.edu>>:
> Dear Frama-C people,
> 
> I was trying to declare some ghost variables of logic types,  for example
> 
> int main() {
>   //@ ghost integer a = 0;
>   //@ assert a >= 0;
> }
> 
> Then I ran it with command "frame-c -wp test.c",  it told me that there is a syntax error at line 2 where is the ghost variable declaration.
> 
> If I change integer to int, there is no problem.  So I was wandering if WP supports declaring logic type ghost variables ?
> 
> 
> The issue is not in WP: there is no support for ghost variable with logic types in Frama-C's kernel itself. You can see what elements of ACSL are implemented in Frama-C's kernel (which does not mean that all plug-ins will be able to handle them) in the following document:  http://frama-c.com/download/acsl-implementation-Phosphorus-20170501.pdf <http://frama-c.com/download/acsl-implementation-Phosphorus-20170501.pdf> Items marked in red are not supported or only partially supported.
> 
> Best regards,
> -- 
> E tutto per oggi, a la prossima volta
> Virgile
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20171106/64d650a4/attachment.html>