~cnx/klee - KLEE fork for patch differentiation testing

Age	Commit message (Collapse)	Author
2020-04-30	Moved header files that were placed directly in include/klee/ into ↵	Cristian Cadar
	appropriate existing directories and a new directory Statistics; a few missing renames.
2020-04-30	Removed include/klee/util and moved header files to appropriate places	Cristian Cadar

2020-04-30	Move header files from lib/Expr to include/klee/Expr to eliminate includes ↵	Cristian Cadar
	using "../"
2020-04-30	Removed the Internal directory from include/klee	Cristian Cadar

2020-02-19	Use `ref<>` for UpdateNode	Martin Nowack
	Remove additional reference counting as part of UpdateNodeList and UpdateNode. Simplifies code.
2019-12-12	[optimize-array] Fix value transformation	Timotej Kapus
	Value transformation operates on word instead of byte arrays. That means the Read indicies need to be adjusted to reflect that. Previously IndexCleanerVisitor tried to remove the multiplications in the index to covert byte indicies to word indicies. However as the two added test cases show this is not sufficent. Therefore we remove the IndexCleanerVisistor and just divide the index with word size which should always be correct.
2019-12-12	[optimize-array] Fix hole index in buildMixedSelectExpr	Timotej Kapus
	buildMixedSelectExpr was using the byte index for holes in the select condition instead of the word based one. This only occured if there was more than 1 hole.
2019-12-12	[optimize-array] Fix hash collisions	Timotej Kapus
	The caching maps in ArrayExpr are broken, they only consider hashes and don't check for structural equality. This can lead to hash collisions and invalid Expr replacement. This is especially potetent for UpdateLists, who only put the array name in the hash, so there can be a lot of colisions.
2019-12-12	[optimize-array] Fix update list read order	Timotej Kapus
	ArrayExprOptimizer read the UpdateList in the wrong order, which meant that it used least recent update instead of the most recent one. This patch fixes this as well as adds a test to illustrate the issue.
2019-09-03	Moved solver-related header files into a separate klee/Solver/ directory.	Cristian Cadar

2019-08-01	Renamed misspelled file	Cristian Cadar

2019-07-30	Consolidated Expr-related include files into a single include/klee/Expr ↵	Cristian Cadar
	directory. This improves the organization of the code, and also makes it easier to reuse Expr outside KLEE.
2019-06-04	make endif guard naming consistent	Julian Büning

2019-06-04	make include guard naming consistent	Julian Büning

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-15	Placed --rewrite-constraints in the constraint solving category	Cristian Cadar

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

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

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 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
2018-10-26	llvm5: APInt->getSignBit -> getSignMask	Jiri Slaby
	This was renamed in LLVM commit 54f0462d2b7f, so handle the rename. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-10-26	llvm5: integerPartWidth is from llvm::APFloatBase	Jiri Slaby
	Otherwise we see: ../lib/Expr/Expr.cpp:331:14: error: no member named 'integerPartWidth' in namespace 'llvm'; did you mean 'llvm::APFloatBase::integerPartWidth'? Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-10-23	Updated an include to reflect a recent filename change	Cristian Cadar

2018-10-23	Move unrelated function from ReadExpr class	Martin Nowack

2018-10-23	Avoid unsafe static downcasts	Martin Nowack

2018-10-23	Modernize code	Martin Nowack
	* use `using` instead of typdef * use `collection.empty()` instead of size * use `auto` if clear * use `emplace_back` where useful * use `nullptr` instead of NULL * use `override` if applicable * use `explicit` for constructor to avoid implicit conversion
2018-10-23	Move optimization specific headers away from the project include directory	Martin Nowack
	Don't pollute the project include directory with optimization specific headers.
2018-10-23	Clean-up headers	Martin Nowack
	Remove unneeded headers from include files
2018-10-23	Remove condition check before function invocation	Martin Nowack
	Conditions are checked inside of `optimizeExpr()` anyway. This simplifies the code a lot.
2018-10-23	Move ConstantExpr check inside optimizeExpr function	Martin Nowack

2018-10-23	optimizeExpr: return the result as return value instead as function argument	Martin Nowack
	simplifies code a lot.
2018-10-23	Fixed compilation of array optimization patch with LLVM >= 4.0	Cristian Cadar

2018-10-23	Added missing headers and clang-format the files	Cristian Cadar

2018-10-23	Added support for KLEE value-based array optimization	Andrea Mattavelli

2018-10-23	Added support for KLEE index-based array optimization	Andrea Mattavelli

2018-06-29	Fix the final -Wimplicit-fallthrough warning	Daniel Schemmel

2018-06-29	Make ConstantExpr hashing function faster and modify affected test	Timotej Kapus

2018-05-24	isLSB should be a boolean, as it is only used in truth contexts	Daniel Schemmel

2018-05-09	Improve handling of constant array in Z3	Timotej Kapus

2017-10-04	Remove Autoconf/Makefile build system and adjust the TravisCI	Dan Liew
	configuration, TravisCI scripts and Dockerfile build appropriately. There are a bunch of clean ups this enables but this commit doesn't attempt them. We can do that in future commits.
2017-08-27	Remove unnecessary null pointer checks	Oscar Deits
	Fixes klee/klee#717 delete on null pointer is always safe.
2017-07-23	Remove support for LLVM < 3.4	Martin Nowack
	Request LLVM 3.4 as minimal requirement for KLEE
2017-06-12	llvm: don't use clEnumValEnd for LLVM 4.0	Jiri Slaby
	It became unnecessary when defining options and mainly undefined. So introduce KLEE_LLVM_CL_VAL_END as suggested by @delcypher. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2017-03-23	Add `AssignmentValidatingSolver`. It's purpose is to check any computed	Dan Liew
	assignments against the corresponding `Query` object and check the assignment evaluates correctly. This can be switched on using `-debug-assignment-validating-solver` on the command line.
2017-02-14	ReadExpr::create() was missing an opportunity to constant fold when handling ↵	Dan Liew
	constant arrays.
2016-11-28	Clean up `Expr::compare()` interface by	Dan Liew
	* Making `Expr::compre(const Expr&, ExprEquivSet)` private and moving its implementation into `Expr.cpp`. * Document `Expr::compare(const Expr&)`. This partially addresses #515 .