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:
b81be96
)
model: detect uninitialized atomic reads
author
Brian Norris
<banorris@uci.edu>
Sat, 7 Jul 2012 00:54:54 +0000
(17:54 -0700)
committer
Brian Norris
<banorris@uci.edu>
Sat, 7 Jul 2012 01:00:51 +0000
(18:00 -0700)
model.cc
patch
|
blob
|
history
diff --git
a/model.cc
b/model.cc
index a67163f0c34c761e3fac0b5b2c39b180ed8c2444..884ed64d0b30b51ec73954e3797f10a2e70fe793 100644
(file)
--- a/
model.cc
+++ b/
model.cc
@@
-323,6
+323,9
@@
void ModelChecker::build_reads_from_past(ModelAction *curr)
ASSERT(curr->is_read());
ASSERT(curr->is_read());
+ /* Track whether this object has been initialized */
+ bool initialized = false;
+
for (i = 0; i < thrd_lists->size(); i++) {
action_list_t *list = &(*thrd_lists)[i];
action_list_t::reverse_iterator rit;
for (i = 0; i < thrd_lists->size(); i++) {
action_list_t *list = &(*thrd_lists)[i];
action_list_t::reverse_iterator rit;
@@
-341,10
+344,27
@@
void ModelChecker::build_reads_from_past(ModelAction *curr)
curr->get_node()->add_read_from(act);
/* Include at most one act per-thread that "happens before" curr */
curr->get_node()->add_read_from(act);
/* Include at most one act per-thread that "happens before" curr */
- if (act->happens_before(curr))
+ if (act->happens_before(curr)) {
+ initialized = true;
break;
break;
+ }
}
}
}
}
+
+ if (!initialized) {
+ /* TODO: need a more informative way of reporting errors */
+ printf("ERROR: may read from uninitialized atomic\n");
+ }
+
+ if (DBG_ENABLED() || !initialized) {
+ printf("Reached read action:\n");
+ curr->print();
+ printf("Printing may_read_from\n");
+ curr->get_node()->print_may_read_from();
+ printf("End printing may_read_from\n");
+ }
+
+ ASSERT(initialized);
}
static void print_list(action_list_t *list)
}
static void print_list(action_list_t *list)