model: rename isfinalfeasible -> is_feasible_prefix_ignore_relseq

[c11tester.git] / model.cc

diff --git a/model.cc b/model.cc
index 8453f2e51a0c7866da57db9e6b65560442bb1905..da68074240d9ea2b416b40665ef7843d2c7df7ae 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -424,7 +424,7 @@ void ModelChecker::print_bugs() const
 void ModelChecker::record_stats()
 {
        stats.num_total++;
-       if (!isfinalfeasible())
+       if (!isfeasibleprefix())
                stats.num_infeasible++;
        else if (have_bug_reports())
                stats.num_buggy_executions++;
@@ -483,7 +483,7 @@ bool ModelChecker::next_execution()
 {
        DBG();
        /* Is this execution a feasible execution that's worth bug-checking? */
-       bool complete = isfinalfeasible() && (is_complete_execution() ||
+       bool complete = isfeasibleprefix() && (is_complete_execution() ||
                        have_bug_reports());
 
        /* End-of-execution bug checks */
@@ -1210,15 +1210,21 @@ bool ModelChecker::promises_expired() const
        return false;
 }
 
-/** @return whether the current partial trace must be a prefix of a
- * feasible trace. */
+/**
+ * This is the strongest feasibility check available.
+ * @return whether the current trace (partial or complete) must be a prefix of
+ * a feasible trace.
+ */
 bool ModelChecker::isfeasibleprefix() const
 {
-       return promises->size() == 0 && pending_rel_seqs->size() == 0 && !is_infeasible();
+       return pending_rel_seqs->size() == 0 && is_feasible_prefix_ignore_relseq();
 }
 
-/** Returns whether the current completed trace is feasible. */
-bool ModelChecker::isfinalfeasible() const
+/**
+ * Returns whether the current completed trace is feasible, except for pending
+ * release sequences.
+ */
+bool ModelChecker::is_feasible_prefix_ignore_relseq() const
 {
        if (DBG_ENABLED() && promises->size() != 0)
                DEBUG("Infeasible: unrevolved promises\n");
@@ -2358,7 +2364,7 @@ void ModelChecker::print_summary() const
        dumpGraph(buffername);
 #endif
 
-       if (!isfinalfeasible())
+       if (!isfeasibleprefix())
                model_print("INFEASIBLE EXECUTION!\n");
        print_list(action_trace, stats.num_total);
        model_print("\n");
@@ -2495,7 +2501,7 @@ bool ModelChecker::take_step() {
         * (4) no pending promises
         */
        if (!pending_rel_seqs->empty() && (!next || next->is_model_thread()) &&
-                       isfinalfeasible() && !unrealizedraces.empty()) {
+                       is_feasible_prefix_ignore_relseq() && !unrealizedraces.empty()) {
                model_print("*** WARNING: release sequence fixup action (%zu pending release seuqences) ***\n",
                                pending_rel_seqs->size());
                ModelAction *fixup = new ModelAction(MODEL_FIXUP_RELSEQ,