[klee-dev] math.h functions interpreted as external
juanfrancisco.garcia
juanfrancisco.garcia at imdea.org
Thu Jan 7 10:26:24 GMT 2021
I'm getting this warnings for all math.h functions,
KLEE: WARNING ONCE: calling external: floor(9221120237041090560)
KLEE: WARNING ONCE: calling external: round(0)
math.h is included, and if I change libc to uclibc I also get this
warnings:
KLEE: WARNING: undefined reference to function: acos
KLEE: WARNING: undefined reference to function: atan2
KLEE: WARNING: undefined reference to function: ceil
KLEE: WARNING: undefined reference to function: cos
KLEE: WARNING: undefined reference to function: floor
KLEE: WARNING: undefined reference to function: round
KLEE: WARNING: undefined reference to function: sin
KLEE: WARNING: undefined reference to function: sqrt
Are math.h functions supported in klee?
I also tried with z3 solver that supports floating point, and it gives
the same warnings.
Thanks in advance,
Juan Francisco García
More information about the klee-dev
mailing list