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

***@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-***@imperial.ac.uk/msg01440.html

[Daniel Liew]

I'd recommend you use the upstream version of STP[1] instead. The
build system has changed for upstream CMake so you will need a recent
version of CMake and to follow the new STP build guide [2]. If you
can't do that then you could try one of the older commits before the
switch to CMake [3] that has some additional fixes that I added
relating to problems building the parser.


[1] https://github.com/stp/stp
[2] https://github.com/stp/stp/blob/master/INSTALL
[3] https://github.com/stp/stp/tree/4baa287e9f90c478b0f59c6dc2fa4fe611a1d3c4

hope that helps.

Regards,
Dan Liew.

Post by 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: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
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
/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
--
Key fingerprint = EC9F 905D 866D BE46 A896 C827 BE0C 9242 03F4 552D
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

[ChangZhuo Chen]

Thank for your help. klee works on my environment now.