Hi, On 3 March 2018 at 07:29, Alberto Barbaro <[email protected]> wrote: > 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?
You can ignore the warning as long as the code you run doesn't call these with symbolic arguments. You'll see a warning if this happens because KLEE has to concretize the arguments and call the function via LLVM's JIT. In your case it doesn't look like you're passing any symbolic data to the application so you're running concretely so you should be fine. If any function gets called that's external (i.e. is not in the LLVM bitcode, like floor is in your example) KLEE will emit a message telling you its calling an external. The reason these functions aren't available is because KLEE doesn't link in Uclibc's C library. My fork of KLEE that supports symbolic floating-point arithmetic [1] does link this library. [1] https://github.com/srg-imperial/klee-float _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
