Re: [klee-dev] Testing coreutils: Invalid record

[felicia]

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  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

Re: [klee-dev] Testing coreutils: Invalid record

[Dan Liew]

On 28 December 2015 at 05:35, felicia  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