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: hollas at informatik.htw-dresden.de (Boris Hollas)
  • Date: Wed, 07 Dec 2011 21:00:20 +0100
  • In-reply-to: <02dc01ccb516$bbc50120$334f0360$@informatik.uni-freiburg.de>
  • References: <000901ccb0fb$6411f4c0$2c35de40$@informatik.uni-freiburg.de> <000701ccb10f$38f61960$aae24c20$@informatik.uni-freiburg.de> <4EDF7538.8080701@inria.fr> <02dc01ccb516$bbc50120$334f0360$@informatik.uni-freiburg.de>
On Wed, 2011-12-07 at 20:30 +0100, Markus Lindenmann wrote:

> 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

The problem with C is that it lacks precise semantics and has a lot of
dark and ugly corners. To translate C to BoogiePL you have to resolve
all of these issue, which has already been done in Cil and Frama-C. I
doubt the Eclipse C-Parser will help you here.
-- 
Best regards,
Boris


PS: Sorry that my previous post in German went here.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20111207/4ead1f3d/attachment.htm>