--- layout: fc_discuss_archives title: Message 61 from Frama-C-discuss on October 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Logic types and Ghost code



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>