Age | Commit message (Collapse) | Author |
|
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.
|
|
|