| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | Changed use-after-free and double-free tests to expect KDAlloc, plus some ↵ | Cristian Cadar | |
| small improvements. | |||
| 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-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-05 | test/Feature/StackTraceOutput.c: relative checks, clang-format | Julian Büning | |
| 2023-06-05 | re-enable StackTraceOutput.c test | Julian Büning | |
| This test previously had a REQUIRES line with geq-llvm-7.0. Because LLVM version 7.0 is no longer "known" (test/lit.cfg), the required feature is not available and the test is discarded as unsupported by llvm-lit. | |||
| 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 | also check for default CHECK directive in ArrayOpt Tests | Matthis Gördel | |
| 2023-05-26 | Copy stats to test directory when running tests | Daniel Schemmel | |
| The sqlite3 databases used for the stats are journalled and potentially must be written to. Therefore, the sqlite3 driver used by `klee-stats` requires write permissions on the database files. By copying the stats files to the test directory, we can now compile and test an out-of-tree build without requiring any write permissions on the source folder at all. | |||
| 2023-05-26 | Refactored and fixed the code dealing with the entry point. | Cristian Cadar | |
| main() should not be processed if the entry point is a different function. This also fixes an abnormal termination when --entry-point and --libc=uclibc are used together (#1572) | |||
| 2023-04-21 | Tests: replaced "-data" and "-stat" by "_data" and "_stat" for consistency ↵ | Cristian Cadar | |
| with recent changes. | |||
| 2023-03-26 | tests: add some missing headers | Frank Busse | |
| 2023-03-23 | Remove model_version from the POSIX runtime, as we have never used it. | Cristian Cadar | |
| 2023-03-23 | tests: add Feature/KleeStatsTermClasses.c | Frank Busse | |
| 2023-03-23 | tests: add Feature/KleeStatsBranches.c | Frank Busse | |
| 2023-03-22 | Added more test cases for --entry-point. EntryPointMissing is currently ↵ | Cristian Cadar | |
| expected to fail. | |||
| 2023-03-22 | STP: add option to switch SAT solver: --stp-sat-solver and set default to ↵ | Frank Busse | |
| CryptoMinisat | |||
| 2023-03-22 | Change `llvm_map_components_to_libnames` to `llvm_config` CMake function | Martin Nowack | |
| With recent LLVM versions, this should allow to link against dynamic LLVM libraries. | |||
| 2023-03-22 | Remove hard to understand and debug pcregrep test | Cristian Cadar | |
| 2023-03-22 | Fixed typo | Martin Nowack | |
| 2023-03-22 | Handle fail of KLEE gracefully | Martin Nowack | |
| Under 64bit architecture, a ptr-error might be found. Ignore this for now. | |||
| 2023-03-22 | Explicitly check if 32bit support is enabled for testing | Martin Nowack | |
| Ignore test in the first place, if no 32bit is enabled. | |||
| 2023-03-20 | ConstantArrayExprVisitor: Fix detection of multiple array indices | Lukáš Zaoral | |
| Previously, the code did two consecutive checks. First one succeeded only if the given index was not already seen and the second one did an analogous check but for arrays. However, if the given index usage was already detected for some array, its usage for another array that already had some other index detected would be silently skipped and the `incompatible` flag would not be set. Therefore, if the code contained e.g. the following conditional jump on two arrays with two symbolic indices, the multi-index access would remain undetected: if ((array1[k] + array2[x] + array2[k]) == 0) Resulting in the following output: KLEE: WARNING: OPT_I: infeasible branch! KLEE: WARNING: OPT_I: successful | |||
| 2023-03-20 | llvm14: port test/Feature/VarArgByVal.c to LLVM 14 | Lukáš Zaoral | |
| LLVM 14 has introduced the noundef function argument attribute. | |||
| 2023-03-20 | llvm14: Add LLVM 14 to lit.cfg | Lukáš Zaoral | |
| 2023-03-17 | Don't fail `KleeStats.c` test if it takes 1s or longer | Martin Nowack | |
| 2023-03-17 | Disable `const_array_opt1` for ubsan as well | Martin Nowack | |
| 2023-03-17 | [cmake] Use LLVM's CMake functionality only | Martin Nowack | |
| LLVM became more complex, use LLVM's CMake functionality directly instead of replicating this behaviour in KLEE's build system. Use the correct build flags provided by LLVM itself. This is influenced by the way LLVM is built in the first place. Remove older CMake support (< 3.0). | |||
| 2023-03-16 | Add some system tests for KDAlloc | Daniel Schemmel | |
| 2023-03-16 | Integrate KDAlloc into KLEE | Daniel Schemmel | |
| 2023-02-28 | Add a few simple solver tests | Daniel Schemmel | |
| 2023-02-06 | Disable memcpy_chk_err.c on FreeBSD, where a call to __memcpy_chk is not ↵ | Cristian Cadar | |
| generated | |||
| 2023-02-06 | Add an extra check to test/Runtime/FreeStanding/memcpy_chk_err.c ensuring ↵ | Cristian Cadar | |
| that a call to __memcpy_chk is emitted | |||
| 2023-01-06 | fix output check in test const_arr_opt1 | Matthis Gördel | |
| 2022-12-09 | add missing FileCheck command to test | Matthis Gördel | |
| 2022-12-09 | fix FileCheck cmd of VarArgByVal test | Matthis Gördel | |
| 2022-09-26 | Improve the message for when large arrays become symbolic. Only print this ↵ | Cristian Cadar | |
| warning once per array. Add test case. | |||
| 2022-09-24 | Pass llvm.experimental.noalias.scope.decl to IntrinsicLowering so that it ↵ | Pavel | |
| strips out these intrinsics | |||
| 2022-09-14 | Improve pattern for FileCheck in UBSan's tests | Pavel | |
| 2022-09-14 | Improve pattern for FileCheck in UBSan's tests | Pavel | |
| 2022-09-14 | Eliminate .undefined_behavior.err category and simplify tests | Pavel | |
| 2022-09-14 | Remove LLVM version < 9 | Pavel | |
| 2022-09-14 | Check extensions of generated files in tests | Pavel | |
| 2022-09-14 | Remove LLVM version < 6 | Pavel | |
| 2022-09-14 | Support UBSan-enabled binaries | Pavel Yatcheniy | |
| 2022-07-24 | Support arguments of width 128, 256 and 512 bits for external calls | Pavel | |
| 2022-07-04 | Inline asm external call | Mikhail | |
| 2022-06-30 | rename CallSite to CallBase | Frank Busse | |
| 2022-06-30 | remove LLVM < 9 | Frank Busse | |
| 2022-06-27 | Fix error with empty EntryPoint | Saveliy Grigoryev | |
 |
index : ~cnx/klee | |
| KLEE fork for patch differentiation testing |
| about summary refs log tree commit diff homepage |