[klee-dev] Missing floor, modf and pow

[Alberto Barbaro]

Thanks Dan,
all clear now.

Thanks again

2018-03-03 21:23 GMT+00:00 Dan Liew <dan at su-root.co.uk>:

> Hi,
>
> On 3 March 2018 at 07:29, Alberto Barbaro <barbaro.alberto at gmail.com>
> 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 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?
>
> 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
>
-------------- next part --------------
HTML attachment scrubbed and removed