[klee-dev] Testing coreutils: Invalid record

[Dan Liew]

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