Hi Juan,
The warnings say that no implementation for these functions is
available. You should compile uclibc with support for these functions.
However, note that mainline KLEE does not have support for symbolic
floating point operations, but there are a couple of (open-source but
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:
