--- layout: fc_discuss_archives title: Message 38 from Frama-C-discuss on November 2009 ---
nam nam wrote: > 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? > Hi, In addition to Virgile's answer: for the specific case of floating-point operations, you may have a look at recent additions made to Frama-C and its Jessie plugin, that were developed within the Hisseo project: http://hisseo.saclay.inria.fr/documents.html See in particular "Behavioral Properties of Floating-Point Programs" <http://hisseo.saclay.inria.fr/ayad09.pdf> If you are OK to ignore issues related to FP rounding, and thus if you are willing to first prove your program in a ideal model were FP operations behave like if they were computed in real numbers, then you can just specify cosine as //@ ensures \result == \cos(x); double cos(double x); If, on the other hand, you want to take FP rounding into account, you will have to specify cosine with something like /*@ requires \abs(x) <= some constant; @ ensures \abs(\result - \cos(x)) <= some constant; @*/ double cos(double x); Again, look at reference above for more details. - Claude -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | mobile: +33 6 33 14 57 93 Parc Orsay Universit? | fax: +33 1 74 85 42 29 4, rue Jacques Monod - B?timent N | http://www.lri.fr/~marche/ F-91893 ORSAY Cedex |