The Coq mailing list

[Michael<michaelschausten AT googlemail.com>]

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 (souch as acos, asin) there are ACSL-annotations, however there is
nothing for sqrt.

Are there
a) some annotations  on how the C suare root behaves anywhere, and I just
missed them, or
b) do I have to give specifications on my own, and take them as admitted


Sincerely,