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

[ThanhVu (Vu) Nguyen]

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]).  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".
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

As suggested from this msg
http://keeda.stanford.edu/pipermail/klee-dev/2012-October/000940.html ,  I
checked and verified the file lib/libstp.a etc are in the STP dir.  The
command  readelf -h lib/libstp.a gives something like
File: lib/libstp.a(SMTLIBPrinter.cpp.o)

                        ELF Header:
Class:                             ELF64
Data:                              2's complement, little endian
Version:                           1 (current)
Machine:                           Advanced Micro Devices X86-64
...

Note that I did build stp with CFLAGS_M32, i.e., make CFLAGS_M32=  -j2.


I was able to build KLEE with STP r940 just fine on Debian so it seems
there's some incompatibility problem among Arch Linux, Klee, and STP. I
would appreciate any suggestion on how to get Klee built on my  system.
 Thanks in advance.



---
Arch system info: uname -a
Linux prime 3.11.6-1-ARCH #1 SMP PREEMPT Fri Oct 18 23:22:36 CEST 2013
x86_64 GNU/Linux

[1] error when building stp-r940
CVC.y:1109.3-1114.1: warning: rule useless in parser due to conflicts
[-Wother]
 | Updates WITH_TOK '[' Expr ']' ASSIGN_TOK Expr
   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
flex -Cfe  -olexCVC.cpp -Pcvc CVC.lex
g++ -O2 -DCRYPTOMINISAT2 -I../../src/  -I../AST -DONLY_MSPACES -DMSPACES
-I../../src/sat/cryptominisat2/mtl -I../../src/sat/cryptominisat2
-DEXT_HASH_MAP -Wno-deprecated   -c -o lexCVC.o lexCVC.cpp
g++ -O2 -DCRYPTOMINISAT2 -I../../src/  -I../AST -DONLY_MSPACES -DMSPACES
-I../../src/sat/cryptominisat2/mtl -I../../src/sat/cryptominisat2
-DEXT_HASH_MAP -Wno-deprecated   -c -o parseCVC.o parseCVC.cpp
CVC.y: In function ‘int cvcparse()’:
CVC.y:211:13: error: ‘AssertsQuery’ was not declared in this scope
   ((ASTVec*)AssertsQuery)->push_back(parserInterface->CreateNode(TRUE));
             ^
CVC.y:217:13: error: ‘AssertsQuery’ was not declared in this scope
   ((ASTVec*)AssertsQuery)->push_back(parserInterface->CreateNode(TRUE));
             ^
CVC.y:233:13: error: ‘AssertsQuery’ was not declared in this scope
   ((ASTVec*)AssertsQuery)->push_back(asserts);
             ^
<builtin>: recipe for target 'parseCVC.o' failed
make[1]: *** [parseCVC.o] Error 1
make[1]: Leaving directory
'/nfs/adaptive/tnguyen/Src/Devel/KLEE/stp-r940/src/parser'
Makefile:26: recipe for target 'all' failed
make: *** [all] Error 2

Vu,
-------------- next part --------------
HTML attachment scrubbed and removed