projects
/
model-checker.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
| inline |
side by side
(parent:
7f6f387
)
model: do not assume THREAD_FINISH is always the last action
author
Brian Norris
<banorris@uci.edu>
Wed, 3 Oct 2012 22:36:26 +0000
(15:36 -0700)
committer
Brian 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
patch
|
blob
|
history
diff --git
a/model.cc
b/model.cc
index 788a6706b26074b91db6de091f12ef532c54bd27..326358ea79c8b80ed0a356854cef43288c0ec304 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) ||
-
last->get_type() == THREAD_FINISH
))
+
get_thread(int_to_id(i))->is_complete()
))
future_ordered = true;
for (rit = list->rbegin(); rit != list->rend(); rit++) {