nodestack: eliminate get_future_value_expiration()

[model-checker.git] / nodestack.cc

diff --git a/nodestack.cc b/nodestack.cc
index a4d2b1a491a989cb094f8709d2d3ca19e2687b0e..708ec3d0f5fa3da43a563228ef53c4b6e72475dd 100644 (file)
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -381,20 +381,14 @@ void Node::add_read_from(const ModelAction *act)
 }
 
 /**
- * Gets the next 'future_value' value from this Node. Only valid for a node
- * where this->action is a 'read'.
+ * Gets the next 'future_value' from this Node. Only valid for a node where
+ * this->action is a 'read'.
  * @return The first element in future_values
  */
-uint64_t Node::get_future_value() const
-{
-       ASSERT(future_index >= 0 && future_index < ((int)future_values.size()));
-       return future_values[future_index].value;
-}
-
-modelclock_t Node::get_future_value_expiration() const
+struct future_value Node::get_future_value() const
 {
        ASSERT(future_index >= 0 && future_index < ((int)future_values.size()));
-       return future_values[future_index].expiration;
+       return future_values[future_index];
 }
 
 int Node::get_read_from_size() const