--- layout: fc_discuss_archives title: Message 50 from Frama-C-discuss on September 2010 ---
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.