--- layout: fc_discuss_archives title: Message 24 from Frama-C-discuss on December 2011 ---
Hello, On 12/07/2011 03:16 PM, Claude Marche wrote: > 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 ??? I fully agree with Claude: implementing a C+ACSL parser is *huge*: both for the amount of implementation work that is required and for the difficulty of this task which is very error-prone. For Frama-C, we did not do such a work from scratch but we reused the pre-existing Cil parser (http://cil.sourceforge.net). To answer to one of the primary questions, the C+ACSL Frama-C's AST is fully documented in file cil/src/cil_types.mli which is available in the last open-source release (http://frama-c.com/download.html). Writing a framac2boogie translator as a Frama-C plug-in should be much easier than writing again a C+ACSL parser from scratch. Hope this helps, Julien