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] ACSL Parsing

  • Subject: [Frama-c-discuss] ACSL Parsing
  • From: lindenmm at informatik.uni-freiburg.de (Markus Lindenmann)
  • Date: Fri, 2 Dec 2011 17:27:01 +0100
  • In-reply-to: <000901ccb0fb$6411f4c0$2c35de40$@informatik.uni-freiburg.de>
  • References: <000901ccb0fb$6411f4c0$2c35de40$@informatik.uni-freiburg.de>
Hi everyone,

 

 

We are trying to implement a translator from C+ACSL to Boogie at our
University. However, we ran into some questions where we think, Frama-C has
already solved them.

 

The first one: Is there a complete grammar for ACSL available? Because the
one we found (e.g. http://frama-c.com/download/acsl.pdf but also in other
documents) is splitted over multiple pages and seems to have some
inconsistencies - i.e. some term are not defined at all (e.g.
'ghost-statement', ) or the definition is split-up (e.g. 'statement' - does
this mean, 'statement' is the union of all definitions, or does it refer to
different 'statements').

In addition we would like to put  the grammar in a parser generator (e.g.
JavaCup) - is this already available and if so, where and for which parser
generator?

 

Finally we try to write a C+ACSL AST and we were looking if the one from
Frama-C - because it is tested and sophisticated -  is documented somewhere.
If so, is this documentation publicly available?

 

 

Thanks in advance and have a nice weekend,

Markus

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20111202/abc1b818/attachment.htm>