Thanks Dan, all clear now. Thanks again
2018-03-03 21:23 GMT+00:00 Dan Liew <[email protected]>: > 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
