--- layout: fc_discuss_archives title: Message 38 from Frama-C-discuss on November 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] using library function in frama-C



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 |