[klee-dev] Cannot build stp for KLEE in debian x86_64

[ChangZhuo Chen]

Hi All,

I follow the procedure in [1] to setup KLEE. However, it fails in
building STP with the following fail message. Please help to check if
anything wrong in my environment, thanks.


g++ -O2  -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS -DEXT_HASH_MAP
-Wno-deprecated   -c -o lexcvc.o lexcvc.cpp
g++ -O2  -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS -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);
             ^
make[1]: *** [parsecvc.o] Error 1
make[1]: Leaving directory `/home/czchen/src/llvm-project/klee/stp/src/parser'



My machine is Debian GNU/Linux testing, x86_64 architecture. The
procedures I done for KLEE are listed as following:

1. Use apt-get to install dependencies
2. Export C_INCLUDE_PATH / CPLUS_INCLUDE_PATH
3. Down http://llvm.org/releases/2.9/llvm-gcc4.2-2.9-x86_64-linux.tar.bz2
4. Set path so that llvm-gcc points to llvm-gcc4.2-2.9-x86_64-linux/bin/llvm-gcc

    czchen at mystra:~/src/llvm-project/klee% which llvm-gcc
    /home/czchen/src/llvm-project/klee/llvm-gcc4.2-2.9-x86_64-linux/bin/llvm-gcc

5. Download and build LLVM-2.9, with patch from [2]
6. Download STP from [3]
7. Run ./scripts/configure --with-prefix=`pwd`/install
--with-cryptominisat2 in stp-r940 directory
8. Run make OPTIMIZE=-O2 CFLAGS_M32= install
9. Error message show up

I also tried stp-r1180 as describe in [4] without success.


[1] http://ccadar.github.io/klee/GetStarted.html
[2] http://mailman.ic.ac.uk/pipermail/klee-dev/2013-September/000364.html
[3] http://www.doc.ic.ac.uk/~cristic/klee/stp.html
[4] http://www.mail-archive.com/klee-dev@imperial.ac.uk/msg01440.html
-- 
ChangZhuo Chen (陳昌倬) <czchen at gmail.com>
Key fingerprint = EC9F 905D 866D BE46 A896  C827 BE0C 9242 03F4 552D