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:
f05f7c7
)
model: bugfix - infinite loop in resolve_release_sequences()
author
Brian Norris
<banorris@uci.edu>
Fri, 21 Sep 2012 17:23:21 +0000
(10:23 -0700)
committer
Brian Norris
<banorris@uci.edu>
Fri, 21 Sep 2012 17:26:04 +0000
(10:26 -0700)
model.cc
patch
|
blob
|
history
diff --git
a/model.cc
b/model.cc
index 64c1daa5d8f2b52aa561b50cbd2a07a65853ec84..0283911b6eea07e57c7b7266fe3c80fc2d755595 100644
(file)
--- a/
model.cc
+++ b/
model.cc
@@
-1233,7
+1233,7
@@
bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_
/* propagate synchronization to later actions */
action_list_t::reverse_iterator it = action_trace->rbegin();
-
while ((*it) != act
) {
+
for (; (*it) != act; it++
) {
ModelAction *propagate = *it;
if (act->happens_before(propagate)) {
propagate->synchronize_with(act);