about summary refs log tree commit diff homepage
path: root/lib/Basic
AgeCommit message (Collapse)Author
2016-09-26Modified logging information to steer the usage of klee_message, ↵Andrea Mattavelli
klee_warning, and klee_error
2016-09-15Rename `-debug-cross-check-core-solver` option toDan Liew
`-debug-crosscheck-core-solver` as requested by Cristian
2016-09-15Add ``-debug-cross-check-core-solver`` option to allow cross-checkingDan Liew
with another solver. For example the core solver can be STP and the cross checking solver can be Z3. Unfortunately a few fragile tests don't pass when actually using this option.
2016-09-15Clang-format ``ConstructSolverChain.cpp``Dan Liew
2016-06-10rename the configure option --with-metasmt-default-solver to ↵Hoang M. Le
--with-metasmt-default-backend and improve the associated CXX flag
2016-06-10use default metaSMT solver as defined in configurationHoang M. Le
2016-04-14Disabling --solver-optimize-divides by default, as the optimization is ↵Cristian Cadar
currently buggy, and we keep hitting this bug... See https://github.com/klee/klee/issues/334 for details.
2016-03-01Documented default values for various options and improved the description ↵Cristian Cadar
of some.
2016-02-23Added missing copyright headers per klee/issue #301Marko Dimjašević
2016-02-10Add some of the basic plumbing required to support a Z3 solver in KLEE.Dan Liew
2016-02-08Fixed two spelling errors.Marko Dimjašević
2016-01-14Make it possible to build KLEE without using STP and only MetaSMT.Dan Liew
The default core solver is STP if KLEE is built with STP otherwise it is MetaSMT. Whilst I'm here rename SUPPORT_METASMT macro to ENABLE_METASMT for consistency.
2016-01-12Refactor setting the core solver (i.e. STP, MetaSMT or DummySolver) by providingDan Liew
a ``createCoreSolver()`` function. The solver used is set by the new ``--solver-backend`` command line argument. The default is STP. This change necessitated refactoring the MetaSMT stuff. That clearly didn't belong in the Executor! The MetaSMT command line option is now ``--metasmt-backend`` as this only picks the MetaSMT backend. In order to use MetaSMT ``--solver-backend=metasmt`` needs to be passed. Note I don't have MetaSMT built on my development machine so I don't know if the MetaSMT stuff even compiles...
2014-05-29Refactoring from std::ostream to llvm::raw_ostreamMartin Nowack
According to LLVM: lightweight and simpler implementation of streams.
2013-12-21Do not install KLEE's internal libraries.Dan Liew
2013-10-15command-line option --use-metasmt declared and defined inside #ifdef ↵Hristina Palikareva
SUPPORT_METASMT ... #endif macros
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-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-07-18Patch by Stephan Falke fixing an incorrect message. Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@186589 91177308-0d34-0410-b5e6-96231b3b80d8
2013-04-03Code reformatting.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@178642 91177308-0d34-0410-b5e6-96231b3b80d8
2013-03-11Forgot to add ConstructSolverChain.cpp in the previous patch.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@176813 91177308-0d34-0410-b5e6-96231b3b80d8
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
2009-05-29Changed .ktest header from BOUT\n to KTEST. Old .bout files can still be read.Cristian Cadar
Increased KTEST version. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72592 91177308-0d34-0410-b5e6-96231b3b80d8
2009-05-23Changed bout to ktest. Kept "BOUT\n" as the header of test files, for ↵Cristian Cadar
backward compatibility. Also changed KLEE_RUNTEST to KTEST_FILE. Updated tutorial-1. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72312 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-22 16:54:50 +0000