~cnx/klee - KLEE fork for patch differentiation testing

Age	Commit message (Collapse)	Author
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-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__.
2013-09-02	Fixed unused static function warning for forceImport	Martin Nowack

2013-08-30	Merge pull request #20 from delcypher/remove_pointless_loop	Cristian Cadar
	Remove unnecessary loop from SolverTest unit test.
2013-08-30	Merge branch 'CompilerWarnings' of https://github.com/MartinNowack/klee into ↵	Cristian Cadar
	MartinNowack-CompilerWarnings
2013-08-29	Added some of the common *at functions to the model	Paul Marinescu

2013-08-29	Revert "Use new PathV2 interface for LLVM 2.9 and higher"	Martin Nowack
	This reverts commit 5c059018c02a7c7db252a3cb636a39c89c430a06.
2013-08-29	Merge branch 'CompilerWarnings' of https://github.com/MartinNowack/klee into ↵	Cristian Cadar
	MartinNowack-CompilerWarnings
2013-08-29	Fix compiling issues with llvm 2.9	Martin Nowack
	Interface for ParseCommandLineOptions changed with LLVM 3.2 preserving constness for pointer to arguments.
2013-08-29	Use new PathV2 interface for LLVM 2.9 and higher	Martin Nowack
	Enable PathV2 interface starting from LLVM 2.9 and do some minor include cleanup.
2013-08-28	Modified the buildmode of bitcode libraries.	Dan Liew
	The Default is Release+Asserts but if you are building KLEE with debug symbols (for example "Release+Debug+Asserts" or "Debug+Asserts") then this breaks because KLEE will look for the bitcode libraries in the wrong place because the RUNTIME_CONFIGURATION macro is not defined to be what KLEE actually builds as. This has been tweaked so that when we build the bitcode libraries the Makefile variable "DEBUG_SYMBOLS" is correctly overridden.