Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] Logic types and Ghost code
  • From: barbaraisabelvieira at gmail.com (Barbara Vieira)
  • Date: Wed, 20 Oct 2010 11:13:32 +0100
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>