Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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