~cnx/klee - KLEE fork for patch differentiation testing

Age	Commit message (Collapse)	Author
2019-03-21	remove obsolete LegacyLLVMPassManagerTy	Julian Büning

2019-03-21	remove obsolete macro KLEE_LLVM_GEP_TYPE	Julian Büning

2019-03-20	STPSolver: C++11, add missing free, refactoring	Frank Busse

2019-03-19	Add support to assign debug instructions to optimised code	Martin Nowack

2019-03-19	Use debugging information from newer LLVM versions	Martin Nowack

2019-03-19	separate between instructions and functions	Martin Nowack

2019-03-19	Refactor InstructionInfoTable	Martin Nowack
	Better debug information
2019-03-19	Add Read consistency test case, spelling	Timotej Kapus

2019-03-19	Fix representation of ReadExpr of equivalent arrays	Martin Nowack
	ObjectStates can be shared between multiple states. A read expression of a symbolic object can be represented differently depending on previous read expression on the same object. If the read expression uses a symbolic index, all pending updates will become entries in the update list of the object state. If the same object state is read again, with a concrete index, the latest update list item will be referenced, even though it might contain more recent but non-essential updates. If, instead, a concrete read will be executed first, it does not contain the non-essential updates. For both executions, the ReadExpr with a constant index will have two different representations, which is not intented. This patch makes sure, we do not include more recent, non-essential updates for concrete reads. Fixes #921
2019-03-18	Disable optimisation for functions that contain KLEE calls	Martin Nowack
	Compilers are allowed to hoist function calls and do GVE. This is currently done even without `--optimization` enabled. This is unfortunate in the context of KLEE function calls that might depend on specific code position without direct control flow dependencies. In such cases, function calls can be hoisted. To circumvent this, disallow to optimise functions that contain such calls by default. This might reduce optimisation for some functions containing such function calls but still allows it for all others. This patch adds an additional pass, that detects all functions starting with a prefix `klee_` and disable optimisations for functions containing such calls. This is enabled by default but can be disabled by `--klee-call-optimisation=false`.
2019-03-17	Renamed --use-cache to --use-branch-cache	Cristian Cadar

2019-03-17	run VerifierPass after optimization and instrumentation	Julian Büning

2019-03-16	Added support for disabling --batch-instructions and --batch-time by setting ↵	Cristian Cadar
	them to 0
2019-03-15	Placed option categories in the klee namespace and options in the anonymous ↵	Cristian Cadar
	namespace in Executor.cpp
2019-03-15	Placed --max-time in the termination category	Cristian Cadar

2019-03-15	Placed --rewrite-constraints in the constraint solving category	Cristian Cadar

2019-03-15	Categorized the options in SpecialFunctionHandler.cpp	Cristian Cadar

2019-03-15	Added help message for --use-constant-arrays, and placed option in the ↵	Cristian Cadar
	constraint solving category
2019-03-15	Renamed --seed-out to --seed-file and --seed-out-dir to --seed-dir, and ↵	Cristian Cadar
	placed them in the seeding category. Moved options and option categories in Executor.cpp to the klee namespace.
2019-03-15	Reformatted options and headers in Executor.cpp and did a proofreading pass ↵	Cristian Cadar
	over all help messages.
2019-03-15	Added several options in Executor.cpp to the constraint solving category	Cristian Cadar

2019-03-15	Created a new statistics option category	Cristian Cadar

2019-03-15	Moved the options in Optimize.cpp to the module category	Cristian Cadar

2019-03-15	Created a new module-related option category and moved the options in ↵	Cristian Cadar
	KModule.cpp in there
2019-03-13	Added function to hide all options in a given category. Removed uneeded ↵	Cristian Cadar
	(and incorrectly-implemented) function for hiding all options unrelated to a set of categories.
2019-03-13	Placed --warnings-only-to-file in a miscellaneous category	Cristian Cadar

2019-03-13	Placed --use-visitor-hash in the expresion building/printing category	Cristian Cadar

2019-03-13	Renamed --red-zone-space to --redzone-size and improved help message	Cristian Cadar

2019-03-13	Added --const-array-opt to building&printing expression category	Cristian Cadar

2019-03-13	Renamed --use-construct-hash to --use-construct-hash-stp and moved it and ↵	Cristian Cadar
	use-construct-hash-z3 to the expression building/printing category
2019-03-13	Moved options in ExprSMTLIBPrinter.cpp to the expression building and ↵	Cristian Cadar
	printing category
2019-03-13	Documented options in ExprPPrinter.cpp and placed them into a new option ↵	Cristian Cadar
	category for building and printing expressions
2019-03-13	Consistently use "default=true" and "default=false" instead of "default=on" ↵	Cristian Cadar
	and "default=off" in --help
2019-03-13	Added options in QueryLoggingSolver.cpp to the constraint solving category	Cristian Cadar

2019-03-13	Added missing description for some options in CmdLineOptions.cpp (and some ↵	Cristian Cadar
	reformatting).
2019-03-13	Added options in CexCachingSolver.cpp to the constraint solving category and ↵	Cristian Cadar
	improved help messages
2019-03-13	Created new search option category and moved there the options in ↵	Cristian Cadar
	UserSearcher.cpp
2019-03-13	Added options in ArrayExprOptimizer.cpp to the constraint solving category	Cristian Cadar

2019-03-13	Reordered includes in ArrayExprOptimizer.cpp for consistency with the other ↵	Cristian Cadar
	files
2019-03-13	Created a new memory management option category for the options in ↵	Cristian Cadar
	MemoryManager.cpp
2019-03-13	Added --debug-log-state-merge to path merging category	Cristian Cadar

2019-03-12	Fixed unitialised memory in `MergeHandler`	Martin Nowack
	Add missing initialisation for `closedMean` for `MergeHandler`
2019-03-12	time: add double type for span multiplications	Frank Busse

2019-03-12	Removed unneeded and confusing disable-opt option, reformatted Optimize() ↵	Cristian Cadar
	function and updated some .ll tests to use --optimize=false instead of --disable-opt
2019-03-11	Replaced "default=off" with "default=false"	MartinNowack
	Co-Authored-By: ccadar <c.cadar@imperial.ac.uk>
2019-03-11	Created a path merging option category and improved help message for path ↵	Cristian Cadar
	merging options
2019-03-11	Added options in STPSolver.cpp to the constraint solving category	Cristian Cadar

2019-03-11	Added Z3 options to the constraint solving category	Cristian Cadar

2019-03-11	Add support for LLVM 8.0	Martin Nowack

2019-03-05	workaround for LLVM PR39177	Julian Büning
	provides a workaround for LLVM bug PR39177, which affects LLVM versions 3.9 - 7.0.0: https://bugs.llvm.org/show_bug.cgi?id=39177 This commit is intended to be reverted once support for LLVM versions <= 7 is dropped from KLEE.