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