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: Claude.Marche at inria.fr (Claude Marche)
  • Date: Wed, 07 Dec 2011 15:16:24 +0100
  • In-reply-to: <000701ccb10f$38f61960$aae24c20$@informatik.uni-freiburg.de>
  • References: <000901ccb0fb$6411f4c0$2c35de40$@informatik.uni-freiburg.de> <000701ccb10f$38f61960$aae24c20$@informatik.uni-freiburg.de>
Hi,

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

- Claude

On 02/12/2011 17:27, Markus Lindenmann wrote:
> Hi everyone,
>
> We are trying to implement a translator from C+ACSL to Boogie at our
> University. However, we ran into some questions where we think, Frama-C
> has already solved them.
>
> The first one: Is there a complete grammar for ACSL available? Because
> the one we found (e.g. http://frama-c.com/download/acsl.pdf but also in
> other documents) is splitted over multiple pages and seems to have some
> inconsistencies ? i.e. some term are not defined at all (e.g.
> ?/ghost-statement/?, ) or the definition is split-up (e.g. ?/statement?
> /? does this mean, ?/statement?/ is the union of all definitions, or
> does it refer to different/?/statements?).
>
> In addition we would like to put the grammar in a parser generator (e.g.
> JavaCup) ? is this already available and if so, where and for which
> parser generator?
>
> Finally we try to write a C+ACSL AST and we were looking if the one from
> Frama-C ? because it is tested and sophisticated ? is documented
> somewhere. If so, is this documentation publicly available?
>
> Thanks in advance and have a nice weekend,
>
> Markus
>
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss