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

[Frama-c-discuss] ACSL Parsing



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