| Age | Commit message (Collapse) | Author |
|---|
|
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...
|
|
Support directory
|
|
|
|
|
|
preferences added in the POSIX model. Removed option --prefer-cex which controlled all CEX preferences.
|
|
s/KLEE_INSTALL_LIB_DIR/KLEE_INSTALL_RUNTIME_DIR/
The new name is more accurrate.
|
|
|
|
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
|
|
|
|
fix travis build of upstream STP and also how KLEE links against STP.
|
|
|
|
|
|
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
|
|
This requires clang with -fsanitize=unsigned-integer-overflow
tested with clang and llvm 3.4.2
|
|
Will redo the merge to preserve original commits.
This reverts commit a743d7072d9ccf11f96e3df45f25ad07da6ad9d6.
|
|
and mul operations. Refactored tests into two main cases, and
disabled them on LLVM 2.9, which does not support -fsanitized=*signed-integer-overflow.
|
|
klee: let user override path to runtime library
|
|
* 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()
|
|
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>
|
|
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>
|
|
configure/Makefile code that adds Boost as a depdendency because We
don't need to support old versions of STP that needed Boost.
|
|
not 3.0."
|
|
MemoryBuffer from the std::unique_ptr when getLazyBitcodeModule()
succesfully takes ownership.
|
|
|
|
The commit that caused this is r202052.
|
|
|
|
|
|
|
|
was removed by r210803
|
|
Remove --read-args command line option because this feature has been
|
|
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.
|
|
available in LLVM's command line parser for a while (response files).
|
|
already dependent on it.
|
|
- 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.
|
|
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.
|
|
|
|
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."
|
|
|
|
|
|
iostream injects static constructor function into every compilation unit.
Remove this to avoid it.
|
|
According to LLVM: lightweight and simpler implementation of streams.
|
|
undefined symbols in the z3 library.
|
|
|
|
If directory has no trailing slash, the slash is not addedd
if concatenated
|
|
not have the equals() method.
|
|
|
|
of old V1 path API.
LLVM2.9 supports LLVM's V2 path API. Because that is the minimum
version we support we should just use this API everywhere so we
reduce the number of #if LLVM_VERSION_CODE macros and duplicated
code.
|
|
Old Path API was removed
|
|
|
|
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.
|
