--- layout: fc_discuss_archives title: Message 102 from Frama-C-discuss on September 2013 ---
> > 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>