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@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@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
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
