about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
-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);