--- layout: fc_discuss_archives title: Message 24 from Frama-C-discuss on December 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] ACSL Parsing



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