| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |||
| 2020-02-19 | Use `ref<>` for UpdateNode | Martin Nowack | |
| Remove additional reference counting as part of UpdateNodeList and UpdateNode. Simplifies code. | |||
| 2020-02-19 | Clean-up header files | Martin Nowack | |
| * Replace c header with c++ header * remove unneeded header file | |||
| 2020-02-19 | Add move assignment operator and move construct for `ref` class. | Martin Nowack | |
| 2020-02-19 | Add `ReferenceCounter` struct utilized by ref<> | Martin Nowack | |
| Using KLEE's `ref<>` shared ptr requires the referenced object to contain a reference counter to be added and initialised to 0 as part of the constructor. To support better reuse of the `ref<>` ptr add a `ReferenceCounter` struct. Just adding this struct to a new class/struct as member enables reference counting with `ref<>` - no additional counter management needed. | |||
| 2020-02-19 | Fix ptr reference invalidation if last reference gets freed before new ↵ | Martin Nowack | |
| reference assigned. | |||
| 2020-02-13 | Use call-by-reference for hash-function invocation | Martin Nowack | |
| 2020-02-13 | Replace old TR1 implementations of unordered_map/set with std::* versions | Martin Nowack | |
| TR1 implementation got replaced by the std::* equivalents with C++11. Start to use the standard versions instead of the old ones. | |||
| 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-11-07 | [expr-visitor] Remove unnecessary allocation | Timotej Kapus | |
| 2019-10-29 | ExecutorTimers: refactor and move to support lib | Frank Busse | |
| - moves timer handling from Executor into support lib - introduces TimerGroup, removes TimerInfo/WriteStatsTimer/UpdateReachableTimer/WriteIStatsTimer classes - removes ExecutorTimers.cpp and ExecutorTimerInfo.h - removes -max-instruction-time flag (see #1114) | |||
| 2019-09-03 | Moved solver-related header files into a separate klee/Solver/ directory. | Cristian Cadar | |
| 2019-07-30 | Use #include "klee/..." (instead of #include <klee/...>) consistently. | Cristian Cadar | |
| 2019-07-30 | Consolidated Expr-related include files into a single include/klee/Expr ↵ | Cristian Cadar | |
| directory. This improves the organization of the code, and also makes it easier to reuse Expr outside KLEE. | |||
| 2019-07-23 | Refactor ConstraintManager to more modern coding standards | Daniel Schemmel | |
| Eliminates -Wdeprecated-copy warnings Performed clang-format on touched file | |||
| 2019-06-04 | fix some incorrect first lines | Julian Büning | |
| 2019-06-04 | make endif guard naming consistent | Julian Büning | |
| 2019-06-04 | DiscretePdf.h: add include guards | Julian Büning | |
| 2019-06-04 | make include guard naming consistent | Julian Büning | |
| 2019-06-04 | Fixed identifiers used in ifdefs to (1) not use reserved names and (2) use a ↵ | Cristian Cadar | |
| consistent naming convention | |||
| 2019-06-04 | Remove parenthesis around returns, as reported and discussed in #891 | Cristian Cadar | |
| 2019-05-30 | ExecutionState: remove fnAliases | Julian Büning | |
| 2019-05-30 | remove klee_alias_function() | Julian Büning | |
| this function can be used to modify the control flow of the program on different paths, enabling self-modifying code. | |||
| 2019-04-02 | Do not take sys/capability.h header into account on FreeBSD. Also use ↵ | Gleb Popov | |
| libutil.h header there. | |||
| 2019-03-21 | drop support for LLVM <= 3.7 | Julian Büning | |
| 2019-03-21 | remove obsolete LegacyLLVMPassManagerTy | Julian Büning | |
| 2019-03-21 | remove obsolete macro KLEE_LLVM_GEP_TYPE | Julian Büning | |
| 2019-03-19 | Refactor InstructionInfoTable | Martin Nowack | |
| Better debug information | |||
| 2019-03-17 | Added libcxx flag | Lukas Wölfer | |
| 2019-03-17 | Renamed --use-cache to --use-branch-cache | Cristian Cadar | |
| 2019-03-17 | run VerifierPass after optimization and instrumentation | Julian Büning | |
| 2019-03-15 | Categorized the options in SpecialFunctionHandler.cpp | Cristian Cadar | |
| 2019-03-15 | Placed --exit-on-error, --max-tests and --watchdog in the termination category | Cristian Cadar | |
| 2019-03-15 | Renamed --seed-out to --seed-file and --seed-out-dir to --seed-dir, and ↵ | Cristian Cadar | |
| placed them in the seeding category. Moved options and option categories in Executor.cpp to the klee namespace. | |||
| 2019-03-15 | Created a new module-related option category and moved the options in ↵ | Cristian Cadar | |
| KModule.cpp in there | |||
 |
index : ~cnx/klee | |
| KLEE fork for patch differentiation testing |
| about summary refs log tree commit diff homepage |