diff options
author | Frank Busse <bb0xfb@gmail.com> | 2023-03-24 21:14:02 +0000 |
---|---|---|
committer | MartinNowack <2443641+MartinNowack@users.noreply.github.com> | 2024-01-12 12:00:35 +0000 |
commit | 19b6ae578b0658115d15848604a28434845bb3e3 (patch) | |
tree | 31d52545929760ad725385bd1cdc1153b710fc75 /lib/Core/SpecialFunctionHandler.cpp | |
parent | fc83f06b17221bf5ef20e30d9da1ccff927beb17 (diff) | |
download | klee-19b6ae578b0658115d15848604a28434845bb3e3.tar.gz |
new: persistent ptree (-write-ptree) and klee-ptree
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.
Diffstat (limited to 'lib/Core/SpecialFunctionHandler.cpp')
-rw-r--r-- | lib/Core/SpecialFunctionHandler.cpp | 8 |
1 files changed, 2 insertions, 6 deletions
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index 488fba51..4589471c 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -480,12 +480,8 @@ void SpecialFunctionHandler::handleAssume(ExecutionState &state, state.constraints, e, res, state.queryMetaData); assert(success && "FIXME: Unhandled solver failure"); if (res) { - if (SilentKleeAssume) { - executor.terminateState(state); - } else { - executor.terminateStateOnUserError( - state, "invalid klee_assume call (provably false)"); - } + executor.terminateStateOnUserError( + state, "invalid klee_assume call (provably false)", !SilentKleeAssume); } else { executor.addConstraint(state, e); } |