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