From: Brian Norris <banorris@uci.edu>
Date: Tue, 11 Sep 2012 17:19:46 +0000 (-0700)
Subject: model: add too_many_reads flag
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=def20b2249cf6902b4170965cd30a8e27ecc24f1

model: add too_many_reads flag
---

diff --git a/model.cc b/model.cc
index c8af6cc4..c77d4e17 100644
--- a/model.cc
+++ b/model.cc
@@ -33,6 +33,7 @@ ModelChecker::ModelChecker(struct model_params params) :
 	node_stack(new NodeStack()),
 	mo_graph(new CycleGraph()),
 	failed_promise(false),
+	too_many_reads(false),
 	asserted(false)
 {
 	/* Allocate this "size" on the snapshotting heap */
@@ -75,6 +76,7 @@ void ModelChecker::reset_to_initial_state()
 	DEBUG("+++ Resetting to initial state +++\n");
 	node_stack->reset_execution();
 	failed_promise = false;
+	too_many_reads = false;
 	reset_asserted();
 	snapshotObject->backTrackBeforeStep(0);
 }
@@ -380,7 +382,7 @@ bool ModelChecker::isfeasibleprefix() {
 
 /** @returns whether the current partial trace is feasible. */
 bool ModelChecker::isfeasible() {
-	return !mo_graph->checkForCycles() && !failed_promise;
+	return !mo_graph->checkForCycles() && !failed_promise && !too_many_reads;
 }
 
 /** Returns whether the current completed trace is feasible. */
diff --git a/model.h b/model.h
index 990f559c..5d34b4aa 100644
--- a/model.h
+++ b/model.h
@@ -177,6 +177,7 @@ private:
 	 */
 	CycleGraph *mo_graph;
 	bool failed_promise;
+	bool too_many_reads;
 	bool asserted;
 };