[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