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:
917ae2f
)
changes to allow running programs with racing initialization...
author
Brian Demsky
<bdemsky@uci.edu>
Fri, 26 Oct 2012 23:31:20 +0000
(16:31 -0700)
committer
Brian Demsky
<bdemsky@uci.edu>
Fri, 26 Oct 2012 23:31:20 +0000
(16:31 -0700)
model.cc
patch
|
blob
|
history
diff --git
a/model.cc
b/model.cc
index e5926730b87c512b388e058a23f08e031a5df33a..f8aa4f0a4fd49b6eb487539c9fece2d15146e2a0 100644
(file)
--- a/
model.cc
+++ b/
model.cc
@@
-1994,6
+1994,7
@@
void ModelChecker::build_reads_from_past(ModelAction *curr)
if (!initialized) {
/** @todo Need a more informative way of reporting errors. */
printf("ERROR: may read from uninitialized atomic\n");
+ set_assert();
}
if (DBG_ENABLED() || !initialized) {
@@
-2003,8
+2004,6
@@
void ModelChecker::build_reads_from_past(ModelAction *curr)
curr->get_node()->print_may_read_from();
printf("End printing may_read_from\n");
}
-
- ASSERT(initialized);
}
bool ModelChecker::sleep_can_read_from(ModelAction * curr, const ModelAction *write) {