From: Brian Norris <banorris@uci.edu>
Date: Sat, 23 Feb 2013 00:12:34 +0000 (-0800)
Subject: model: correct the "no valid reads" assertion
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=ebbaf2d1ff97315fdf97943f122392d1a449e41b;ds=sidebyside

model: correct the "no valid reads" assertion

There are "no valid reads" only if there are no valid prior reads-from
candidates AND no potential values.
---

diff --git a/model.cc b/model.cc
index 998059e2..990f03c5 100644
--- a/model.cc
+++ b/model.cc
@@ -2619,7 +2619,7 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
 		}
 	}
 	/* We may find no valid may-read-from only if the execution is doomed */
-	if (!curr->get_node()->get_read_from_size()) {
+	if (!curr->get_node()->get_read_from_size() && curr->get_node()->future_value_empty()) {
 		priv->no_valid_reads = true;
 		set_assert();
 	}