--- layout: fc_discuss_archives title: Message 22 from Frama-C-discuss on December 2011 ---
Hi, On the one hand, I think that implementing a C verifier for C+ACSL programs using Boogie is a great idea, and I'm looking forward to the outcome of this project. On the other hand, I think that implementing a parser for C+ACSL is a very bad idea. The Frama-C kernel is already there for that task, and it is a *huge* task. So why not just implementing your translator as a Frama-C plugin ??? - Claude On 02/12/2011 17:27, Markus Lindenmann wrote: > 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 > > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss