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