--- layout: fc_discuss_archives title: Message 102 from Frama-C-discuss on September 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] "Re: How to ignore Incompatible declarations without emitting errors?"



>
> Hello David,
> Frama-C headers are meant to be used with Frama-C's analyzers as a way of
> making the analyses work. Some might contain calls to Frama-C specific
> directives, some might only be a function declaration with an ACSL
> annotation specifying its behavior, ... The goal here is mostly to find a
> way to make the analyzers understand the behavior of a given function of a
> C standard library.
> They are not meant as a replacement standard library for a C compiler.
> In any case, you should not use them to compile your programs. What David
> suggested is (I think -- David, correct me if I misrepresent your advice)
> that you should probably have a specific version of your program using
> Frama-C C headers (and possibly annotated version of other headers you deem
> relevant to your program) tailored to the analysis you want to make.
> Cheers,
> --
> Richard Bonichon



Dear Richard,

Thanks very much for providing me such detailed answers.

It's helpful.

best regards,
David Yang
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130915/110376bc/attachment.html>