~cnx/klee - KLEE fork for patch differentiation testing

Age	Commit message (Collapse)	Author
2013-11-14	Fix lseek and getdents	Martin 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-13	Merge pull request #60 from MartinNowack/fix_posix	Cristian Cadar
	Fix build of POSIX file descriptor functions
2013-11-13	Merge pull request #65 from delcypher/detect-bitcode-compiler	Cristian Cadar
	Support for the detection of the LLVM bitcode compiler in the configure script.
2013-11-08	Fix the detection of the LLVM bitcode compiler. This is now done at KLEE	Dan 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-05	Merge pull request #63 from delcypher/nouclibc	Dan Liew
	Exit if using --libc=uclibc and KLEE was not configured with uclibc
2013-11-05	Exit if using --libc=uclibc and KLEE was not configured with uclibc	Dan 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-05	Refactored part of KleeHandler construction so that	Dan 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-05	sort and remove some includes	Frank Busse

2013-11-05	Fix arbitrary path limits and improved error handling (exit	Frank Busse
	even if not built with asserts).
2013-11-02	Merge pull request #61 from MartinNowack/fix_futimesat	Paul Marinescu
	Fix Futimesat compilation with newer gcc and clang
2013-11-02	Fix Futimesat compilation with newer gcc and clang	Martin Nowack

2013-11-02	Fix build of POSIX file descriptor functions	Martin Nowack
	Build Large File System functions for 32bit and 64bit correctly
2013-10-29	Merge pull request #26 from delcypher/fix_divide_by_zero	Paul
	Fixed bug where divide by zero bugs would only be detected once in a program
2013-10-22	Merge pull request #41 from hpalikareva/metasmt-multisolver	Cristian Cadar
	Support for KLEE-MultiSolver (http://srg.doc.ic.ac.uk/projects/klee-multisolver/)
2013-10-21	Removed unnecessary/redundant linking of library boost_thread-mt to klee and ↵	Hristina Palikareva
	kleaver.
2013-10-20	Merge pull request #47 from 251/stubs_path_max	Cristian Cadar
	Simplified implementation of canonicalize_file_name(). Addresses #46.
2013-10-18	stubs.c: cleanup	Frank Busse

2013-10-18	stubs.c: fix use of undeclared identifier PATH_MAX	Frank Busse

2013-10-18	Merge pull request #45 from hpalikareva/test-expr-logging	Cristian Cadar
	Fixed solver-related nondeterminism in test case ./test/Feature/ExprLogg...
2013-10-17	Fixed 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-16	tests in ./test/Feature/ExprLogging.c reverted back to not explicitly ↵	Hristina Palikareva
	differentiate on whether metaSMT is used or not
2013-10-15	Merge pull request #43 from hpalikareva/test-large-ints	Cristian Cadar
	Fixed nondeterministic behaviour in test case ./test/Solver/LargeInteger...
2013-10-15	Fixed 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-15	command-line option --use-metasmt declared and defined inside #ifdef ↵	Hristina Palikareva
	SUPPORT_METASMT ... #endif macros
2013-10-14	Replaced --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-11	getConstraintLog() of MetaSMTSolver explicitly states that this feature is ↵	Hristina Palikareva
	not supported; a test case modified to not fail because of this.
2013-10-11	Bug fix in MetaSMTBuilder	Hristina Palikareva

2013-10-11	MetaSMT builder, solver and command-line options.	Hristina Palikareva

2013-10-11	Merge pull request #40 from antiAgainst/intrinsic-trap	Cristian Cadar
	Bugfix: Remove llvm.trap declaration after cleaning all uses.
2013-10-11	Compile separate version of fd files for 3.2 as well.	Cristian Cadar

2013-10-11	Fixed compilation on LLVM 2.9. irreader should be linked only for LLVM >= 3.3	Cristian Cadar

2013-10-11	Added Output/ and site.exp to .gitignore	Cristian Cadar

2013-10-08	Remove llvm.trap declaration after cleaning all uses.	Lei Zhang

2013-10-08	Merge pull request #34 from ddcc/master	Cristian Cadar
	Replace current implementation of linkWithLibrary()
2013-10-03	Merge pull request #39 from hpalikareva/master	Dan Liew
	Extending ./configure with support to use metaSMT.
2013-10-03	Extending ./configure with support to use metaSMT.	Hristina Palikareva

2013-09-25	Merge pull request #25 from paulmar/master	Cristian Cadar
	Added some of the common *at functions & others to the model. Obey --max-forks in switch statements.
2013-09-25	Merge pull request #27 from antiAgainst/intrinsic-trap	Cristian Cadar
	Lower intrinsic instruction "llvm.trap" to a call of the abort() function.
2013-09-25	Obey --max-forks in switch statements	Paul Marinescu

2013-09-24	Add missing header file and linker parameter	Dominic Chen

2013-09-24	Replace implementation of linkWithLibrary()	Dominic Chen

2013-09-23	Lower intrinsic instruction "llvm.trap" to a call of the abort() function.	Lei Zhang

2013-09-21	Merge pull request #17 from MartinNowack/LLVM33	Cristian Cadar
	Make KLEE compile with LLVM 2.3.
2013-09-18	Merge pull request #23 from MartinNowack/fix_putchar	Cristian Cadar
	Fix implementation for putchar
2013-09-18	Compile separate version of fd files only for LLVM 3.3 or higher	Martin Nowack

2013-09-17	Merge pull request #21 from delcypher/fix_query_logging	Cristian Cadar
	Fix queries not being logged correctly if an assertion failure is hit.
2013-09-17	Merge branch 'fix_runtime_build_mode' of https://github.com/delcypher/klee ↵	Cristian Cadar
	into delcypher-fix_runtime_build_mode
2013-09-02	Implemented runtime check for overshift (controllable with --check-overshift	Dan Liew
	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.
2013-09-02	Fixed bug where divide by zero bugs would only be detected once in a program	Dan Liew
	even if there were many divide by zero bugs. The fix basically inlines all function calls to klee_div_zero_check() so that each call to klee_report_error() is a unique instruction for each instrumentation of a divide operation. It also seems that inlining the call "magically" fixed the debug information (file and line number) of the instruction so that the debug information on the inlined instructions matches that of the instrumented division instruction. Note that the command line option -emit-all-errors could be used to workaround the bug fixed in this commit.
2013-09-02	Fixed multiple definitions of POSIX file functions	Martin Nowack
	Function like stat() were defined for 32bit and 64bit version. Added compile time based selection of appropriate version using GNUC macros __x86_64__ and __ppc64__.