Hi Dan,
Thank you for the earlier reply. I think the LLVM should be match
because I just use one version of LLVM, which is LLVM-3.4. (I also use
coreutils version 6.11)
I redo the process again, and somehow got different result.
So, when I execute this:
~/git/original/klee/Release+Asserts/bin/klee --libc=uclibc
--posix-runtime ./echo.bc --sym-arg 3
The error shows like this:
KLEE: ERROR: Link with library
/home/felicia/git/original/klee/Release+Asserts/lib/klee-uclibc.bca
failed: Invalid bitcode signatureLoading module failed : Invalid bitcode
signature
If I removed the --libc=uclibc, the result would be:
..
..
LEE: WARNING: undefined reference to function: error (UNSAFE)!
KLEE: WARNING ONCE: calling external: syscall(4, 36044240, 36139248)
KLEE: WARNING ONCE: calling external: getenv(35986432)
KLEE: WARNING ONCE: calling external: setlocale(6, 35987552)
KLEE: ERROR:
/home/felicia/coreutils-6.11/obj-llvm/src/../../src/echo.c:138: external
modified read-only object
KLEE: NOTE: now ignoring this error at this location
KLEE: done: total instructions = 706
KLEE: done: completed paths = 1
KLEE: done: generated tests = 1
Do you have any recommendation regarding uclibc.bca error? Thank you
very much.
On 2015-12-29 13:29, Dan Liew wrote:
On 28 December 2015 at 05:35, felicia <feli...@comp.nus.edu.sg> wrote:
I followed the instruction on
https://klee.github.io/tutorials/testing-coreutils/
I would like to run coreutils by using KLEE latest version and LLVM
3.4
Since, I use clang instead of llvm-gcc. In the step 2, I use clang to
build
coreutils with these commands below:
../configure --disable-nls CFLAGS="-g"
export LLVM_COMPILER=clang
make CC=/home/felicia/whole-program-llvm-master/wllvm
make -C src arch hostname
CC=/home/felicia/whole-program-llvm-master/wllvm
However when I proceed to step 3: Using KLEE as Interpreter by
execute:
~/full-path-to KLEE/Release+Asserts/bin/klee --libc=uclibc
--posix-runtime
./cat.bc --version,
the output is KLEE: ERROR: error loading program './cat.bc': Invalid
record
Am I missing something? Thank you very much.
That error likely means something is wrong with the LLVM bitcode you
are feeding to KLEE. One possible cause is that the version of LLVM
that your clang was compiled against does not match the version that
you built KLEE with. The LLVM bitcode format changes over time so to
have things work correctly you should use the version of Clang the the
KLEE build system uses to compile its own runtime library.
HTH,
Dan.
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
