| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
under release build.
The problem is that under release build the install command is told
to strip symbols from the tools. It tries to do this for the python
scripts and fails.
This commit hacks this by requesting that symbols are not stripped
from the python scripts.
|
|
it can find klee-uclibc inside the same folder as the other
runtime libraries with the name "klee-uclibc.bca"
This is implemented as follows:
* When building, a sym-link is created to klee-uclibc's libc.a file
in the same directory that the rest of KLEE's runtime libraries
are built. This done so that if a developer changes klee-uclibc
on their system then the correct version of klee-uclibc is used
by KLEE.
* When installing, klee-uclibc's libc.a file is installed in the same
directory that the rest of KLEE's runtime libraries are installed.
In addition the configure script argument --with-uclibc can now
operate in two ways. It can either be passed the path to the root
of klee-uclibc or it can be passed a path to the libc.a file built
by klee-uclibc. This new behaviour has been added to allow users
to potential use pre-built versions of klee-uclibc.
|
|
are now detected at runtime. This allows the correct location
to be used when klee is invoked from the build directory or
from its install location (i.e. make install)
|
|
This reverts commit 1715ee37118cdf8785a1dd70d812b6a88ad623e7.
Conflicts:
Makefile.common
Future commits are going to add a more way elegant to handle the
search for libraries in build/install directory.
|
|
Chroot replay feature
|
|
|
|
|
|
|
|
|
