| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2024-01-12 | Renamed 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-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-04-06 | Support disabling compiler warnings; Use with external headers | Martin Nowack | |
| 2020-10-12 | searchers: more consistent formatting | Frank Busse | |
| 2020-10-12 | DFS/BFS/RandomSearcher: replace loop with std::find | Frank Busse | |
| 2020-10-12 | searchers: move implementations from .h to .cpp | Frank Busse | |
| 2020-10-12 | Searcher: remove addState/removeState functions | Frank Busse | |
| 2020-10-12 | searchers: clean up, add documentation | Frank Busse | |
| 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-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-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-06-29 | Enable subsets for RandomPathSearcher | Timotej Kapus | |
| 2020-06-29 | [PTree] Replace left/right with PointerIntPair | Timotej Kapus | |
| 2020-06-29 | Revert "refactor PTree: use unique_ptr" | Timotej Kapus | |
| This reverts commit 0aed7731210d0eb41c0ea767edb8067130cf6252. | |||
| 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 | Created include/klee/Core directory and moved appropriate files direc\ | Cristian Cadar | |
| tly in lib/Core | |||
| 2020-04-30 | Removed the Internal directory from include/klee | Cristian Cadar | |
| 2019-12-12 | [Searchers] Remove weight from es, add nurs_depth | Timotej Kapus | |
| Having both weight and depth in execution state is wasteful, therefore this patch removes weight. The nurs:depth searcher is replaced by nurs:rp, which uses pow to compute the weight A new nurs:depth searcher is introduced that biases the search with depth, making it the only other searcher that prefers to go deep (similar to dfs). | |||
| 2019-11-28 | Move merging related code from Executor into MergingSearcher | Lukas Wölfer | |
| Co-authored-by: Felix Rath <felix.rath@comsys.rwth-aachen.de> | |||
| 2019-09-20 | refactor PTree: use unique_ptr | Frank Busse | |
| 2019-09-20 | refactor PTree: remove split(), add attach() method | Frank Busse | |
| 2019-03-21 | drop support for LLVM <= 3.7 | Julian Büning | |
| 2019-03-16 | Added support for disabling --batch-instructions and --batch-time by setting ↵ | Cristian Cadar | |
| them to 0 | |||
| 2019-03-12 | time: add double type for span multiplications | Frank Busse | |
| 2018-10-30 | Base time API upon std::chrono | Frank Busse | |
| This should not change the behaviour of KLEE and mimics the old API. - functions moved from util into time namespace - uses time points and time spans instead of double - CLI arguments now have the form "3h5min8us" Changed command line parameters: - batch-time (double to string) - istats-write-interval (double to string) - max-instruction-time (double to string) - max-solver-time (double to string) - max-time (double to string) - min-query-time-to-log (double to string) - seed-time (double to string) - stats-write-interval (double to string) - uncovered-update-interval (double to string) - added: log-timed-out-queries (replaces negative max-solver-time) | |||
| 2018-07-04 | Fix compiler warnings if assertions are disabled | Martin Nowack | |
| 2018-05-15 | Implemented incomplete merging | Lukas Wölfer | |
| 2017-11-30 | Implemented bounded merging functionality | Lukas Wölfer | |
| 2017-10-15 | Fixed assert in BFSSearcher that does not hold as part of interleaved searcher | Julian Büning | |
| 2017-10-03 | Silenced some warnings about unused variables when assertions are disabled. | Cristian Cadar | |
| 2017-08-04 | Removed merging searchers | Lukas Wölfer | |
| 2017-07-23 | Remove support for LLVM < 3.4 | Martin Nowack | |
| Request LLVM 3.4 as minimal requirement for KLEE | |||
| 2017-05-24 | Remove redundant KLEE prefix while logging | Jörg Thalheim | |
| 2016-11-19 | Merge branch 'fix_bfs2' of https://github.com/MartinNowack/klee into ↵ | Cristian Cadar | |
| MartinNowack-fix_bfs2 | |||
| 2016-11-09 | Fix BFS searcher | Martin Nowack | |
| For performance reasons, if KLEE branches, one state is reused and it is progressed by adding new constraints. Make sure both new states end up at the end of the BFS searcher queue. | |||
| 2016-11-08 | add nicer error messages for --use-merge and add explanation why it ↵ | Hoang M. Le | |
| currently cannot be used with random-path | |||
| 2016-09-26 | Modified logging information to steer the usage of klee_message, ↵ | Andrea Mattavelli | |
| klee_warning, and klee_error | |||
| 2016-07-08 | Use vector instead of set to add/remove states | Martin Nowack | |
| Deterministic adding/removing of states. | |||
| 2016-07-08 | IterativeDeepeningTimeSearcher: Fix using wrong iterator | Martin Nowack | |
| 2015-12-17 | Refactoring: Moving klee_warning/_error functions to ErrorHandling in ↵ | Martin Nowack | |
| Support directory | |||
| 2014-09-14 | [LLVM3.5] Update for move of CFG.h into IR. | Daniel Dunbar | |
| - Mostly fixed by removing unnecessary references. | |||
| 2014-09-14 | [LLVM3.5] Update for CallSite.h move into IR/. | Daniel Dunbar | |
| 2014-05-29 | Refactoring from std::ostream to llvm::raw_ostream | Martin Nowack | |
| According to LLVM: lightweight and simpler implementation of streams. | |||
| 2014-04-24 | Removed ununsed Executor field in WeightedRandomSearcher to silence | Dan Liew | |
| clang warning. | |||
| 2013-08-27 | Port to LLVM 3.3 | Martin Nowack | |
| Major changes are: - Switching to llvm-link to build archive files - Use GetMallocUsage instead of GetTotalMemoryUsage (be aware of bug in LLVM 3.3 http://llvm.org/bugs/show_bug.cgi?id=16847) - intrinsic library functions like memcpy/mov/set use weak linkage to be replaced by e.g. uclibc functions - rewrote linking with library - enhanced MemoryLimit test case to check if mallocs were successful | |||
| 2013-07-23 | BFS searcher. | Lei Zhang | |
| 2010-07-15 | Reduce variable shadowing. | Daniel Dunbar | |
| git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@108405 91177308-0d34-0410-b5e6-96231b3b80d8 | |||
 |
index : ~cnx/klee | |
| KLEE fork for patch differentiation testing |
| about summary refs log tree commit diff homepage |