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 <[email protected]> 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@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/[email protected]/msg01440.html > -- > ChangZhuo Chen (陳昌倬) <[email protected]> > Key fingerprint = EC9F 905D 866D BE46 A896 C827 BE0C 9242 03F4 552D > > _______________________________________________ > klee-dev mailing list > [email protected] > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
