Age | Commit message (Collapse) | Author | |
---|---|---|---|
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 | 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-01-19 | Remove statistics limit from istats. | Martin Nowack | |
Statistics encoded in `run.istats` were limited to a maximum number of 13 due to encoding in a `uint64_t` variable. This approach has multiple limitations: - a maximum number of 13 statistics were allowed - a subtle bug can be triggered if many more statistics are added - independent of the selected statistics for `run.istats` Depending on the linking order, statistics will get a different ID. Previously, the ID was used to shift a `1` to its position marking the statistic as being used. This will lead to undefined behaviour if more than 63 statistics are used. Using an llvm::SmallBitVector instead fixes both problems. | |||
2020-01-13 | Assume assembly.ll is local to the run.istats file | Martin Nowack | |
Assuming a `klee-out-*` directory is moved to a different path location, subsequent analysis of the run.istats with KCachegrind focusing on assembly is impossible as the `assembly.ll` cannot be found. The reason is that the absolute path of the object file (assembly.ll) is hard-coded as part of the generated run.istats. To fix this, assume that the file is local to the `run.istats`. | |||
2019-12-13 | Remove unnecessary std::move's that prevent copy elision | 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-11-05 | Core: Executor, remove unused variable | Jiri Slaby | |
numSeeds is unused since commit 4eb050e2999b (ExecutorTimers: refactor and move to support lib), so remove it. | |||
2019-11-05 | Mark all constant global memory objects as constant | Martin Nowack | |
Fixes #264. We first aggregate all constant memory objects initialise them and initialise their counter parts in the concrete memory. After that, we mark memory objects as constant such that they can't be modified (i.e. this includes marking them symbolic). | |||
2019-11-04 | Remove the duplicated check for DebugInfoIntrinsic | Hui Peng | |
2019-10-31 | Executor: fix missing default case in switch instruction | Frank Busse | |
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-10-29 | ExecutorTimers: remove signalling, fix endless looping fork | Frank Busse | |
- adds -timer-interval threshold for timer checks - fixes #831 | |||
2019-10-08 | Executor.h: remove defined functions without implementation | Frank Busse | |
2019-09-20 | refactor PTree: use unique_ptr | Frank Busse | |
2019-09-20 | refactor PTree: remove split(), add attach() method | Frank Busse | |
2019-09-03 | Moved solver-related header files into a separate klee/Solver/ directory. | Cristian Cadar | |
2019-08-15 | ExecutorTimers: move dumpStates/dumpPTree into Executor | Frank Busse | |
* creates two new methods: dumpStates, dumpPTree | |||
2019-08-14 | Replace sprintf with snprintf throughout codebase | Cristian Cadar | |
2019-08-12 | StatsTracker: switch from TRUNCATE to WAL journal mode | Frank Busse | |
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-06-04 | fix some incorrect first lines | Julian Büning | |
2019-06-04 | make endif guard naming consistent | 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-05-31 | PTree: fix dump() method | Frank Busse | |
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-05-28 | Implement handling of the llvm.fabs intrinsic | Felix Rath | |
2019-04-04 | some minor refactorings | Frank Busse | |
2019-04-04 | Clean klee-stats, StatsTracker and cmake | Timotej Kapus | |
2019-04-04 | Change the .stats format into sqlite3 | Timotej Kapus | |
Improves querying of the .stats file, reduces its size, speeds up reads and writes and has better defined fail behaviour. | |||
2019-04-02 | Handle __assert() function as handleAssertFail. This assert variant is used ↵ | Gleb Popov | |
on FreeBSD | |||
2019-04-02 | Fix build of Executor.cpp on FreeBSD. | Gleb Popov | |
2019-03-21 | drop support for LLVM <= 3.7 | Julian Büning | |
2019-03-21 | remove obsolete macro KLEE_LLVM_GEP_TYPE | Julian Büning | |
2019-03-19 | Add support to assign debug instructions to optimised code | Martin Nowack | |
2019-03-19 | Use debugging information from newer LLVM versions | Martin Nowack | |
2019-03-19 | Refactor InstructionInfoTable | Martin Nowack | |
Better debug information | |||
2019-03-17 | run VerifierPass after optimization and instrumentation | Julian Büning | |
2019-03-16 | Added support for disabling --batch-instructions and --batch-time by setting ↵ | Cristian Cadar | |
them to 0 | |||
2019-03-15 | Placed option categories in the klee namespace and options in the anonymous ↵ | Cristian Cadar | |
namespace in Executor.cpp | |||
2019-03-15 | Placed --max-time in the termination category | Cristian Cadar | |
2019-03-15 | Categorized the options in SpecialFunctionHandler.cpp | Cristian Cadar | |
2019-03-15 | Added help message for --use-constant-arrays, and placed option in the ↵ | Cristian Cadar | |
constraint solving category | |||
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 | Reformatted options and headers in Executor.cpp and did a proofreading pass ↵ | Cristian Cadar | |
over all help messages. | |||
2019-03-15 | Added several options in Executor.cpp to the constraint solving category | Cristian Cadar | |