--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on December 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] ACSL Parsing



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>