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: virgile.prevosto at cea.fr (Virgile Prevosto)
  • Date: Mon, 05 Dec 2011 09:34:36 +0100
  • In-reply-to: <CAC3Lx=Zg1ecz8OM_dBd55EkPyCm7OPtSwAiz0KC0b7v_tLuXDQ@mail.gmail.com>
  • References: <000901ccb0fb$6411f4c0$2c35de40$@informatik.uni-freiburg.de> <000701ccb10f$38f61960$aae24c20$@informatik.uni-freiburg.de> <CAC3Lx=Zg1ecz8OM_dBd55EkPyCm7OPtSwAiz0KC0b7v_tLuXDQ@mail.gmail.com>
Hello,

On 02/12/2011 17:52, David MENTRE wrote:

> 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?).
>>

You're right. I have to admit that support for ghost code is pretty weak 
for now. Namely Frama-C will only accept ghost code that is identical to 
C code except for being enclosed in /*@ ghost ... */ or //@ ghost ... 
\n. This might explain why grammar for ghost code did not get reviewed 
very thoroughly until now.

>
> 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.

To complete David's answer, cparser.mly is the parser for C. It will 
also "handle" ghost code but relies on auxiliary lexer and parser for 
all other ACSL annotations. These are located in 
cil/src/logic/logic_lexer.mll and cil/src/logic/logic_parser.mly 
respectively (+ cil/src/logic/logic_preprocess.mll that takes care of 
having ACSL annotations pre-processed when -pp-annot is on).

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile