about summary refs log tree commit diff homepage
AgeCommit message (Collapse)Author
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.
2013-10-11Bug fix in MetaSMTBuilderHristina Palikareva
2013-10-11MetaSMT builder, solver and command-line options.Hristina Palikareva
2013-10-11Merge pull request #40 from antiAgainst/intrinsic-trapCristian Cadar
Bugfix: Remove llvm.trap declaration after cleaning all uses.
2013-10-11Compile separate version of fd files for 3.2 as well.Cristian Cadar
2013-10-11Fixed compilation on LLVM 2.9. irreader should be linked only for LLVM >= 3.3Cristian Cadar
2013-10-11Added Output/ and site.exp to .gitignoreCristian Cadar
2013-10-08Remove llvm.trap declaration after cleaning all uses.Lei Zhang
2013-10-08Merge pull request #34 from ddcc/masterCristian Cadar
Replace current implementation of linkWithLibrary()
2013-10-03Merge pull request #39 from hpalikareva/masterDan Liew
Extending ./configure with support to use metaSMT.
2013-10-03Extending ./configure with support to use metaSMT.Hristina Palikareva
2013-09-25Merge pull request #25 from paulmar/masterCristian Cadar
Added some of the common *at functions & others to the model. Obey --max-forks in switch statements.