~cnx/klee - KLEE fork for patch differentiation testing

Age	Commit message (Collapse)	Author
2024-01-30	Avoid generating array names in solver builders that could accidently collide	Martin Nowack
	If an array name ended with a number, adding a number-only suffix could generate the same name used as part of the solvers. In the specific testcase `val_1` became solver array `val_111` which collided with array `val_11` that became `val_111` as well. Using an `_` as prefix for the suffix, solves that problem in general, i.e. `val_1` becomes `val_1_11` and `val_11` becomes `val_11_1`. Fixes #1668
2022-06-28	Implement getArrayForUpdate iteratively	Daniel Schemmel

2020-05-01	[Solver:STP] Fix handling of array names	Martin Nowack
	Array names used for STP queries used to be restricted to 32 characters, with the last characters replaced by a unique number. Similarly, an array is made unique by `klee_make_symbolic`. Unfortunately, both combined can lead to the generation of the same STP array name for different arrays. This leads to wrong queries with invalid results. This is more likely be triggered with longer names for `klee_make_symbolic` Fixes #1257
2020-04-30	Removed include/klee/util and moved header files to appropriate places	Cristian Cadar

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-09-03	Moved solver-related header files into a separate klee/Solver/ directory.	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-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
2018-05-09	Improve handling of constant array in Z3	Timotej Kapus

2017-06-01	[Z3] Remove unused include.	Dan Liew

2017-06-01	[Z3] Implement API logging.	Dan Liew
	Add `-debug-z3-log-api-interaction` option to allow Z3 API calls to be logged to a file. The files logged by this option can be replayed by the `z3` binary (using its `-log` option). This is incredibly useful because it allows to exactly replay Z3's behaviour outside of KLEE.
2017-06-01	[Z3] Move the `dump()` methods of the Z3NodeHandle<> specializations	Dan Liew
	into `Z3Builder.cpp` so they can be called from in gdb.
2017-06-01	[Z3] Add assertions in Z3 builder to catch underflow with bad widths.	Dan Liew

2016-04-09	Generate unique STP and Z3 array names deterministically	Martin Nowack

2016-02-14	Handle Z3 API change between 4.4.1 and the current master branch	Dan Liew
	for the ``Z3_get_error_msg()`` function.
2016-02-14	Add basic implementation of Z3Builder and Z3Solver and Z3SolverImpl	Dan Liew
	which is based on the work of Andrew Santosa (see PR #295) but fixes many bugs in that implementation. The implementation communicates with Z3 via it's C API. This implementation is based of the STPSolver and STPBuilder and so it inherits a lot of its flaws (See TODOs and FIXMEs). I have also ripped out some of the optimisations (constructMulByConstant, constructSDivByConstant and constructUDivByConstant) that were used in the STPBuilder because * I don't trust them * Z3 can probably do these for us in the future if we use the ``Z3_simplify()`` At a glance its performance seems worse than STP but future work can look at improving this.