From: Brian Norris <banorris@uci.edu>
Date: Fri, 25 Jan 2013 01:18:06 +0000 (-0800)
Subject: model: remove ModelChecker::is_infeasible_ignoreRMW()
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=3b3533a76db06884f44b3e70ccdbad647275fcc4;hp=ed8d4600431acccf43e7ac67ab523fd7486861d0

model: remove ModelChecker::is_infeasible_ignoreRMW()

We don't make any special exceptions for this condition anymore, so drop
the function.
---

diff --git a/model.cc b/model.cc
index 4ccdbce2..9e611fae 100644
--- a/model.cc
+++ b/model.cc
@@ -1407,21 +1407,11 @@ bool ModelChecker::is_feasible_prefix_ignore_relseq() const
  */
 bool ModelChecker::is_infeasible() const
 {
-	return mo_graph->checkForRMWViolation() || is_infeasible_ignoreRMW();
-}
-
-/**
- * Check If the current partial trace is infeasible, while ignoring
- * infeasibility related to 2 RMW's reading from the same store. It does not
- * check end-of-execution feasibility.
- * @see ModelChecker::is_infeasible
- * @return whether the current partial trace is infeasible, ignoring multiple
- * RMWs reading from the same store.
- * */
-bool ModelChecker::is_infeasible_ignoreRMW() const
-{
-	return mo_graph->checkForCycles() || priv->failed_promise ||
-		priv->too_many_reads || priv->bad_synchronization ||
+	return mo_graph->checkForRMWViolation() ||
+		mo_graph->checkForCycles() ||
+		priv->failed_promise ||
+		priv->too_many_reads ||
+		priv->bad_synchronization ||
 		promises_expired();
 }
 
diff --git a/model.h b/model.h
index 960e9e1a..c76a2897 100644
--- a/model.h
+++ b/model.h
@@ -257,7 +257,6 @@ private:
 
 	void print_infeasibility(const char *prefix) const;
 	bool is_feasible_prefix_ignore_relseq() const;
-	bool is_infeasible_ignoreRMW() const;
 	bool is_infeasible() const;
 	bool is_deadlocked() const;
 	bool is_complete_execution() const;