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] Specification of libm functions [was: Re: [Coq-Club] Problem with Gappa installation]
- Subject: [Frama-c-discuss] Specification of libm functions [was: Re: [Coq-Club] Problem with Gappa installation]
- From: guillaume.melquiond at inria.fr (Guillaume Melquiond)
- Date: Tue, 28 Sep 2010 12:11:14 +0200
- In-reply-to: <581470873.2965180.1285578065239.JavaMail.firstname.lastname@example.org>
- References: <581470873.2965180.1285578065239.JavaMail.email@example.com>
This discussion has gone way out of the scope of the coq-club mailing list. So I'm moving it to the frama-c list. Please remove the coq-club CC from further emails. I'm still sending this one to coq-club, so that the original email doesn't seem unanswered to. Le lundi 27 septembre 2010 ? 11:01 +0200, Michael a ?crit : > No that everything seems to work fine, I have another short question (just to > make sure it's not a problem of something missing that should actually already > be there): I included math.h in my C source code, and calculated sqrt of some > double value, which resulted in the coq proof in a variable of which nothing is > known. I then had a look at /usr/local/share/frama-c/libc/math.h. For some > functions (such as acos, asin) there are ACSL-annotations, however there is > nothing for sqrt. > > Are there > a) some annotations on how the C square root behaves anywhere, and I just > missed them, or > b) do I have to give specifications on my own, and take them as admitted I don't think there are any specification for the square root yet, so you will have to craft your own. I guess something like the following would work. It is untested both syntactically and from a specification point of view. /*@ behavior normal: assumes \is_finite(x) && x >= 0; assigns \nothing; ensures \is_finite(\result) && \abs(\result - \sqrt(x)) <= 0x1p-53 * \abs(\sqrt(x)); behavior infinite: assumes \is_plus_infinity(x); assigns \nothing; ensures \is_plus_infinity(\result); behavior edom: assumes \is_minus_infinity(x) || (\is_finite(x) && x < 0); assigns __FC_errno; ensures __FC_errno == 1; disjoint behaviors normal, infinite, edom; */ double sqrt(double x); Perhaps someone else can suggest a better specification. Best regards, Guillaume PS: the \abs(\sqrt(x)) expression is a bit overkill but it should make Gappa happy.
- Prev by Date: [Frama-c-discuss] make error for "Hello Frama-C World" plugin
- Next by Date: [Frama-c-discuss] Binary search now works with Alt-Ergo 0.92
- Previous by thread: [Frama-c-discuss] make error for "Hello Frama-C World" plugin
- Next by thread: [Frama-c-discuss] Binary search now works with Alt-Ergo 0.92