--- layout: fc_discuss_archives title: Message 61 from Frama-C-discuss on October 2010 ---
Hi everyone, I'm using Frama-C Boron, in particularly the Jessie plug-in. I have a question regarding logic types. I have the following axiomatic definition: /*@ axiomatic list_of_ints{ @ type int_list; @ logic int_list null; @ logic int_list cons(int n, int_list s); @ logic int_list concat(int_list s1, int_list s2); @ axiom concat_nil_right: @ \forall int_list s; concat(s,null) == s; @ axiom concat_nil_left: @ \forall int_list s; concat(null,s) == s; @ axiom concat_cons: @ \forall int b, int_list s1,s2; @ concat(cons(b,s1),s2) == cons(b,concat(s1,s2)); @ } @*/ And I would like to declare ghost variables of type int_list; (or other type of variables, but I want to be able to use them -- and also the associated logic functions -- in the ghost code) But it raises a syntax error when I include the declaration: //@ ghost int_list ghost_a = null; My question is: can we declare variables of a logic type in ACSL? How? Can that variables be declared inside the ghost code? Thanks for your help. Best regards, B?rbara Vieira -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20101020/e5f3cbe6/attachment.htm>