--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on November 2009 ---
Thanks for your response. I think my question is well answered. On Fri, Nov 6, 2009 at 11:58 AM, CUOQ Pascal <Pascal.CUOQ at cea.fr> wrote: > > >> This seems to be > >> impossible because frama-c changes the CIL API to some extent. Am I > >> correct? > > > >One of the goals of Frama-C is to provide a library for developing new > >analyzers. But you're correct: Frama-C comes with its own version of CIL > >which is not compatible with the official Berkeley's version of CIL. > > Specifically, we needed to change CIL neither because there is anything > wrong with it, nor because we like gratuitously forking existing > projects, but because we needed to add support for ACSL annotations > and also because some of CIL transformations, which can remove bugs, > were fine in the context of a transformer of correct programs but > were not acceptable in the context of a collection of correct static > analyzers. The philosophy for the latter transformations is to > keep them but insert in the AST enough information to determine > at analysis time if there was a bug in the original code. > > Pascal > > _______________________________________________ > 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 > -- Regards, Jun -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20091106/63cef155/attachment.htm