--- layout: fc_discuss_archives title: Message 16 from Frama-C-discuss on October 2017 ---
Hello, 2017-10-31 16:59 GMT+01:00 Ziqing Luo <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 Items marked in red are not supported or only partially supported. Best regards, -- E tutto per oggi, a la prossima volta Virgile -------------- section suivante -------------- Une pièce jointe HTML a été nettoyée... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20171031/80f43d1a/attachment.html>