[klee-dev] KLEE: ERROR: Loading file /usr/local/lib/klee/runtime/klee-uclibc.bca failed: Invalid record

Biqian Cheng bchen158 at ucr.edu
Tue Aug 9 02:24:27 BST 2022


Hi Frank,

Did you rebuild it (make) in case it was wrong beforehand?


Yes, I tried to use "cmake -DENABLE_POSIX_RUNTIME=ON
-DENABLE_KLEE_UCLIBC=ON -DKLEE_UCLIBC_PATH=/home/klee-uclibc .." then "make
-j2" to rebuild it.

Then check the LLVM version klee is linked against (e.g. ldd
> <path>/bin/klee)


I used "ldd /usr/local/bin/klee", it gives me:

linux-vdso.so.1 (0x00007fff2cba9000)
libsqlite3.so.0 => /lib/x86_64-linux-gnu/libsqlite3.so.0
(0x00007f1841e90000)
libz3.so.4 => /lib/x86_64-linux-gnu/libz3.so.4 (0x00007f18408f0000)
libz.so.1 => /lib/x86_64-linux-gnu/libz.so.1 (0x00007f18408d4000)
libtcmalloc.so.4 => /lib/x86_64-linux-gnu/libtcmalloc.so.4
(0x00007f18406dd000)
libLLVM-10.so.1 => /usr/lib/llvm-10/lib/libLLVM-10.so.1 (0x00007f183c049000)
libstdc++.so.6 => /lib/x86_64-linux-gnu/libstdc++.so.6 (0x00007f183be67000)
libm.so.6 => /lib/x86_64-linux-gnu/libm.so.6 (0x00007f183bd16000)
libc.so.6 => /lib/x86_64-linux-gnu/libc.so.6 (0x00007f183bb24000)
libpthread.so.0 => /lib/x86_64-linux-gnu/libpthread.so.0
(0x00007f183bb01000)
libdl.so.2 => /lib/x86_64-linux-gnu/libdl.so.2 (0x00007f183bafb000)
libgcc_s.so.1 => /lib/x86_64-linux-gnu/libgcc_s.so.1 (0x00007f183bae0000)
/lib64/ld-linux-x86-64.so.2 (0x00007f1842332000)
libunwind.so.8 => /lib/x86_64-linux-gnu/libunwind.so.8 (0x00007f183bac3000)
libffi.so.7 => /lib/x86_64-linux-gnu/libffi.so.7 (0x00007f183bab5000)
libedit.so.2 => /lib/x86_64-linux-gnu/libedit.so.2 (0x00007f183ba7d000)
librt.so.1 => /lib/x86_64-linux-gnu/librt.so.1 (0x00007f183ba73000)
libtinfo.so.6 => /lib/x86_64-linux-gnu/libtinfo.so.6 (0x00007f183ba43000)
liblzma.so.5 => /lib/x86_64-linux-gnu/liblzma.so.5 (0x00007f183ba1a000)
libbsd.so.0 => /lib/x86_64-linux-gnu/libbsd.so.0 (0x00007f183b9fe000)

Is this indicating I'm using LLVM-10, while I'm supposed to use LLVM-11?

and finally the build output of your program.bc (enable verbose mode for
> make/...).


Does this mean make -j2?


> Does klee complain without "--libc=uclibc"?


No, when I deleted "--libc=uclibc". The issue disappears.

Thank you for your help!

--Biqian


On Mon, Aug 8, 2022 at 1:30 PM Frank Busse <f.busse at imperial.ac.uk> wrote:

> Hi,
>
>
> On Mon, 8 Aug 2022 13:18:54 -0700
> Biqian Cheng <bchen158 at ucr.edu> wrote:
>
> > Thanks for your reply. I typed this command as you suggested
> > previously: ./configure --make-llvm-lib --with-cc clang-11
> > --with-llvm-config llvm-config-11
> >
> > Here are what I got after typing that command:
>
> Looks good. Did you rebuild it (make) in case it was wrong beforehand?
> Then check the LLVM version klee is linked against (e.g. ldd
> <path>/bin/klee) and finally the build output of your program.bc
> (enable verbose mode for make/...). Does klee complain
> without "--libc=uclibc"?
>
> > libllvm10/focal,now 1:10.0.0-4ubuntu1 amd64 [installed,automatic]
>
> Given that LLVM10 is on your machine as well I think we're on the right
> path. ;)
>
>
> Kind regards,
>
> Frank
>
-------------- next part --------------
HTML attachment scrubbed and removed


More information about the klee-dev mailing list