| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2024-02-08 | Disable unsupported passes for newer LLVM versions | Martin Nowack | |
| Similar functionality needs to be added using a new pass manager | |||
| 2024-02-08 | Add support to `aligned_alloc` generated by LLVM | Martin Nowack | |
| Handle like `memalign` for now. | |||
| 2024-02-08 | Add support for `Intrinsic::get_rounding` for LLVM 16 | Martin Nowack | |
| `Intrinsic::flt_rounds` got removed | |||
| 2024-02-08 | Use APIs of newer LLVM versions instead of unsupported ones | Martin Nowack | |
| 2024-02-08 | Fix test case: using unsupported `CHECK_NEXT` instead of `CHECK-NEXT` | Martin Nowack | |
| 2024-02-08 | Fix test cases to support opaque pointers | Martin Nowack | |
| 2024-02-08 | Add support for opaque pointers | Martin Nowack | |
| 2024-02-08 | Explicitly enable opaque pointer support for LLVM 15 | Martin Nowack | |
| This automatically lifts old-style pointers to opaque pointers. More recent versions use opaque pointers automatically and do not need an explicit enabling. | |||
| 2024-02-08 | Explicitly build KLEE's exception handling runtime with C++11 | Martin Nowack | |
| Currently, we assume C++11 support being used to by the tested software. This needs to change if newer C++ standards should be supported. | |||
| 2024-02-08 | Assume C compiler's default standard is `-std=gnu17` | Martin Nowack | |
| Newer compilers use `-std=gnu17` as the default when compiling C code. Fix all the test cases that violate this behaviour or explicitly request older standards `-std=c89` where necessary. | |||
| 2024-02-08 | Use KLEE's uClibc v1.4 as default to support the compilation with newer ↵ | Martin Nowack | |
| compilers | |||
| 2024-02-08 | Refactor invocation of old pass manager into legacy function | Martin Nowack | |
| 2024-02-08 | Fix `klee_eh_cxx.cpp` compiler error | Martin Nowack | |
| 2024-02-08 | Fix `klee-libc/memchr.c` compiler warning | Martin Nowack | |
| 2024-02-08 | Replace `%libcxx_include` with `%libcxx_includes` for multi-include directories | Martin Nowack | |
| To support multiple include directories for c++ header files, use `%libcxx_includes`. This string contains the `-I` compiler directive for each include path as well. Update test cases to use new directive. | |||
| 2024-02-08 | Add support for newer `libc++`; Simplify path detection | Martin Nowack | |
| `libc++` include headers are now split between platform dependent and platform independent code. Before, only include files for the platform independent code were considered. Add support to automatically find platform dependent includes as well. Simplify the detection of libraries and paths. Instead of pointing to the `v1` directory, pointing to the include directory for `-DKLEE_LIBCXX_INCLUDE_PATH` is enough. Update build script to support this as well. | |||
| 2024-02-08 | MERGE libc++ build system | Martin Nowack | |
| 2024-02-08 | Add support to build newer LLVM versions | Martin Nowack | |
| `-DLLVM_ENABLE_PROJECTS` does not include runtimes anymore, instead a `-DLLVM_ENABLE_RUNTIMES` should be used in addition | |||
| 2024-01-30 | Change `GetConstraintLog` to work with `std::string`s instead of `char*`s | Daniel Schemmel | |
| 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 | |||
| 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 | |
 |
index : ~cnx/klee | |
| KLEE fork for patch differentiation testing |
| about summary refs log tree commit diff homepage |