--- layout: fc_discuss_archives title: Message 37 from Frama-C-discuss on November 2009 ---
Hello, Frama-C can be used on programs containing calls to library functions also known as leaf functions in some parts of the manuals, i.e. function prototypes without an associated body. Functions from the C standard library are not special in this respect, except that the headers provided by compilers such as gcc tend to rely on their own built-in functions which renders them difficult to parse with Frama-C. In addition, depending on the kind of properties you want to establish on your program, you may need to provide some specification, or an implementation for these functions. This is already the case for a few functions in the share/frama-c directory of your installation, mostly under the form of an implementation, for use with the value analysis plugin. A project with our colleagues at Fraunhofer FIRST has started in September on this topic (http://www.first.fraunhofer.de/owx_1_4951_2_2_0_2f0471d9a8fbdc.html), so that you can expect to see standard specifications in some future release of Frama-C. More specifically, a certain number of math functions have an ACSL built-in counterpart (operating over the real type of mathematical reals), which you can use in your specifications. In particular, you have access to a \cos and a \sin function. Best regards, -- Virgile Prevosto Ing?nieur-Chercheur CEA, LIST, Laboratoire des logiciels s?rs -------- Message d'origine-------- De: frama-c-discuss-bounces at lists.gforge.inria.fr de la part de nam nam Date: sam. 14/11/2009 16:55 ?: frama-c-discuss at lists.gforge.inria.fr Objet : [Frama-c-discuss] using library function in frama-C Hi all I am working with Frama C to verify some programs. But I have a question. Does Frama C suppose using function that are in library to verify program especially for float-return function? For example, in my program I have to call cos or sin function, how can I verify this program? Thank you Nam -------------- section suivante -------------- Une pi?ce jointe non texte a ?t? nettoy?e... Nom: non disponible Type: application/ms-tnef Taille: 3889 octets Desc: non disponible Url: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20091115/6a427751/attachment.bin