about summary refs log tree commit diff homepage
path: root/tools/kleaver
AgeCommit message (Collapse)Author
2014-01-25Upstream STP's libstp now depends on boost. This commit updatesDan Liew
the configure script to detect this by first trying to link without boost and if that fails then trying to link libstp with boost. This also updates the relevant Makefiles so that the klee and kleaver executables link in STP's boost dependencies if necessary.
2013-12-06Deprecate LLVM 2.8 and lowerMartin Nowack
2013-10-21Removed unnecessary/redundant linking of library boost_thread-mt to klee and ↵Hristina Palikareva
kleaver.
2013-10-11MetaSMT builder, solver and command-line options.Hristina Palikareva
2013-08-06TimingSolver and constructSolverChain() no longer coupled with pointers to ↵Hristina Palikareva
STPSolver objects. Timeout is now set by the solver at the top of the solver chain rather than by STPSolver.
2013-08-06Methods getConstraintLog() and setTimeout() made virtual and moved from ↵Hristina Palikareva
STPSolver to base Solver and SolverImpl classes, and consequently redefined in derived classes to call the corresponding methods down the solver chain. Method setTimeout() renamed to setCoreSolverTimeout().
2013-08-06Renaming solver-related command-line options in order to decouple them from ↵Hristina Palikareva
STP. More specifically, command-line options max-stp-time, use-forked-stp and stp-optimize-divides renamed to max-solver-time, use-forked-solver and solver-optimize-divides, respectively. Option of running the SMT solver in a separate process (i.e. forked) set to true by default. Options of running SMT solver forked and with optimized divides made available to Kleaver as well.
2013-03-11Patch by Dan Liew which unifies the solver construction between KLEECristian Cadar
and Kleaver and fixes --use-query-log in Kleaver. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@176811 91177308-0d34-0410-b5e6-96231b3b80d8
2013-03-06Patch by Tomek Kuchta which adds the --max-stp-time option to Kleaver.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@176571 91177308-0d34-0410-b5e6-96231b3b80d8
2013-01-29Patch by Tomasz Kuchta that fixes the fragile way in which KLEE and Kleaver ↵Cristian Cadar
options were shared. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@173819 91177308-0d34-0410-b5e6-96231b3b80d8
2013-01-22Patch by Hristina Palikareva which enables Kleaver to configure theCristian Cadar
solver chain. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@173180 91177308-0d34-0410-b5e6-96231b3b80d8
2013-01-02Refactoring patch by Tomasz Kuchta that moves options shared by KLEE and ↵Cristian Cadar
Kleaver to a separate file. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@171395 91177308-0d34-0410-b5e6-96231b3b80d8
2013-01-02Patch by Tomasz Kuchta adding more detailed information on query failures.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@171391 91177308-0d34-0410-b5e6-96231b3b80d8
2013-01-02Patch by Tomasz Kuchta adding a new option (min-query-time-to-log) that ↵Cristian Cadar
enables KLEE to log only the queries exceeding a certain duration, or only those that time out. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@171385 91177308-0d34-0410-b5e6-96231b3b80d8
2012-10-24Patch by Dan Liew: "Added -print-smtlib option to kleaver tool thatCristian Cadar
allows .pc files to be printed as SMT-LIBv2 queries." git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@166563 91177308-0d34-0410-b5e6-96231b3b80d8
2012-07-31Patch by Dan Liew that removes our internal copy of STP, and makes the ↵Cristian Cadar
--with-stp option mandatory: "1. At configure time the --with-stp= option is now mandatory. 2. The HAVE_EXT_STP macro has been removed. 3. The ENABLE_EXT_STP autoconf replacement variable has been removed and consequently the Makefile variable of the same name has been removed." git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@161055 91177308-0d34-0410-b5e6-96231b3b80d8
2011-07-20Deprecate LLVM_VERSION_MAJOR and LLVM_VERSION_MINOR in favour ofPeter Collingbourne
version codes. This makes the preprocessor-based version tests more concise and less error prone. Also, fix the version tests in lib/Expr/Parser.cpp (immutable zext and trunc were introduced in LLVM 2.9); now 2.9 passes "make test". git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@135583 91177308-0d34-0410-b5e6-96231b3b80d8
2011-04-23Patch by arrowdodger ↵Cristian Cadar
(http://keeda.stanford.edu/pipermail/klee-dev/2011-April/000617.html) for compiling KLEE with the latest LLVM changes. Tested against LLVM 2.7 and 2.8. The AsmAddresses test fails in 2.8 unless assertions are explicitely enabled (--enable-assertions). git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@130065 91177308-0d34-0410-b5e6-96231b3b80d8
2010-07-14Add option to use an external version of STPPeter Collingbourne
This patch adds a new configure option, --with-stp, which configures KLEE to use an external version of STP instead of the version in the source tree. It includes documentation referring users to the STP download location. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@108347 91177308-0d34-0410-b5e6-96231b3b80d8
2010-04-05STP: Switch build to using LLVM style Makefiles.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@100395 91177308-0d34-0410-b5e6-96231b3b80d8
2009-09-01Update for LLVM ostream changes.Daniel Dunbar
- Includes patch by Michael Stone! git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@80665 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-16kleaver: Add some command line options for choosing the Solver.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73485 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-14Rename FoldingExprBuilder -> SimplifyingExprBuilderDaniel Dunbar
Also, start printing query # with -print-ast (for testing purposes). git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73350 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-14Use ExprBuilder for constructing expressions in the Parser.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73345 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-09Switch Array* print-outs to use name instead of ID, and update a fewDaniel Dunbar
constructors I missed. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73127 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-08kleaver: Use raw_ostream, and print some stats.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73045 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-07Don't delete decls before parsing is complete.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73023 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-05Support counter example queries (at least, the restricted set that weDaniel Dunbar
use). - Arrays don't have sizes yet, so we don't get initial values correctly. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72939 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-05Don't evaluate queries if there were parse failures.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72934 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-05Add evaluation support to kleaver (now the default).Daniel Dunbar
- Currently only handles validity queries. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72933 91177308-0d34-0410-b5e6-96231b3b80d8
2009-05-21Initial KLEE checkin.Daniel Dunbar
- Lots more tweaks, documentation, and web page content is needed, but this should compile & work on OS X & Linux. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72205 91177308-0d34-0410-b5e6-96231b3b80d8
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-26 19:42:01 +0000