nodestack: pass 'struct future_value' to add_future_value()

[model-checker.git] / nodestack.cc

diff --git a/nodestack.cc b/nodestack.cc
index a4d2b1a491a989cb094f8709d2d3ca19e2687b0e..7d703bbff0860abb4cb7732b76a5780f0af0c13d 100644 (file)
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -8,6 +8,7 @@
 #include "common.h"
 #include "model.h"
 #include "threads-model.h"
+#include "modeltypes.h"
 
 /**
  * @brief Node constructor
@@ -89,7 +90,7 @@ Node::~Node()
 }
 
 /** Prints debugging info for the ModelAction associated with this Node */
-void Node::print()
+void Node::print() const
 {
        action->print();
        model_print("          backtrack: %s", backtrack_empty() ? "empty" : "non-empty ");
@@ -225,8 +226,10 @@ 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(struct future_value& fv)
 {
+       uint64_t value = fv.value;
+       modelclock_t expiration = fv.expiration;
        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) {
@@ -249,8 +252,7 @@ bool Node::add_future_value(uint64_t value, modelclock_t expiration)
                        (int)future_values.size() >= model->params.maxfuturevalues)
                return false;
 
-       struct future_value newfv = {value, expiration};
-       future_values.push_back(newfv);
+       future_values.push_back(fv);
        return true;
 }
 
@@ -381,20 +383,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