Age | Commit message (Collapse) | Author |
|
LLVM versions
With newer LLVM versions (starting with LLVM 2.7) debug information are directly associated
as meta data with each instruction.
Therefore, debug information can be acquired directly from each instruction.
|
|
Patch by Daniel Lupei, fixing a performance bug with the counterexample cache. (This is an old patch, reported at http://llvm.org/bugs/show_bug.cgi?id=11435, on KLEE's old bug tracking system.)
|
|
Re-add support for running individual tests when built with LLVM3.3
|
|
It seems that the LLVM configure script no longer
looks for tclsh which was used to execute individual tests. E.g.
$ cd test
$ make TESTONE=Runtime/POSIX/DirConsistency.c check-one VERBOSE=1
This prevented the above from working. This commit fixes this by
having our configure script look for tclsh instead. The path_tclsh.m4
macro is taken from the projects/sample/autoconf/m4/ in LLVM3.3
|
|
Allow different build modes for LLVM coexist (this issue can be avoided entirely if out of source builds are used and each build is its own directory)
|
|
|
|
counterexample cache. (This is an old patch, reported at
http://llvm.org/bugs/show_bug.cgi?id=11435, on KLEE's old bug tracking
system.)
|
|
Chroot replay feature
|
|
|
|
Deprecate LLVM 2.8 and lower and remove support for it
|
|
|
|
|
|
Patch Set II - Memleaks
|
|
|
|
|
|
Fixes memleak
|
|
|
|
Fix using assembler addresses for global variables
|
|
|
|
prior patch, this is part of the CU experiments and doesn't really
belong here.
|
|
Fix runtime posix
|
|
|
|
uclibc is compiled without symbolic printf support
|
|
Wrong data types and casts led to wrong values on 64 bit machines
with high values filedescriptor positions.
Fixes DirConsistency and DirSeek test case
|
|
Format of assembler address strings are different
with newer LLVM version (They don't have a prefix anymore).
This fix takes care of newer LLVM versions (>=3.3) as well.
|
|
Fix build of POSIX file descriptor functions
|
|
Support for the detection of the LLVM bitcode compiler in the configure script.
|
|
configure time, not LLVM configure time! Configure will fail without
a working LLVM bitcode compiler. The precedence of detection is as
follows:
1. Compilers set by newly added --with-llvmcc= --with-llvmcxx= configure flags.
2. Clang in LLVM build directory.
3. llvm-gcc in PATH.
4. clang in PATH.
This has been tested with llvm2.9 (llvm-gcc in PATH) and llvm3.3 (clang
built in LLVM build directory).
This addresses a major pain point for new users of KLEE who forget to
put llvm-gcc in their PATH at LLVM configure time and then are later
forced to reconfigure and rebuild LLVM just so KLEE knows the right
PATH!
|
|
Exit if using --libc=uclibc and KLEE was not configured with uclibc
|
|
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).
|
|
Fix Futimesat compilation with newer gcc and clang
|
|
|
|
Build Large File System functions for 32bit and 64bit correctly
|
|
Fixed bug where divide by zero bugs would only be detected once in a program
|
|
Support for KLEE-MultiSolver (http://srg.doc.ic.ac.uk/projects/klee-multisolver/)
|
|
kleaver.
|
|
Simplified implementation of canonicalize_file_name(). Addresses #46.
|
|
|
|
|
|
Fixed solver-related nondeterminism in test case ./test/Feature/ExprLogg...
|
|
./test/Feature/ExprLogging.c -- using the counterexample cache affects the total number of queries issued to the solver.
|
|
differentiate on whether metaSMT is used or not
|
|
Fixed nondeterministic behaviour in test case ./test/Solver/LargeInteger...
|
|
-- only 16 bytes of array a were initialised in Query 2, but values of 17 bytes were later required for comparison.
|
|
SUPPORT_METASMT ... #endif macros
|
|
https://github.com/ccadar/klee/issues/32) and fixed an #include in one of the tests.
|
|
not supported; a test case modified to not fail because of this.
|