Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] ACSL Parsing

  • Subject: [Frama-c-discuss] ACSL Parsing
  • From: Julien.Signoles at cea.fr (Julien Signoles)
  • Date: Wed, 07 Dec 2011 15:36:01 +0100
  • In-reply-to: <4EDF7538.8080701@inria.fr>
  • References: <000901ccb0fb$6411f4c0$2c35de40$@informatik.uni-freiburg.de> <000701ccb10f$38f61960$aae24c20$@informatik.uni-freiburg.de> <4EDF7538.8080701@inria.fr>
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