From: Brian Norris <banorris@uci.edu>
Date: Wed, 23 Jan 2013 18:43:48 +0000 (-0800)
Subject: nodestack: pass writer ModelAction to add_future_value()
X-Git-Tag: oopsla2013~344
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=f10dc6ce67a97ab18423e7cedaa24961bf0d80dc;p=model-checker.git

nodestack: pass writer ModelAction to add_future_value()

NodeStack will have to know a little more about who wrote the future
value, so just pass the ModelAction as a parameter.
---

diff --git a/model.cc b/model.cc
index 017455d..97df9a2 100644
--- a/model.cc
+++ b/model.cc
@@ -857,7 +857,7 @@ void ModelChecker::add_future_value(const ModelAction *writer, ModelAction *read
 {
 	/* Do more ambitious checks now that mo is more complete */
 	if (mo_may_allow(writer, reader) &&
-			reader->get_node()->add_future_value(writer->get_value(),
+			reader->get_node()->add_future_value(writer,
 				writer->get_seq_number() + params.maxfuturedelay))
 		set_latest_backtrack(reader);
 }
diff --git a/nodestack.cc b/nodestack.cc
index 708ec3d..46f7d12 100644
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -225,8 +225,9 @@ bool Node::misc_empty() const
  * @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)
+bool Node::add_future_value(const ModelAction *writer, modelclock_t expiration)
 {
+	uint64_t value = writer->get_value();
 	int idx = -1; /* Highest index where value is found */
 	for (unsigned int i = 0; i < future_values.size(); i++) {
 		if (future_values[i].value == value) {
diff --git a/nodestack.h b/nodestack.h
index 55991c3..d2e6491 100644
--- a/nodestack.h
+++ b/nodestack.h
@@ -76,7 +76,7 @@ public:
 	 * occurred previously in the stack. */
 	Node * get_parent() const { return parent; }
 
-	bool add_future_value(uint64_t value, modelclock_t expiration);
+	bool add_future_value(const ModelAction *writer, modelclock_t expiration);
 	struct future_value get_future_value() const;
 	bool increment_future_value();
 	bool future_value_empty() const;