| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2024-01-30 | Modify getValueFromSeeds() to include more functionality and simplify its ↵ | Cristian Cadar | |
| callers | |||
| 2024-01-30 | Make Assignment::evaluate be const | Cristian Cadar | |
| 2024-01-30 | Add checks to the seed concretization tests about the expected number of queries | Cristian Cadar | |
| 2024-01-30 | Added a test for --allow-seed-extension | Cristian Cadar | |
| 2024-01-30 | Removed --zero-seed-extension, and merge it with --allow-seed-extension. ↵ | Cristian Cadar | |
| This reworked logic also fixes a buffer overflow which could be triggered during seed extension. | |||
| 2024-01-30 | Refactored some code related to seeding. | Cristian Cadar | |
| 2024-01-30 | On a symbolic allocation, retrieve size from a seed, if available | Cristian Cadar | |
| 2024-01-30 | Concretize arguments to external function calls using seeds, if available. ↵ | Cristian Cadar | |
| Added a test case. | |||
| 2024-01-30 | Concretize constants using seed values, when available. Added two tests (w/ ↵ | Cristian Cadar | |
| and w/o seed extension) based on FP concretization. | |||
| 2024-01-30 | Switch to FreeBSD 14 and 13.2; Use LLVM 13 | Martin Nowack | |
| 2024-01-12 | Remove check for the number of solver queries | Tomasz Kuchta | |
| 2024-01-12 | Make test more deterministic | Tomasz Kuchta | |
| 2024-01-12 | Follow-up: applied review comments, implemented meta-data cleanup (one more ↵ | Tomasz Kuchta | |
| map added to ExecutionState); now storing addresses of MemoryObjects for easier cleanup | |||
| 2024-01-12 | Feature: implement single memory object resolution for symbolic addresses. | Tomasz Kuchta | |
| This feature implements tracking of and resolution of memory objects in the presence of symbolic addresses. For example, an expression like the following: int x; klee_make_symbolic(&x, sizeof(x), "x"); int* tmp = &b.y[x].z; For a concrete array object "y", which is a member of struct "b", a symbolic offset "x" would normally be resolved to any matching memory object - including the ones outside of the object "b". This behaviour is consistent with symbex approach of exploring all execution paths. However, from the point of view of security testing, we would only be interested to know if we are still in-bounds or there is a buffer overflow. The implemented feature creates and tracks (via the GEP instruction) the mapping between the current symbolic offset and the base object it refers to: in our example we are able to tell that the reference should happen within the object "b" (as the array "y" is inside the same memory blob). As a result, we are able to minimize the symbolic exploration to only two paths: one within the bounds of "b", the other with a buffer overflow bug. The feature is turned on via the single-object-resolution command line flag. A new test case was implemented to illustrate how the feature works. | |||
| 2024-01-12 | Renamed PTree to ExecutionTree (and similar) | Cristian Cadar | |
| 2024-01-12 | Rename files from PTree to ExecutionTree (and similar) | Cristian Cadar | |
| 2024-01-12 | SearcherTest: remove redundant root init, fix branch type | Frank Busse | |
| 2024-01-12 | new: persistent ptree (-write-ptree) and klee-ptree | Frank Busse | |
| Introduce three different kinds of process trees: 1. Noop: does nothing (e.g. no allocations for DFS) 2. InMemory: same behaviour as before (e.g. RandomPathSearcher) 3. Persistent: similar to InMemory but writes nodes to ptree.db and tracks information such as branch type, termination type or source location (asm) in nodes. Enabled with -write-ptree ptree.db files can be analysed/plotted with the new "klee-ptree" tool. | |||
| 2023-10-23 | replace deprecated (as of c++20) std::is_pod with std::trivial && ↵ | Daniel Schemmel | |
| std::is_standard_layout | |||
| 2023-09-11 | Make KDAlloc the default memory allocator | Cristian Cadar | |
| 2023-09-11 | Changed use-after-free and double-free tests to expect KDAlloc, plus some ↵ | Cristian Cadar | |
| small improvements. | |||
| 2023-09-07 | Remove broken experimental optimisation for validity (--cex-cache-exp) | Cristian Cadar | |
| 2023-07-21 | Add code to only keep in the --help menu the KLEE/Kleaver option categories | Cristian Cadar | |
| 2023-07-21 | Move some options to the klee namespace and declare them in OptionCategories.h | Cristian Cadar | |
| 2023-07-12 | Replaced --suppress-external-warnings and --all-external-warnings with ↵ | Cristian Cadar | |
| --external-call-warnings=none|once-per-function|all. This eliminates the ambiguity when both of the old options were set. Added test for the new option. | |||
| 2023-07-10 | remove timings from kdalloc tests | Daniel Schemmel | |
| 2023-07-10 | Simplify KDAlloc tests | Daniel Schemmel | |
| 2023-07-08 | Combine all `ConstantExpr::toMemory` cases into one. | Daniel Schemmel | |
| Note that (as it did previously), this relies on the native types having the same internal representation as the ApInt type. | |||
| 2023-07-08 | Using std::memcpy prevents alignment problems and removes an unnecessary ↵ | Daniel Schemmel | |
| special case | |||
| 2023-07-06 | Implement getLocationInfo in the same style as getSize | Daniel Schemmel | |
| 2023-07-06 | Have CoWPtr::get and CoWPtr::getOwned return pointers instead of references | Daniel Schemmel | |
| 2023-07-06 | rename Allocator::location_info to Allocator::locationInfo for | Daniel Schemmel | |
| consistency | |||
| 2023-07-06 | Perform location_info tests in KDAlloc's random test | Daniel Schemmel | |
| 2023-06-26 | RefTest: suppress -Wself-move | Julian Büning | |
| This warning (introduced with GCC 13, also present in clang) warns precisely about what we want to test here. | |||
| 2023-06-26 | Consistently use ".ktest" when referring to .ktest files in the help menu | Cristian Cadar | |
| 2023-06-26 | Remove parentheses around klee_ intrinsics from the help menu | Cristian Cadar | |
| 2023-06-26 | Fixed a couple of spelling issues in the help menu | Cristian Cadar | |
| 2023-06-26 | Improved help message for --exit-on-error-type=Abort | Cristian Cadar | |
| 2023-06-11 | Rewrote has_permission in the POSIX runtime. We now only return with ↵ | Cristian Cadar | |
| permission error a single time in symbolic execution mode. The rewrite also fixes a bug reported in #1230. Rewrote the FilePerm.c test accordingly. | |||
| 2023-06-11 | SpecialFunctionHandler: use std::array for handlerInfo | Julian Büning | |
| 2023-06-11 | fix ktest-randgen: use after free | Julian Büning | |
| 2023-06-09 | Fixed a format specifier pointed to by a compiler warning. | Cristian Cadar | |
| 2023-06-07 | Changed version to 3.1-pre | Cristian Cadar | |
| 2023-06-07 | Release notes for KLEE 3.0 v3.0 3.0.x | Cristian Cadar | |
| 2023-06-07 | Set version number to 3.0 | Cristian Cadar | |
| 2023-06-07 | Fixed end date in the 2.3 release notes | Cristian Cadar | |
| 2023-06-07 | Build and push Docker image as part of a release | Martin Nowack | |
| 2023-06-07 | Use recommended LLVM 13 as part of the Docker image | Martin Nowack | |
| 2023-06-07 | unittests/CMakeLists.txt: set gtest include dir only if necessary | Julian Büning | |
| 2023-06-07 | unittests/CMakeLists.txt: do not echo GTEST_SRC_DIR on error | Julian Büning | |
| This prevents the error message to include the internal "GTEST_SRC_DIR-NOTFOUND" value. | |||
 |
index : ~cnx/klee | |
| KLEE fork for patch differentiation testing |
| about summary refs log tree commit diff homepage |