--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on November 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] ask for slicing spec



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