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

[Frama-c-discuss] ACSL Parsing



Hello,

2011/12/2 Markus Lindenmann <lindenmm at informatik.uni-freiburg.de>:
> 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?

The answer at both of your questions is probably to look at the C+ACSL
parser in Frama-C source code. It is derived from CIL and written
using ocamllex and ocamlyacc tools.

Look at files :
  frama-c-Nitrogen-20111001\cil\src\frontc\cparser.mly (grammar)
  frama-c-Nitrogen-20111001\cil\src\frontc\clexer.mll (lexer)

In cparser.mly, description of statements start at line 875.

Sincerely yours,
david