Fix for the issue reported and diagnosed by Seungbeom, where KLEE was

skipping forks without reporting it.  Added a warning the first time a
fork is skipped for each of four different reasons.



git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73307 91177308-0d34-0410-b5e6-96231b3b80d8

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);