--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on December 2011 ---
Hi everyone, We are trying to implement a translator from C+ACSL to Boogie at our University. However, we ran into some questions where we think, Frama-C has already solved them. 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? Thanks in advance and have a nice weekend, Markus -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20111202/abc1b818/attachment.htm>