Hi Dan, Many thanks for this patch. I applied it, together with your other patches from the stp-remove branch. I think the only remaining patches are the ones updating the documentation, at which I plan to look soon.
Best wishes, Cristian On 07/23/2012 01:04 PM, Delcypher wrote: > Hi Cristian, > > I have had a go at removing the old copy of STP from the build system by : > > * Modifying the configure script > * Modifying the makefiles > * Modifying lib/Solver/Solver.cpp and lib/Solver/STPBuilder.h (they > depend on the HAVE_EXT_STP macro). > * Updating the Getting started documentation. > > I've rebuilt and run the tests (make check and make unittests) and > everything seems to be okay. > > It's not the most elegant solution as ./configure --help lists > --with-stp as an optional argument when in fact it is mandatory > (configure will fail if this argument is not passed). > I'm not an autoconf expert so I'm not sure how to make it do something else. > > The changes (along with a few others that I think should be merged into > KLEE) is on a branch called stp-remove which is available here: > https://github.com/delcypher/klee/tree/stp-remove > > Regards, > Dan Liew. > > > > On 20 July 2012 16:49, Cristian Cadar <[email protected] > <mailto:[email protected]>> wrote: > > Hi, > > The STP version in the repository is really old, from 2009. I plan to > remove that directory soon and make --with-stp required when configuring > KLEE. Would anyone like to update the configure script accordingly? > > It should be fine to use a newer version of STP; we mention r940 on the > website because we have tested it on some of our benchmarks, and it > works well. If anyone can recommend another version, I will add it to > the website. > > Best, > Cristian > > On 07/20/2012 03:23 PM, Delcypher wrote: > > Hi Carlos, > > > > I myself am quite new to KLEE I can't answer your first question > but I > > can help with the second. If you configure KLEE as follows > > $ ./configure --with-llvm=/path/to/llvm-2.9/ > > > > Then the ENABLE_EXT_STP variable will set to 0 (see > > autoconf/configure.ac <http://configure.ac> <http://configure.ac> > ) in the Makefiles. > > If you run the following in the root of the source directory. > > $ grep -r 'ENABLE_EXT_STP' . > > > > You will see the files that depend of this variable. From glancing at > > the list of files the two most important files appear to > > beMakefile.common, tools/klee/Makefile and tools/kleaver/Makefile > > > > It appears that setting ENABLE_EXT_STP to zero will cause the > contents > > of the stp/ directory (root of the project source) to be built > and the > > resulting static libraries are used instead of an external STP > library. > > When ENABLE_EXT_STP is set to 1 (which happens if you specify > > --with-stp=/path/to/stpat configure time) then the stp/ directory > will > > not be built and the external library you specified will be used > instead. > > > > So the answer to your question "I have is to know which version does > > Klee defaults to of the STP when we do not provide on the > configuration > > the location to the STP?" is that the version of STP used is the > version > > in the stp/ folder in the root of the project. I have no idea which > > version of STP is in that folder so I can't help you any further > than that. > > > > I hope that helps a little bit. > > > > Regards, > > Dan Liew. > > > > On 20 July 2012 07:52, Carlos Andrade <[email protected] > <mailto:[email protected]> > > <mailto:[email protected] <mailto:[email protected]>>> > wrote: > > > > Dears, > > > > I am new to this list and Klee and I hope this is a question not > > related to this list, if so apologizes in advance. > > > > (1) I am interested on using Klee output of STP tests together with > > the pySTP wrapper, is this still viable? I did some search on my own > > on the STP log and noticed that the latest update to STP was > > 2012-06-15, however Klee suggests revision 940 which dates to > > 2010-07-08. On the PySTP website > > (http://security.dico.unimi.it/~roberto/pystp/) there are two > > versions where the latest one (0.2) dates to 2010-08-08 (it is not > > version control so there are only two available). Moreover, they > > require that STP is compiled and the libraries are copied to PySTP. > > I ended up finding libconsteval.a only on an old branch on the > > repository from 2008-07-09, but putting them together with 940 other > > required libraries by the wrapper didn't seem to work. Is there > > still any revision together with Klee version that would be > > compatible both between the output of Klee for .cvc and this Py > > wrapper? > > > > (2) The second question I have is to know which version does Klee > > defaults to of the STP when we do not provide on the configuration > > the location to the STP? That is, when we run: > > $ ./configure --with-llvm=/path/to/llvm-2.9/ > > > > Thank you for your attention. > > > > Best Regards, > > > > Carlos Andrade > > http://carlosandrade.co > > > > _______________________________________________ > > klee-dev mailing list > > [email protected] <mailto:[email protected]> > <mailto:[email protected] > <mailto:[email protected]>> > > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev > > > > > > > > > > _______________________________________________ > > klee-dev mailing list > > [email protected] <mailto:[email protected]> > > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev > _______________________________________________ > klee-dev mailing list > [email protected] <mailto:[email protected]> > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev > > _______________________________________________ klee-dev mailing list [email protected] http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
