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: dmentre at linux-france.org (David MENTRE)
  • Date: Fri, 2 Dec 2011 17:52:29 +0100
  • In-reply-to: <000701ccb10f$38f61960$aae24c20$@informatik.uni-freiburg.de>
  • References: <000901ccb0fb$6411f4c0$2c35de40$@informatik.uni-freiburg.de> <000701ccb10f$38f61960$aae24c20$@informatik.uni-freiburg.de>
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