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.root@zmbs3.inria.fr>
  • References: <581470873.2965180.1285578065239.JavaMail.root@zmbs3.inria.fr>
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.