about summary refs log tree commit diff homepage
path: root/lib/Core/SpecialFunctionHandler.cpp
diff options
context:
space:
mode:
authorFrank Busse <bb0xfb@gmail.com>2023-03-24 21:14:02 +0000
committerMartinNowack <2443641+MartinNowack@users.noreply.github.com>2024-01-12 12:00:35 +0000
commit19b6ae578b0658115d15848604a28434845bb3e3 (patch)
tree31d52545929760ad725385bd1cdc1153b710fc75 /lib/Core/SpecialFunctionHandler.cpp
parentfc83f06b17221bf5ef20e30d9da1ccff927beb17 (diff)
downloadklee-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.cpp8
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);
   }