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/[email protected]/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,
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
