| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2024-02-27 | Extend toConstant() to take an additional boolean argument that decides ↵ | Cristian Cadar | |
| whether the expression is concretised. Also changed a C string argument to std::string. | |||
| 2024-02-27 | This commit fixes the concretization of arguments following an external call ↵ | Cristian Cadar | |
| with symbolic arguments. It also introduces a new external call policy, where the symbolic inputs are left unconstrained following such a call, useful for certain external calls such as printf. | |||
| 2024-02-19 | Rename --ptree-batch-size to --exec-tree-batch size, and ↵ | Cristian Cadar | |
| --compress-execution-tree to --compress-exec-tree. Fix an incorrect reference to --write-exec-tree. | |||
| 2024-02-17 | Fixed incorrect reference in ExternalCallWarnings | Cristian Cadar | |
| 2024-02-16 | drop llvm 9 and 10 | Daniel Schemmel | |
| 2024-02-08 | Use `std::` namespace for `uint64_t` | MartinNowack | |
| Co-authored-by: Daniel Schemmel <danielschemmel@users.noreply.github.com> (cherry picked from commit 5d9af025ee5a01b1650f11ed0612a10357a98308) | |||
| 2024-02-08 | Add support to `aligned_alloc` generated by LLVM | Martin Nowack | |
| Handle like `memalign` for now. | |||
| 2024-02-08 | Use APIs of newer LLVM versions instead of unsupported ones | Martin Nowack | |
| 2024-02-08 | Add support for opaque pointers | Martin Nowack | |
| 2024-01-30 | Change `GetConstraintLog` to work with `std::string`s instead of `char*`s | Daniel Schemmel | |
| 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 | 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-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 | 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-09-11 | Make KDAlloc the default memory allocator | 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-06 | rename Allocator::location_info to Allocator::locationInfo for | Daniel Schemmel | |
| consistency | |||
| 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 | SpecialFunctionHandler: use std::array for handlerInfo | Julian Büning | |
| 2023-06-09 | Fixed a format specifier pointed to by a compiler warning. | Cristian Cadar | |
| 2023-06-05 | make BatchingSearcher more readable | Julian Büning | |
| 2023-06-05 | fix BatchingSearcher's disabled time budget | Julian Büning | |
| The functionality of the batching searcher that increases the time budget if it is shorter than the time between two calls to `selectState()` ignored the disabled time budget. Effectively, the batching searcher thus picks a very arbitrary time budget on its own. | |||
| 2023-06-05 | CMake: use built-in FindSQLite3 module | Julian Büning | |
| available since CMake version 3.14 | |||
| 2023-05-26 | Improve error message when KDAlloc fails to create a mapping | Daniel Schemmel | |
| 2023-05-26 | Use unique_ptr for MemoryManager and avoid re-creating it in the first place | Martin Nowack | |
| No need to re-create and re-alloc all the memory again after execution. | |||
| 2023-04-21 | use unique_ptr all throughout the solver chain | Daniel Schemmel | |
| 2023-04-06 | Use newer C++ standard for KLEE's iterators; fixes deprecation warning | Martin Nowack | |
| 2023-04-06 | Support disabling compiler warnings; Use with external headers | Martin Nowack | |
| 2023-04-06 | Mark variable as potentially unused | Martin Nowack | |
| 2023-04-01 | remove include/klee/Support/IntEvaluation.h | Daniel Schemmel | |
| 2023-03-27 | Core/Executor: long double on i686 must be aligned to 4 bytes | Lukáš Zaoral | |
| According to i686 System V ABI 2.1.1, long double must be aligned to 4 bytes. Thus, its size with padding is 12 bytes. Prior to this change only 10 bytes were used. This commit fixes the following out of bound pointer access. ``` $ clang -m32 -O0 -Xclang -disable-O0-optnone -g -emit-llvm -c test/Feature/VarArgAlignment.c -o varalign.bc $ klee varalign.bc KLEE: output directory is "/home/lukas/klee/klee-out-19" KLEE: Using Z3 solver backend KLEE: WARNING: undefined reference to function: printf KLEE: WARNING ONCE: calling external: printf(44120064, 1, 2, 3) at test/Feature/VarArgAlignment.c:23 17 i1, i2, i3: 1, 2, 3 l1: 4 i4: 5 ld1: 6.000000 KLEE: ERROR: test/Feature/VarArgAlignment.c:35: memory error: out of bound pointer KLEE: NOTE: now ignoring this error at this location KLEE: done: total instructions = 499 KLEE: done: completed paths = 1 KLEE: done: generated tests = 1 ``` | |||
| 2023-03-23 | stats: add termination class stats | Frank Busse | |
| 2023-03-23 | stats: add branch type stats | Frank Busse | |
| 2023-03-23 | stats: rename States -> ActiveStates, add States | Frank Busse | |
| 2023-03-23 | stats: add Allocations | Frank Busse | |
| 2023-03-23 | stats: rename numQueries/Queries -> SolverQueries, add Queries | Frank Busse | |
| 2023-03-23 | stats: add ExternalCalls | Frank Busse | |
| 2023-03-23 | stats: add QCacheHits/Misses | Frank Busse | |
| 2023-03-23 | stats: add InhibitedForks | Frank Busse | |
 |
index : ~cnx/klee | |
| KLEE fork for patch differentiation testing |
| about summary refs log tree commit diff homepage |