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

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