Bug: ModelExecution had bogus model_params reference.

[c11tester.git] / execution.cc

diff --git a/execution.cc b/execution.cc
index 33c862bac36fd2a7e788cfae00a1a46a774ecd4a..47a6ebbff7b76dfbbd7f0ec9898606e4f469d29e 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -58,7 +58,7 @@ struct model_snapshot_members {
 
 /** @brief Constructor */
 ModelExecution::ModelExecution(ModelChecker *m,
-               struct model_params *params,
+               const struct model_params *params,
                Scheduler *scheduler,
                NodeStack *node_stack) :
        model(m),
@@ -366,7 +366,10 @@ ModelAction * ModelExecution::get_last_fence_conflict(ModelAction *act) const
 ModelAction * ModelExecution::get_last_conflict(ModelAction *act) const
 {
        switch (act->get_type()) {
-       /* case ATOMIC_FENCE: fences don't directly cause backtracking */
+       case ATOMIC_FENCE:
+               /* Only seq-cst fences can (directly) cause backtracking */
+               if (!act->is_seqcst())
+                       break;
        case ATOMIC_READ:
        case ATOMIC_WRITE:
        case ATOMIC_RMW: {
@@ -377,6 +380,8 @@ ModelAction * ModelExecution::get_last_conflict(ModelAction *act) const
                action_list_t::reverse_iterator rit;
                for (rit = list->rbegin(); rit != list->rend(); rit++) {
                        ModelAction *prev = *rit;
+                       if (prev == act)
+                               continue;
                        if (prev->could_synchronize_with(act)) {
                                ret = prev;
                                break;
@@ -1209,7 +1214,7 @@ bool ModelExecution::check_action_enabled(ModelAction *curr) {
  *
  * @param curr The current action to process
  * @return The ModelAction that is actually executed; may be different than
- * curr; may be NULL, if the current action is not enabled to run
+ * curr
  */
 ModelAction * ModelExecution::check_current_action(ModelAction *curr)
 {
@@ -2811,7 +2816,7 @@ void ModelExecution::fixup_release_sequences()
 {
        while (!pending_rel_seqs.empty() &&
                        is_feasible_prefix_ignore_relseq() &&
-                       !unrealizedraces.empty()) {
+                       haveUnrealizedRaces()) {
                model_print("*** WARNING: release sequence fixup action "
                                "(%zu pending release seuqence(s)) ***\n",
                                pending_rel_seqs.size());