| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2022-03-17 | remove obsolete KLEE_LLVM legacy defines | Julian Büning | |
| 2022-03-17 | remove LLVM < 6 from sources | Frank Busse | |
| 2021-12-20 | llvm13: llvm::APInt::toString has been moved to StringExtras.h | Lukas Zaoral | |
| See: https://reviews.llvm.org/D103888 | |||
| 2020-11-12 | Casting.h: isa_and_nonnull<> | Julian Büning | |
| 2020-11-12 | Ref: implement operator bool() | Julian Büning | |
| 2020-07-01 | Clean-up and add documentation | Martin Nowack | |
| 2020-07-01 | Separate constraint set and constraint manager | Martin Nowack | |
| 2020-07-01 | Move constraint implementation from header to cpp files | Martin Nowack | |
| 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 | |
 |
index : ~cnx/klee | |
| KLEE fork for patch differentiation testing |
| about summary refs log tree commit diff homepage |