[klee-dev] Missing floor, modf and pow

[Alberto Barbaro]

Hi all,
few months ago I was trying to understand how to test pngpixel via KLEE and
after few suggestion I was able to do it.

I have just one more question. When I run KLEE I have this output:

klee at 0c7da896b087:~/targets/libpng-1.6.34/contrib/examples$ klee
--libc=uclibc --posix-runtime pngpixel.bc 1 1 file.png
KLEE: NOTE: Using klee-uclibc :
/home/klee/klee_build/klee/Release+Debug+Asserts/lib/klee-uclibc.bca
KLEE: NOTE: Using model:
/home/klee/klee_build/klee/Release+Debug+Asserts/lib/libkleeRuntimePOSIX.bca
KLEE: output directory is
"/home/klee/targets/libpng-1.6.34/contrib/examples/klee-out-3"
KLEE: Using STP solver backend
KLEE: WARNING: undefined reference to function: floor
KLEE: WARNING: undefined reference to function: modf
KLEE: WARNING: undefined reference to function: pow
KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 92453184) at
/home/klee/klee_src/runtime/POSIX/fd.c:1044
KLEE: WARNING ONCE: calling __user_main with extra arguments.
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled.
Using alignment of 8.
KLEE: WARNING ONCE: _setjmp: ignoring

KLEE: done: total instructions = 106954
KLEE: done: completed paths = 1
KLEE: done: generated tests = 1
klee at 0c7da896b087:~/targets/libpng-1.6.34/contrib/examples$

Can I "ignore" the fact that floor, modf and pow are missing because I'm
using uclibc?

Thanks
-------------- next part --------------
HTML attachment scrubbed and removed