--- layout: fc_discuss_archives title: Message 33 from Frama-C-discuss on December 2011 ---
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