Hi, instead of debugging this on the mailing list, I think it would be
better to open an issue on GitHub.
Thanks,
Cristian
On 12/02/14 15:42, ThanhVu (Vu) Nguyen wrote:
The LLVM2.9 bin path is in my PATH. But it *does not* have clang++ or
clang as shown below. The original klee repo configure script
apparently does not check (and use?) clang* that's why I didn't get
such errors before.
prime Wed Feb 12:08:35:58 (4270)
~/Src/Devel/KLEE/llvm-gcc4.2-2.9-x86_64-linux/bin
$ ls
llvm-c++* x86_64-unknown-linux-gnu-cpp-4.2.1*
llvm-cpp* x86_64-unknown-linux-gnu-gcc-4.2.1*
llvm-g++* x86_64-unknown-linux-gnu-llvm-c++*
llvm-gcc* x86_64-unknown-linux-gnu-llvm-cpp*
llvm-gccbug* x86_64-unknown-linux-gnu-llvm-g++*
llvm-gcov* x86_64-unknown-linux-gnu-llvm-gcc*
llvm-gfortran* x86_64-unknown-linux-gnu-llvm-gfortran*
Vu,
On Wed, Feb 12, 2014 at 8:34 AM, Daniel Liew <[email protected]
<mailto:[email protected]>> wrote:
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 <[email protected]
<mailto:[email protected]>> 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
<[email protected] <mailto:[email protected]>>
> 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
<[email protected] <mailto:[email protected]>>
>> wrote:
>>>
>>> git pull https://github.com/delcypher/klee.git
>>> feature_support_stp_with_boost
>>
>>
>>
>>
>> Vu,
>
>
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
