Enforce fork/branch limits in branch() and fix double termination

* extend help messages for -max-memory and -max-memory-inhibit
* introduces branchingPermitted()
* enforces fork/branch limits in branch() (vector version)
* changes main loop
  * calls updateStates() before checkMemoryUsage()
  * calls updateStates() again in case we early terminate states

This should prevent double termination for now. Other solutions are
imho more expensive as we would have to compare possibly large
vectors of states (either states(arr) in checkMemoryUsage() or
removedStates in terminateState()).

1 files changed, 7 insertions, 1 deletions

diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index 7acbc60f..d27fa503 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -436,7 +436,13 @@ private:
                                     ref<Expr> e,
                                     ref<ConstantExpr> value);
 
-  void checkMemoryUsage();
+  /// check memory usage and terminate states when over threshold of -max-memory + 100MB
+  /// \return true if below threshold, false otherwise (states were terminated)
+  bool checkMemoryUsage();
+
+  /// check if branching/forking is allowed
+  bool branchingPermitted(const ExecutionState &state) const;
+
   void printDebugInstructions(ExecutionState &state);
   void doDumpStates();