action: add get_write_value()

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 9ebc85344cd8c4343349a4d7df21e9d034915edc..a66648bce12064d9c6730dc845f8292f277e97f6 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -1022,7 +1022,7 @@ void ModelChecker::add_future_value(const ModelAction *writer, ModelAction *read
                        write_thread = write_thread->get_parent();
 
                struct future_value fv = {
-                       writer->get_value(),
+                       writer->get_write_value(),
                        writer->get_seq_number() + params.maxfuturedelay,
                        write_thread->get_id(),
                };
@@ -1324,8 +1324,9 @@ bool ModelChecker::initialize_curr_action(ModelAction **curr)
  */
 bool ModelChecker::read_from(ModelAction *act, const ModelAction *rf)
 {
+       ASSERT(rf);
        act->set_read_from(rf);
-       if (rf != NULL && act->is_acquire()) {
+       if (act->is_acquire()) {
                rel_heads_list_t release_heads;
                get_release_seq_heads(act, act, &release_heads);
                int num_heads = release_heads.size();