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] 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 |