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> ) 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 <carlos.andr...@acm.org > <mailto:carlos.andr...@acm.org>> 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 > klee-dev@keeda.stanford.edu <mailto:klee-dev@keeda.stanford.edu> > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev > > > > > _______________________________________________ > klee-dev mailing list > klee-dev@keeda.stanford.edu > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev _______________________________________________ klee-dev mailing list klee-dev@keeda.stanford.edu http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
