| Age | Commit message (Collapse) | Author |
|---|
|
|
|
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
|
|
|
|
|
|
|
|
|
|
or if the configured path does not exist.
Previously if KLEE was configured and compiled without uclibc linking
would still succeed because KLEE_UCLIBC was blank so LLVM was
effectively asked to link with "/lib/libc.a" i.e. the system's native
C library!
|
|
- A fixed size buffer is no longer used for output Directory path
(would of failed for large paths).
- KLEE warns about the presence of klee-out-* files that aren't
directories.
- We don't get stuck in an infinite loop if there aren't available
directories.
|
|
|
|
even if not built with asserts).
|
|
Fixed bug where divide by zero bugs would only be detected once in a program
|
|
kleaver.
|
|
|
|
|
|
|
|
Make KLEE compile with LLVM 2.3.
|
|
command line argument).
Overshift is where a Shl, AShr or LShr has a shift width greater
than the bit width of the first operand. This is undefined behaviour
in LLVM so we report this as an error.
|
|
This reverts commit 5c059018c02a7c7db252a3cb636a39c89c430a06.
|
|
Interface for ParseCommandLineOptions changed with LLVM 3.2
preserving constness for pointer to arguments.
|
|
Enable PathV2 interface starting from LLVM 2.9 and do some minor include
cleanup.
|
|
|
|
|
|
Major changes are:
- Switching to llvm-link to build archive files
- Use GetMallocUsage instead of GetTotalMemoryUsage (be aware of bug in
LLVM 3.3 http://llvm.org/bugs/show_bug.cgi?id=16847)
- intrinsic library functions like memcpy/mov/set use weak linkage to be
replaced by e.g. uclibc functions
- rewrote linking with library
- enhanced MemoryLimit test case to check if mallocs were successful
|
|
Patch Set VII - Handle additional debug intrinsics of LLVM
|
|
Fixed typos.
|
|
|
|
|
|
|
|
STPSolver objects. Timeout is now set by the solver at the top of the solver chain rather than by STPSolver.
|
|
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().
|
|
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.
|
|
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
|
