about summary refs log tree commit diff homepage
path: root/tools
AgeCommit message (Collapse)Author
2016-02-23Added missing copyright headers per klee/issue #301Marko Dimjašević
2016-02-14Add basic implementation of Z3Builder and Z3Solver and Z3SolverImplDan Liew
which is based on the work of Andrew Santosa (see PR #295) but fixes many bugs in that implementation. The implementation communicates with Z3 via it's C API. This implementation is based of the STPSolver and STPBuilder and so it inherits a lot of its flaws (See TODOs and FIXMEs). I have also ripped out some of the optimisations (constructMulByConstant, constructSDivByConstant and constructUDivByConstant) that were used in the STPBuilder because * I don't trust them * Z3 can probably do these for us in the future if we use the ``Z3_simplify()`` At a glance its performance seems worse than STP but future work can look at improving this.
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-14Remove unnecessary MetaSMT includes from kleaver's ``main.cpp``.Dan Liew
2016-01-14Refactor the MetaSMT makefile commands into its own file which canDan Liew
be included by tools that needs to link against MetaSMT. Apart from making the Makefile code cleaner this allowed the Solver unit test linking to succeed when not building with STP support. Unfortunately when using MetaSMT as the core solver the Solver unit tests do not pass. Clearly no one tried this before... :(
2016-01-14Fix linking with stp via MetaSMT when not building with direct STPDan Liew
support
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...
2015-12-17Refactoring: Moving klee_warning/_error functions to ErrorHandling in ↵Martin Nowack
Support directory
2015-08-14tools/klee: pass the entry function name as argumentRiccardo Schirone
2015-08-14tools/klee/main: remove whitespacesRiccardo Schirone
2015-06-03Added an option --readable-posix-inputs which is used to turn on/off the CEX ↵Cristian Cadar
preferences added in the POSIX model. Removed option --prefer-cex which controlled all CEX preferences.
2015-04-25Rename macroDan Liew
s/KLEE_INSTALL_LIB_DIR/KLEE_INSTALL_RUNTIME_DIR/ The new name is more accurrate.
2015-04-25Do not install gen-random-bout.Dan Liew
2015-04-25Give KLEE release version information in the output of klee and kleaverDan Liew
when they are given the --version command line option. Unfortunately to make the build type and git revision available we need to check this for every build which means KLEE's support library will be rebuilt for every build which will slow down incremental builds. This addresses issue #231
2015-04-25Remove dead STP logging code.Dan Liew
2015-04-03Upstream STP now depends on an external build of minisat. Attempt toDan Liew
fix travis build of upstream STP and also how KLEE links against STP.
2015-04-02Silenced some compilation warnings.Cristian Cadar
2015-04-01[tools] Added fortified version wrapper for fprintfMartin Nowack
2015-02-13refactor integer overflow detection, add signed intLuca Dariz
Instead of checking for every possible casse which result in overflow, it is much simpler to perform the operation using integers with bigger dimension and check if the result overflow
2015-02-13Detect overflow of unsigned add, sub and mul operationsLuca Dariz
This requires clang with -fsanitize=unsigned-integer-overflow tested with clang and llvm 3.4.2
2015-02-13Revert "Merged @luckyluke's change for detecting overflow of unsigned add, sub"Cristian Cadar
Will redo the merge to preserve original commits. This reverts commit a743d7072d9ccf11f96e3df45f25ad07da6ad9d6.
2015-02-10Merged @luckyluke's change for detecting overflow of unsigned add, subCristian Cadar
and mul operations. Refactored tests into two main cases, and disabled them on LLVM 2.9, which does not support -fsanitized=*signed-integer-overflow.
2014-12-18Merge pull request #178 from mchalupa/masterCristian Cadar
klee: let user override path to runtime library
2014-12-02Implement :named and let abbreviation modes in ExprSMTLIBPrinterRaimondas Sasnauskas
* Set the default abbreviation mode to let (ExprSMTLIBPrinter::ABBR_LET) * Remove the now defunct ExprSMTLIBLetPrinter * Improve performance of ExprSMTLIBPrinter::scan() by keeping track of visited Expr to avoid visiting them again * Rename ExprSMTLIBPrinter::printQuery() to ExprSMTLIBPrinter::printQueryExpr()
2014-12-01klee: let user override path to runtime libraryMarek Chalupa
When looking for runtime library, look first into KLEE_RUNTIME_LIBRARY_PATH environment variable. This allows to use klee not only in 'hardcoded' environment. Signed-off-by: Marek Chalupa <mchqwerty@gmail.com>
2014-11-13tools: prepend DESTDIR when installingJiri Slaby
Some tools prepend DESTDIR properly, some not. ktest-tool and klee-stats do not, so 'make install' chokes with an error: llvm[2]: Installing Release+Asserts /usr/bin/ktest-tool /usr/bin/install: cannot create regular file '/usr/bin/ktest-tool': Permission denied Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2014-11-01Upstream libstp is no longer dependent on Boost so remove theDan Liew
configure/Makefile code that adds Boost as a depdendency because We don't need to support old versions of STP that needed Boost.
2014-09-25Patch by Sean Bartell: "F_Binary was actually moved in LLVM 3.4 (r186447), ↵Cristian Cadar
not 3.0."
2014-09-17Fix segfault under LLVM3.5 . I forgot to release ownership of theDan Liew
MemoryBuffer from the std::unique_ptr when getLazyBitcodeModule() succesfully takes ownership.
2014-09-17Fix more LLVM3.5 compilation issues.Dan Liew
2014-09-17Compilation fix for LLVM3.5 caused by the removal of sys::fs::F_Binary.Dan Liew
The commit that caused this is r202052.
2014-09-17Another LLVM3.5 compilation fix.Dan Liew
2014-09-16[LLVM3.5] Update Kleaver for MemoryBuffer::getFileOrSTDIN changes.Daniel Dunbar
2014-09-16Fix #include under LLVM3.5. OwningPtr doesn't exist anymore.Dan Liew
2014-09-16Fix LLVM3.5 compilation a little more. ``Support/system_error.h``Dan Liew
was removed by r210803
2014-09-15Merge pull request #158 from delcypher/remove_response_filesCristian Cadar
Remove --read-args command line option because this feature has been
2014-09-15Taught klee_warning(), klee_error() etc... to emit coloured text output.Dan Liew
Also use bold green text when KLEE finishes. This is done by taking advantage of llvm::raw_ostream's nice API for controlling the console text colour.
2014-09-15Remove --read-args command line option because this feature has beenDan Liew
available in LLVM's command line parser for a while (response files).
2014-09-14Remove dependence on the bc tool. Use python instead because we areDan Liew
already dependent on it.
2014-09-13Add KLEE specific DEBUG macros.Daniel Dunbar
- This allows us to build in +Asserts mode even when LLVM isn't (by disabling the checks in that mode). - Eventually it would be nice to just move off of LLVM's DEBUG infrastructure entirely and just have our own copy, but this works for now. - Fixes #150.
2014-09-12Tweak the workarounds for multiple definition of PACKAGE_* macros from ↵Daniel Dunbar
config.h files. - There seems to be a better solution for this by defining a macro prefix, per: http://www.gnu.org/software/autoconf-archive/ax_prefix_config_h.html but I have no experience with that and it looks like it might involve rewriting a bunch of our macro checks.
2014-09-12Do not require <sys/capability.h>, which is Linux specific.Daniel Dunbar
2014-07-21Merge pull request #113 from antiAgainst/klee-statsCristian Cadar
klee-stats refactoring and improvement by antiAgainst: "this includes changing from OptionParser to ArgumentParser, rewriting not-pythonic code, respecting PEP8, etc; Adding line chart drawing in klee-stats."
2014-07-18Refactor klee-stats and add simple line chart drawing functionality.Lei Zhang
2014-07-09Fix to avoid warning message taking address of mainMartin Nowack
2014-05-29Remove #include <iostream> to avoid static constructorsMartin Nowack
iostream injects static constructor function into every compilation unit. Remove this to avoid it.
2014-05-29Refactoring from std::ostream to llvm::raw_ostreamMartin Nowack
According to LLVM: lightweight and simpler implementation of streams.
2014-04-23Fixing linking order if metaSMT is used: linking rt after z3 to avoid ↵Hristina Palikareva
undefined symbols in the z3 library.
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-22 06:51:51 +0000