--- layout: fc_discuss_archives title: Message 33 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 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