Age | Commit message (Collapse) | Author | |
---|---|---|---|
2021-03-04 | [Z3] Handle the case when interruption caught by Z3 | Pavel Yatcheniy | |
2021-02-16 | Executor: remove obsolete special case for __cxa_{re,}throw | Julian Büning | |
__cxa_throw and __cxa_rethrow were not handled by special function handlers in the final version of #966 (which introduced support for C++ exception handling) | |||
2021-02-16 | add ifdefs for C++ exception handling | Julian Büning | |
restoring old behavior without EH support | |||
2020-12-04 | llvm11: CallBase::getParamAlignment has been deprecated | Lukas Zaoral | |
and should be replaced with CallBase::getParamAlign | |||
2020-12-04 | llvm11: GlobalValue::getAlignment has been removed | Lukas Zaoral | |
See: https://reviews.llvm.org/D80368 | |||
2020-12-04 | llvm11: IPConstantPropagationPass has been removed | Lukas Zaoral | |
See: https://reviews.llvm.org/D84447 | |||
2020-12-04 | llvm11: Composite and Sequential types were removed | Lukas Zaoral | |
See: https://reviews.llvm.org/D75660 https://reviews.llvm.org/D75661 | |||
2020-12-04 | llvm11: Use getCalledOperand instead of getCalledValue | Lukas Zaoral | |
CallBase::getCalledValue has been deprecated by getCalledOperand since LLVM 8 and has been removed in LLVM 11 See: https://reviews.llvm.org/D78882 | |||
2020-12-04 | llvm11: Make conversions from StringRef to std::string explicit | Lukas Zaoral | |
The same applies to SmallString. See: llvm/llvm-project@777180a#diff-497ba4c0c527a125d382b51a34f32542 | |||
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-21 | fix Executor: remove UB from bindInstructionConstants | Julian Büning | |
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 | MergingSearcher: remove random-path incompatibility | Frank Busse | |
2020-10-12 | searchers: clean up, add documentation | Frank Busse | |
2020-10-12 | address MartinNowack's remaining feedback | Julian Büning | |
2020-10-12 | Exception handling only for LLVM >= 8.0.0 | Julian Büning | |
2020-10-12 | use isa<> and explicit nullptr-check for compilation with older LLVM ↵ | Felix Rath | |
versions, also mark two errors as ExecErrors, as these should not be caused by users | |||
2020-10-12 | Implemented support for C++ Exceptions | Felix Rath | |
We implement the Itanium ABI unwinding base-API, and leave the C++-specific parts to libcxxabi. Co-authored-by: Lukas Wölfer <lukas.woelfer@rwth-aachen.de> | |||
2020-10-09 | implement fneg instruction | Julian Büning | |
2020-10-09 | fix: fabs() working on the wrong argument | David Laprell | |
2020-10-09 | Replace `NULL` with explicit `nullptr` | Martin Nowack | |
2020-10-09 | Explicitly track global variables in getDirectCallTarget | Martin Nowack | |
Global variables can't be a direct call target. Their values are read and treated as indirect call targets. | |||
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-09-03 | Guard process-tree compression with a command-line switch | Sebastian Poeplau | |
2020-09-03 | Fix PTree::remove to clean the tree properly | Sebastian Poeplau | |
The previous version left unnecessary intermediate nodes behind, sometimes leading to very long paths in the tree. | |||
2020-09-02 | More robust handling of unknown intrinsics | Alastair Reid | |
- If an unknown intrinsic appears in the bitcode file, it is reported but execution can proceed. - If an unknown intrinsic is encountered during execution of some path, - the intrinsic is reported - this path is treated as an error - execution of other paths can proceed To be more precise, there is a list of "known unknown intrinsics". Intrinsics not on this list will prevent execution. | |||
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-29 | remove holes in Instruction-/FunctionInfoTable, add documentation | Frank Busse | |
2020-07-01 | Clean-up and add documentation | Martin Nowack | |
2020-07-01 | Remove state contructor with constraints | Martin Nowack | |
This constructor has been a hack and was wrongly used, use ConstraintManager instead. Allow copy-constructing states only via `ExecutionState::branch()` call. | |||
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 | Use `unique_ptr` for solver in timing solver | Martin Nowack | |
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-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-06-29 | Implement fshr/fshl intrinsics | Alastair Reid | |
Changes: - IntrinsicCleaner accepts fshr/fshl as accepted intrinsics - Executor::executeCall converts fshr/fshl to urem/zext/concat/shift/extract - Klee/main suppresses warnings about externals that are LLVM reserved (i.e., begin with "llvm.") - New test exercises 32 and 7 bit versions including oversize shift values Test values are based on LLVM's test for fshl/fshr - Changes that depend on existence of fshr/fshl are guarded by #if LLVM_VERSION_CODE >= LLVM_VERSION(7, 0) or ; REQUIRES: geq-llvm-7.0 | |||
2020-06-25 | Enforce fork/branch limits in branch() and fix double termination | Frank Busse | |
* extend help messages for -max-memory and -max-memory-inhibit * introduces branchingPermitted() * enforces fork/branch limits in branch() (vector version) * changes main loop * calls updateStates() before checkMemoryUsage() * calls updateStates() again in case we early terminate states This should prevent double termination for now. Other solutions are imho more expensive as we would have to compare possibly large vectors of states (either states(arr) in checkMemoryUsage() or removedStates in terminateState()). | |||
2020-06-25 | fix Executor: initializeGlobalAliases | Julian Büning | |
2020-06-25 | Executor: consolidate initialization of global objects | Julian Büning | |
2020-06-25 | Executor: light refactoring of {allocate,initialize}GlobalObjects | Julian Büning | |
mainly range-based for, code deduplication | |||
2020-06-25 | Executor: split initializeGlobals | Julian Büning | |
2020-06-25 | ExecutorUtil: assert that GlobalValue is already known | Julian Büning | |