projects
/
c11tester.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
c80c149
)
a bug fix
author
Brian Demsky
<bdemsky@uci.edu>
Wed, 3 Oct 2012 01:06:46 +0000
(18:06 -0700)
committer
Brian Demsky
<bdemsky@uci.edu>
Wed, 3 Oct 2012 01:06:46 +0000
(18:06 -0700)
model.cc
patch
|
blob
|
history
diff --git
a/model.cc
b/model.cc
index ae0a787f3ad7a776c416a47cbb302d95f03c02c2..0006fd63d66e172336df1296c417a787fe559d2a 100644
(file)
--- a/
model.cc
+++ b/
model.cc
@@
-139,6
+139,9
@@
Thread * ModelChecker::get_next_thread(ModelAction *curr)
ModelAction *next = node_stack->get_next()->get_action();
if (next == diverge) {
ModelAction *next = node_stack->get_next()->get_action();
if (next == diverge) {
+ if (earliest_diverge == NULL || *diverge < *earliest_diverge)
+ earliest_diverge=diverge;
+
Node *nextnode = next->get_node();
/* Reached divergence point */
if (nextnode->increment_promise()) {
Node *nextnode = next->get_node();
/* Reached divergence point */
if (nextnode->increment_promise()) {
@@
-158,8
+161,12
@@
Thread * ModelChecker::get_next_thread(ModelAction *curr)
Node *node = nextnode->get_parent();
tid = node->get_next_backtrack();
node_stack->pop_restofstack(1);
Node *node = nextnode->get_parent();
tid = node->get_next_backtrack();
node_stack->pop_restofstack(1);
+ if (diverge==earliest_diverge) {
+ earliest_diverge=node->get_action();
+ }
}
DEBUG("*** Divergence point ***\n");
}
DEBUG("*** Divergence point ***\n");
+
diverge = NULL;
} else {
tid = next->get_tid();
diverge = NULL;
} else {
tid = next->get_tid();
@@
-198,9
+205,6
@@
bool ModelChecker::next_execution()
if ((diverge = get_next_backtrack()) == NULL)
return false;
if ((diverge = get_next_backtrack()) == NULL)
return false;
- if (earliest_diverge == NULL || *diverge < *earliest_diverge)
- earliest_diverge=diverge;
-
if (DBG_ENABLED()) {
printf("Next execution will diverge at:\n");
diverge->print();
if (DBG_ENABLED()) {
printf("Next execution will diverge at:\n");
diverge->print();