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



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>