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

[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.

On 17 January 2014 04:23, ChangZhuo Chen <czchen at gmail.com> wrote:
> 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
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev