X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=nodestack.cc;h=f73d4cf4a154e264ed93a32f250c6a0f6dfaa11a;hp=743cb864452589f615d937220fe9440bf8bad093;hb=5d5b4d719178c48c3e5f616b5eb61b7d68dc2b49;hpb=174ad8165eeeb78fb4da391be331a26da044641f

diff --git a/nodestack.cc b/nodestack.cc
index 743cb86..f73d4cf 100644
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -192,8 +192,13 @@ bool Node::misc_empty() {
 
 
 /**
- * Adds a value from a weakly ordered future write to backtrack to.
+ * Adds a value from a weakly ordered future write to backtrack to. This
+ * operation may "fail" if the future value is already set (with a later
+ * expiration), or if the futurevalues set has reached its maximum.
+ * @see model_params.maxfuturevalues
+ *
  * @param value is the value to backtrack to.
+ * @return True if the future value was successully added; false otherwise
  */
 bool Node::add_future_value(uint64_t value, modelclock_t expiration) {
 	int suitableindex=-1;
@@ -211,7 +216,12 @@ bool Node::add_future_value(uint64_t value, modelclock_t expiration) {
 		future_values[suitableindex].expiration=expiration;
 		return true;
 	}
-	struct future_value newfv={value, expiration};
+
+	if (model->params.maxfuturevalues > 0 &&
+			(int)future_values.size() >= model->params.maxfuturevalues)
+		return false;
+
+	struct future_value newfv = {value, expiration};
 	future_values.push_back(newfv);
 	return true;
 }