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

[Daniel Liew]

Hi Vu,

First of all it's great to hear another Arch Linux user is trying out KLEE :)

On 12 February 2014 02:12, ThanhVu (Vu) Nguyen <tnguyen at cs.unm.edu> wrote:
> Hi,
>
> I try to build Klee using the instruction from this page
> http://ccadar.github.io/klee/GetStarted.html .  I was not able to build
> stp-r940.tgz, after doing "make OPTIMIZE=-O2 CFLAGS_M32= install" ,  I get
> error about AssertsQuery not declared in scope (see [1]).

Yes I saw this issue several months ago. I fixed it upstream [1].

> So I try the
> latest version of stp as suggested from this message
> http://www.mail-archive.com/klee-dev@imperial.ac.uk/msg01315.html .  I was
> able to build this stp version fine with the make command  "make CFLAGS_M32=
> -j2".

Just to note if you're using the upstream STP which uses CMake you
don't need the CFLAGS_M32 flag. That
flag was a disgusting hack for the old build system in STP.

> Next, after building klee-uclibc and get to step 6 configure KLEE,  after
> issuing the command
>
>  ./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-runtime,
>
> I get the error about -lstp as below
>
> checking for stp/c_interface.h... yes
> checking for vc_setInterfaceFlags in -lstp... no
> configure: error: Unable to link with libstp

This is my fault. I recently changed [2] how ``libstp.a`` is built in
STP so that it now depends on the Boost libraries. I have a pull
request [3] to fix this in KLEE but I have not yet merged it yet
because I have not tested how this impacts the meta-SMT build of KLEE.
It sounds like you're only using STP so it should be fine to merge my
pull request into your local branch. To get the pull request you could
do something like this...

$ cd /path/to/klee/git/repo
$ git checkout -b delcypher-feature_support_stp_with_boost master
$ git pull git at github.com:delcypher/klee.git feature_support_stp_with_boost

After doing this if you try to reconfigure hopefully things will work.
Please let me know how you get on.

Thanks,
Dan


[1] https://github.com/stp/stp/commit/ece1a55fb367bd905078baca38476e35b4df06c3
[2] https://github.com/stp/stp/pull/70
[3] https://github.com/ccadar/klee/pull/99