--- layout: fc_discuss_archives title: Message 15 from Frama-C-discuss on October 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 ?



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 ?

In addition, if WP supports that, does it support declare ghost variables
of user-defined logic types ?

Thank you,
Ziqing Luo
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20171031/7e5a1cab/attachment.html>