--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on November 2009 ---
>> 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