[klee-dev] Arch linux: Cannot build Klee , stuck with "Unable to link with libstp"

Daniel Liew daniel.liew at imperial.ac.uk
Wed Feb 12 15:34:28 GMT 2014


The new issue you are seeing now has nothing to do with STP. It is to
do with your LLVM bitcode compiler. LLVM Bitcode is not stable between
releases of LLVM (i.e. you cannot mix LLVM bitcode generated by
LLVM2.9 and LLVM3.3)

If see the configure output...

Using C llvm compiler : /usr/bin/clang
Using C++ llvm compiler : /usr/bin/clang++
checking C LLVM Bitcode compiler works...
/nfs/adaptive/tnguyen/Src/Devel/KLEE/llvm-2.9/Release+Asserts/bin/llvm-dis:
Unknown bitstream version!
configure: error: Failed converting LLVM Bitcode to LLVM assembly.
Maybe your LLVM versions do not match?

Configure is trying to use your system's clang as the LLVM bitcode
compiler (which is probably Clang 3.3 or 3.4, depending on when you
last ran ``pacman -Syuu``). This won't work (if you use LLVM2.9) and
configure rightly stops you from going any further. If you intend to
use LLVM2.9 with KLEE then you need to put the llvm-gcc [1] compiler
in your PATH before running KLEE's configure script.

[1] http://llvm.org/releases/2.9/llvm-gcc4.2-2.9-x86_64-linux.tar.bz2
or http://llvm.org/releases/2.9/llvm-gcc-4.2-2.9-i686-linux.tgz


Hope that helps.
Dan.

On 12 February 2014 15:15, ThanhVu (Vu) Nguyen <tnguyen at cs.unm.edu> wrote:
> Perhaps you can give me the latest repo of STP that are known to work on
> KLEE & Arch ?  I.e., the one that passes the libstp check .
>
> Vu,
>
>
> On Wed, Feb 12, 2014 at 8:08 AM, ThanhVu (Vu) Nguyen <tnguyen at cs.unm.edu>
> wrote:
>>
>> That seems to work ,  but now when running configure I get some other
>> checking error about LLVM Bitcode.  This check passed fine using the klee
>> original repo.  The LLVM2.9 was built as instructed from
>> http://ccadar.github.io/klee/GetStarted.html
>>
>>
>>  ./configure --with-llvm=/nfs/adaptive/tnguyen/Src/Devel/KLEE/llvm-2.9/
>> --with-stp=/nfs/adaptive/tnguyen/Src/Devel/KLEE/stp/binary-build/
>> --with-uclibc=/nfs/adaptive/tnguyen/Src/Devel/KLEE/klee-uclibc/
>> --enable-posix-runtimechecking build system type... x86_64-unknown-linux-gnu
>> checking host system type... x86_64-unknown-linux-gnu
>> checking target system type... x86_64-unknown-linux-gnu
>> checking type of operating system we're going to host on...
>> checking llvm source dir... /nfs/adaptive/tnguyen/Src/Devel/KLEE/llvm-2.9
>> checking llvm obj dir... /nfs/adaptive/tnguyen/Src/Devel/KLEE/llvm-2.9
>> checking llvm package version... 2.9
>> checking llvm version major... 2
>> checking llvm version minor... 9
>> checking llvm is release version... 1
>> checking llvm build mode... Release+Asserts
>> checking LLVM Bitcode compiler...
>> checking for llvm-gcc... NOT_FOUND
>>
>> checking for clang... FOUND
>> checking for clang++... FOUND
>> Using C llvm compiler : /usr/bin/clang
>> Using C++ llvm compiler : /usr/bin/clang++
>> checking C LLVM Bitcode compiler works...
>> /nfs/adaptive/tnguyen/Src/Devel/KLEE/llvm-2.9/Release+Asserts/bin/llvm-dis:
>> Unknown bitstream version!
>> configure: error: Failed converting LLVM Bitcode to LLVM assembly. Maybe
>> your LLVM versions do not match?
>>
>>
>>
>> On Wed, Feb 12, 2014 at 8:04 AM, Daniel Liew <daniel.liew at imperial.ac.uk>
>> wrote:
>>>
>>> git pull https://github.com/delcypher/klee.git
>>> feature_support_stp_with_boost
>>
>>
>>
>>
>> Vu,
>
>




More information about the klee-dev mailing list