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

>> 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