| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2023-04-06 | Mark variable as potentially unused | Martin Nowack | |
| 2023-04-01 | remove include/klee/Support/IntEvaluation.h | Daniel Schemmel | |
| 2023-03-27 | (gcc-13) include cstdint for *int*_t | Jiri Slaby | |
| Otherwise we see errors like this with gcc13: include/klee/Statistics/Statistic.h:31:10: error: no type named 'uint32_t' in namespace 'std' | |||
| 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 numQueries/Queries -> SolverQueries, add Queries | Frank Busse | |
| 2023-03-23 | remove obsolete header | Daniel Schemmel | |
| 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: PointerType::getElementType() was deprecated | Lukáš Zaoral | |
| ... for LLVM 14 in [1] and has already been removed from the LLVM 15 branch in [2]. Some changes are only temporary to silence the warning though, as Type::getPointerElementType() is planned to be removed as well. [3] [1] https://reviews.llvm.org/D117885/new/ [2] https://github.com/llvm/llvm-project/commit/d593cf7 [3] https://llvm.org/docs/OpaquePointers.html#migration-instructions | |||
| 2023-03-17 | Use bitcode library paths via config generation instead of `-D` flags | Martin Nowack | |
| 2023-03-16 | Add the KDAlloc allocator using both of its suballocators | Daniel Schemmel | |
| 2023-03-16 | The KDAlloc loh allocator is useful for variable sized (large) allocations | Daniel Schemmel | |
| 2023-03-16 | The KDAlloc slot allocator is useful for small sized allocations | Daniel Schemmel | |
| 2022-09-14 | Eliminate .undefined_behavior.err category and simplify tests | Pavel | |
| 2022-09-14 | Introduce separate categories for different kinds of undefined behavior | Pavel | |
| 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-07-04 | Fix memory leak in crosscheck core solver mechanism | Daniel Schemmel | |
| 2022-06-30 | remove LLVM < 9 | Frank Busse | |
| 2022-04-28 | Make Uclibc support a runtime option, not a compile-time one. | Gleb Popov | |
| 2022-04-25 | use mallinfo2 if available | Frank Busse | |
| 2022-03-17 | remove obsolete KLEE_LLVM legacy defines | Julian Büning | |
| 2022-03-17 | ADT/Ref.h: remove header | Frank Busse | |
| 2022-03-17 | remove LLVM < 6 from sources | Frank Busse | |
| 2022-03-17 | Document that GetTotalMallocUsage returns the usage in bytes | Cristian Cadar | |
| 2022-01-05 | introduce BranchTypes | Frank Busse | |
| 2021-12-23 | Introduce termination categories | Frank Busse | |
| Track all path terminations: esp. for debugging or visualising a persistent process tree (with or without full MoKlee integration) it is helpful to know the exact reason (StateTerminationType) why a path terminated. | |||
| 2021-05-04 | differentiate between partial and completed paths in summary and fix paths ↵ | Frank Busse | |
| stats when not dumping states | |||
| 2020-12-23 | klee.h: fix compiler warnings (function declaration is not a prototype) | Frank Busse | |
| 2020-11-12 | Casting.h: isa_and_nonnull<> | Julian Büning | |
| 2020-11-12 | Ref: implement operator bool() | Julian Büning | |
| 2020-11-04 | Link to the different runtime libraries depending on the application to test. | Martin Nowack | |
| Currently, only 32bit vs. 64bit is supported. | |||
| 2020-10-12 | Exception handling only for LLVM >= 8.0.0 | Julian Büning | |
| 2020-09-26 | Replace llvm::CallSite with llvm::CallBase on LLVM 8+ | Lukas Zaoral | |
| This is in preparation for LLVM 11 as the llvm:CallSite class has been removed. | |||
| 2020-08-19 | DiscretePDF: use IDs instead of pointers (see PR #739) | Frank Busse | |
| 2020-08-07 | New intrinsic: klee_is_replay | Alastair Reid | |
| This instrinsic detects whether the program is being executed symbolically or concretely (i.e., using the libkleeRuntest library). The intended usage (illustrated in the test program) is to allow the test program to display the input values by invoking any libraries it wants to. This is especially valuable if you are constructing complex, structured values and for languages like Rust (or C++) that have rich libraries and print libraries. For example, you might pick a symbolic value N with the assumption "0 <= N < 10" and then pick N symbolic values and write them to an array. The resulting ktest file is a bit hard to understand compared with the output of the standard print function in Rust/C++. | |||
| 2020-07-30 | introduce --rng-initial-seed=<unsigned> | Frank Busse | |
| * move global theRNG into Executor * pass theRNG via ctor to searchers * remove some type warnings from RNG.cpp Fixes #1023. | |||
| 2020-07-29 | remove holes in Instruction-/FunctionInfoTable, add documentation | Frank Busse | |
| 2020-07-01 | Clean-up and add documentation | Martin Nowack | |
| 2020-07-01 | Use constraint sets and separate metadata for timing solver invocation | Martin Nowack | |
| Decouple ExecutionState from TimingSolver Instead of providing an execution state to the timing solver use a set of constraints and an additional object for metadata. Fixes: * correct accounting of metadata to a specific state * accounting of all solver invocations (e.g. solver-getRange was not accounted) * allows to invoke the solver without a state (avoids costly copying of states/constraints) | |||
| 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 | Created include/klee/Core directory and moved appropriate files direc\ | Cristian Cadar | |
| tly in lib/Core | |||
| 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-04-08 | Statistic: slightly modernise class definition | Frank Busse | |
| 2020-04-08 | stats: remove queryConstructTime (unused) | Frank Busse | |
| 2020-02-19 | Use `ref<>` for MemoryObject handling | Martin Nowack | |
| This uses the `ref<>`-based memory handling of MemoryObjects. This makes it explicit that references are held in: - ExecutionState::symbolics - ObjectState | |||
 |
index : ~cnx/klee | |
| KLEE fork for patch differentiation testing |
| about summary refs log tree commit diff homepage |