Age | Commit message (Collapse) | Author |
|
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
|
|
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@176571 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
options were shared.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@173819 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
solver chain.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@173180 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
Kleaver to a separate file.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@171395 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@171391 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
enables KLEE to log only the queries exceeding a certain duration, or only those that time out.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@171385 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
watchdog is in effect kills the watchdog immediately, giving the user
a shell prompt prematurely while the child process is still running.
This patch keeps the watchdog running until the child is finished.
I see no need to be able to kill the watchdog forcefully, as long
as the child process can be killed forcefully with two interrupts."
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@168696 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
klee_get_value*. It might be better to just get (most of) the exported
symbols right from the SpecialFunctionHandler class."
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@166585 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
head (Just a cosmetic change to make things a bit more readable)" and
"move duplicate code to a function and also remove an old comment that
seems to be obsolete by now. (Another cosmetic change)"
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@166581 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
writing out test cases (option --write-smt2s) in KLEE."
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@166568 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
allows .pc files to be printed as SMT-LIBv2 queries."
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@166563 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
--print-rel-times, --precision) to klee-stats.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@165499 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@163632 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
--with-stp option mandatory:
"1. At configure time the --with-stp= option is now mandatory.
2. The HAVE_EXT_STP macro has been removed.
3. The ENABLE_EXT_STP autoconf replacement variable has been removed and consequently the Makefile variable of the same name has been removed."
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@161055 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
and max memory consumption and states. A bug in the compare-by=<key> functionality has been fixed and the --compare-at=[<value>|last] option has been added. Specifying a value reports all statistics at the point where <key> had value <value>; specifying 'last' reports at the largest <key> value common to all executions"
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@158948 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@158835 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@158721 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@154110 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
install location instead of the compile-tree location if a
compile-time macro is enabled."
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@148961 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@146741 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@146353 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
fixes the ntohs prototype in klee-libc, and removes some unused code.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@146352 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@139026 91177308-0d34-0410-b5e6-96231b3b80d8
|
|
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@135598 91177308-0d34-0410-b5e6-96231b3b80d8
|