--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on December 2011 ---
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