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: lindenmm at informatik.uni-freiburg.de (Markus Lindenmann)
  • Date: Wed, 7 Dec 2011 20:30:48 +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>
Hi Claude,


> 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.

Thanks, we are as well :)

> 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 ???

That would be possible, but we try to put it into Eclipse CDT and we are
therefore
(more or less) bound to Java. We consider using the Eclipse CDT C-Parser and
extend it for our needs. However, we are not yet sure if this is possible at
all,
or if we have to go other ways.


Best regards,
Markus