about summary refs log tree commit diff homepage
AgeCommit message (Collapse)Author
2013-12-19Simplify acquisition of debug informtion for instruction info with newer ↵Martin Nowack
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.
2013-12-19Merge pull request #76 from srg-imperial/masterDan Liew
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.)
2013-12-19Merge pull request #79 from delcypher/fix_llvm33_single_testDan Liew
Re-add support for running individual tests when built with LLVM3.3
2013-12-19Re-add support for running individual tests when built with LLVM3.3Dan Liew
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
2013-12-19Merge pull request #80 from MartinNowack/fix_multiple_buildmodesDan Liew
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)
2013-12-19Allow different build modes for LLVM coexistMartin Nowack
2013-12-12Patch by Daniel Lupei, fixing a performance bug with theCristian Cadar
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.)
2013-12-11Merge pull request #31 from antiAgainst/chroot-replayCristian Cadar
Chroot replay feature
2013-12-08Add chroot jail support in klee-replay.Lei Zhang
2013-12-06Merge pull request #72 from MartinNowack/deprecate_llvm28MartinNowack
Deprecate LLVM 2.8 and lower and remove support for it
2013-12-06Remove stoppoint referencesMartin Nowack
2013-12-06Deprecate LLVM 2.8 and lowerMartin Nowack
2013-12-05Merge pull request #11 from MartinNowack/MemleaksCristian Cadar
Patch Set II - Memleaks
2013-12-05Close file descriptors used for warnings and messagesMartin Nowack
2013-12-05Fix unitialized valueMartin Nowack
2013-12-05Free used constants if not used anymoreMartin Nowack
Fixes memleak
2013-12-05Fix timer leakMartin Nowack
2013-11-25Merge pull request #67 from MartinNowack/fix_asm_addressCristian Cadar
Fix using assembler addresses for global variables
2013-11-15Merge branch 'master' of https://github.com/ccadar/kleeCristian Cadar
2013-11-15Removed testing-env file. As for testing-dir that was removed in aCristian Cadar
prior patch, this is part of the CU experiments and doesn't really belong here.
2013-11-15Merge pull request #69 from MartinNowack/fix_runtime_posixCristian Cadar
Fix runtime posix
2013-11-14Remove unused testing-dirMartin Nowack
2013-11-14Add additional note that testcase might fail ifMartin Nowack
uclibc is compiled without symbolic printf support
2013-11-14Fix lseek and getdentsMartin Nowack
Wrong data types and casts led to wrong values on 64 bit machines with high values filedescriptor positions. Fixes DirConsistency and DirSeek test case
2013-11-13Fix using assembler addresses for global variablesMartin Nowack
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.
2013-11-13Merge pull request #60 from MartinNowack/fix_posixCristian Cadar
Fix build of POSIX file descriptor functions
2013-11-13Merge pull request #65 from delcypher/detect-bitcode-compilerCristian Cadar
Support for the detection of the LLVM bitcode compiler in the configure script.
2013-11-08Fix the detection of the LLVM bitcode compiler. This is now done at KLEEDan Liew
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!
2013-11-05Merge pull request #63 from delcypher/nouclibcDan Liew
Exit if using --libc=uclibc and KLEE was not configured with uclibc
2013-11-05Exit if using --libc=uclibc and KLEE was not configured with uclibcDan Liew
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!
2013-11-05Refactored part of KleeHandler construction so thatDan Liew
- 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.
2013-11-05sort and remove some includesFrank Busse
2013-11-05Fix arbitrary path limits and improved error handling (exitFrank Busse
even if not built with asserts).
2013-11-02Merge pull request #61 from MartinNowack/fix_futimesatPaul Marinescu
Fix Futimesat compilation with newer gcc and clang
2013-11-02Fix Futimesat compilation with newer gcc and clangMartin Nowack
2013-11-02Fix build of POSIX file descriptor functionsMartin Nowack
Build Large File System functions for 32bit and 64bit correctly
2013-10-29Merge pull request #26 from delcypher/fix_divide_by_zeroPaul
Fixed bug where divide by zero bugs would only be detected once in a program
2013-10-22Merge pull request #41 from hpalikareva/metasmt-multisolverCristian Cadar
Support for KLEE-MultiSolver (http://srg.doc.ic.ac.uk/projects/klee-multisolver/)
2013-10-21Removed unnecessary/redundant linking of library boost_thread-mt to klee and ↵Hristina Palikareva
kleaver.
2013-10-20Merge pull request #47 from 251/stubs_path_maxCristian Cadar
Simplified implementation of canonicalize_file_name(). Addresses #46.
2013-10-18stubs.c: cleanupFrank Busse
2013-10-18stubs.c: fix use of undeclared identifier PATH_MAXFrank Busse
2013-10-18Merge pull request #45 from hpalikareva/test-expr-loggingCristian Cadar
Fixed solver-related nondeterminism in test case ./test/Feature/ExprLogg...
2013-10-17Fixed solver-related nondeterminism in test case ↵Hristina Palikareva
./test/Feature/ExprLogging.c -- using the counterexample cache affects the total number of queries issued to the solver.
2013-10-16tests in ./test/Feature/ExprLogging.c reverted back to not explicitly ↵Hristina Palikareva
differentiate on whether metaSMT is used or not
2013-10-15Merge pull request #43 from hpalikareva/test-large-intsCristian Cadar
Fixed nondeterministic behaviour in test case ./test/Solver/LargeInteger...
2013-10-15Fixed nondeterministic behaviour in test case ./test/Solver/LargeIntegers.pc ↵Hristina Palikareva
-- only 16 bytes of array a were initialised in Query 2, but values of 17 bytes were later required for comparison.
2013-10-15command-line option --use-metasmt declared and defined inside #ifdef ↵Hristina Palikareva
SUPPORT_METASMT ... #endif macros
2013-10-14Replaced --libc=klee with --libc=uclibc in two tests (as for ↵Cristian Cadar
https://github.com/ccadar/klee/issues/32) and fixed an #include in one of the tests.
2013-10-11getConstraintLog() of MetaSMTSolver explicitly states that this feature is ↵Hristina Palikareva
not supported; a test case modified to not fail because of this.
generated by cgit-pink 1.4.1 (git 2.36.1) at 2025-07-18 10:06:44 +0000