Age | Commit message (Collapse) | Author | |
---|---|---|---|
2021-05-04 | differentiate between partial and completed paths in summary and fix paths ↵ | Frank Busse | |
stats when not dumping states | |||
2021-04-20 | Replaced the time-based delay after which the max-static-*-pct checks are ↵ | Cristian Cadar | |
performed with one expressed in terms of number of forks. | |||
2021-04-20 | Refactored maxStaticPctChecks into a sequence of conditions. | Cristian Cadar | |
2021-04-20 | Added a warning when forking is skipped due to MaxStatic*Pct limits being ↵ | Cristian Cadar | |
reached | |||
2021-04-20 | Added -max-static-pct-check-delay to replace the hardcoded delay after which ↵ | Cristian Cadar | |
the MaxStatic*Pct checks are performed. | |||
2021-04-20 | Refactored MaxStatis*Pct conditions into a separate function. | Cristian Cadar | |
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 |