[klee-dev] 'Cannot find linker input' reproducing coreutils experiment

[Pablo González de Aledo]

Installing the last version from https://github.com/ccadar/klee it works
better, but I still get the following warnings

mint at mint ~/coreutils-6.11/obj-llvm/src $ klee --libc=uclibc
--posix-runtime ./cat.bc --version
KLEE: NOTE: Using model:
/llvm-2.9/klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca
KLEE: output directory = "klee-out-4"
KLEE: WARNING ONCE: function "vasnprintf" has inline asm
KLEE: WARNING: undefined reference to function: __ctype_b_loc
KLEE: WARNING: undefined reference to function: __xstat64
KLEE: WARNING: undefined reference to function: signbitl
KLEE: WARNING: executable has module level assembly (ignoring)
KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 56353760)
KLEE: WARNING ONCE: calling __user_main with extra arguments.
KLEE: WARNING ONCE: calling external: __xstat64(1, 56242880, 56514336)
KLEE: WARNING ONCE: calling external: getpagesize()
KLEE: WARNING ONCE: calling external: vprintf(56141712, 56544832)
cat (GNU coreutils) 6.11

License GPLv3+: GNU GPL version 3 or later <http://gnu.org/licenses/gpl.html
>
This is free software: you are free to change and redistribute it.
There is NO WARRANTY, to the extent permitted by law.

Written by Torbjorn Granlund and Richard M. Stallman.
KLEE: WARNING ONCE: calling close_stdout with extra arguments.
Copyright (C) 2008 Free Software Foundation, Inc.
KLEE: done: total instructions = 29255
KLEE: done: completed paths = 1
KLEE: done: generated tests = 1

Are they really warnings, or are they a real problem?. I suppose klee can
not propagate the symbolic values through functions that are undefined.

Thanks.


2013/11/11 Daniel Liew <daniel.liew at imperial.ac.uk>

> > The most similar file to the file asked in my installation is
> > /llvm-2.9/klee/Release+Asserts/lib/libkleeRuntimePOSIX.a. Can I "ln -s"
> this
> > file to the file asked without worries?.
>
> No you **cannot** symlink libkleeRunTimePOSIX.bca to
> libkleeRunTimePOSIX.a they are in two completely different formats.
> The *.bca files are LLVM bitcode archives and *.a files are archives
> of native binary objects.
>
> Can you run?
>
> $ cd /llvm-2.9/klee
> $ find . -iname '*.bca'
>
> if your runtime is building correctly it maybe that the files are
> ending up in a different folder (e.g. "Release" instead of
> "Release+Asserts" which might of happened if you used the
> --with-runtime= argument at configure time).
>
> Can you also confirm that you are running the latest upstream KLEE
> from GitHub ( https://github.com/ccadar/klee )?
>
> Thanks,
> Dan.
>
-------------- next part --------------
HTML attachment scrubbed and removed