--- layout: fc_discuss_archives title: Message 97 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130913/c4dfbd4d/attachment.html>