--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on November 2017 ---
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>