aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/Core/Executor.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Core/Executor.cpp')
-rw-r--r--lib/Core/Executor.cpp10
1 files changed, 10 insertions, 0 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 28e7111c..63d21c6e 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -730,6 +730,16 @@ Executor::fork(ExecutionState &current, ref<Expr> condition, bool isInternal) {
current.forkDisabled ||
inhibitForking ||
(MaxForks!=~0u && stats::forks >= MaxForks)) {
+
+ if (MaxMemoryInhibit && atMemoryLimit)
+ klee_warning_once(0, "skipping fork (memory cap exceeded)");
+ else if (current.forkDisabled)
+ klee_warning_once(0, "skipping fork (fork disabled on current path)");
+ else if (inhibitForking)
+ klee_warning_once(0, "skipping fork (fork disabled globally)");
+ else
+ klee_warning_once(0, "skipping fork (max-forks reached)");
+
TimerStatIncrementer timer(stats::forkTime);
if (theRNG.getBool()) {
addConstraint(current, condition);