model: do not assume THREAD_FINISH is always the last action
authorBrian Norris <banorris@uci.edu>
Wed, 3 Oct 2012 22:36:26 +0000 (15:36 -0700)
committerBrian Norris <banorris@uci.edu>
Wed, 3 Oct 2012 22:36:26 +0000 (15:36 -0700)
It's possible that there will be special fixup ModelActions added, so
just use the Thread::is_complete() method to check for a completed
Thread.

model.cc

index 788a670..326358e 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -1246,7 +1246,7 @@ bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *rel
 
                ModelAction *last = get_last_action(int_to_id(i));
                if (last && (rf->happens_before(last) ||
 
                ModelAction *last = get_last_action(int_to_id(i));
                if (last && (rf->happens_before(last) ||
-                               last->get_type() == THREAD_FINISH))
+                               get_thread(int_to_id(i))->is_complete()))
                        future_ordered = true;
 
                for (rit = list->rbegin(); rit != list->rend(); rit++) {
                        future_ordered = true;
 
                for (rit = list->rbegin(); rit != list->rend(); rit++) {