Frama-C-discuss mailing list archives
This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Frama-c-discuss] RE : using library function in frama-C
- Subject: [Frama-c-discuss] RE : using library function in frama-C
- From: virgile.prevosto at cea.fr (PREVOSTO Virgile)
- Date: Sun, 15 Nov 2009 21:22:22 +0100
- References: <1f8a0c0a0911140755w7d158c4bj9ea865e33a81249a@mail.gmail.com>
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
- References:
- [Frama-c-discuss] using library function in frama-C
- From: doan.thanh.nam.1988 at gmail.com (nam nam)
- [Frama-c-discuss] using library function in frama-C
- Prev by Date: [Frama-c-discuss] using library function in frama-C
- Next by Date: [Frama-c-discuss] using library function in frama-C
- Previous by thread: [Frama-c-discuss] using library function in frama-C
- Next by thread: [Frama-c-discuss] using library function in frama-C
- Index(es):