projects
/
c11tester.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
f644ed0
)
model: add too_many_reads flag
author
Brian Norris
<banorris@uci.edu>
Tue, 11 Sep 2012 17:19:46 +0000
(10:19 -0700)
committer
Brian Norris
<banorris@uci.edu>
Tue, 11 Sep 2012 17:19:46 +0000
(10:19 -0700)
model.cc
patch
|
blob
|
history
model.h
patch
|
blob
|
history
diff --git
a/model.cc
b/model.cc
index c8af6cc4f5bfb2d2c878e6aa035e2cf712d56e29..c77d4e17d4627213d2510774fe9c5d853b91257e 100644
(file)
--- a/
model.cc
+++ b/
model.cc
@@
-33,6
+33,7
@@
ModelChecker::ModelChecker(struct model_params params) :
node_stack(new NodeStack()),
mo_graph(new CycleGraph()),
failed_promise(false),
node_stack(new NodeStack()),
mo_graph(new CycleGraph()),
failed_promise(false),
+ too_many_reads(false),
asserted(false)
{
/* Allocate this "size" on the snapshotting heap */
asserted(false)
{
/* Allocate this "size" on the snapshotting heap */
@@
-75,6
+76,7
@@
void ModelChecker::reset_to_initial_state()
DEBUG("+++ Resetting to initial state +++\n");
node_stack->reset_execution();
failed_promise = false;
DEBUG("+++ Resetting to initial state +++\n");
node_stack->reset_execution();
failed_promise = false;
+ too_many_reads = false;
reset_asserted();
snapshotObject->backTrackBeforeStep(0);
}
reset_asserted();
snapshotObject->backTrackBeforeStep(0);
}
@@
-380,7
+382,7
@@
bool ModelChecker::isfeasibleprefix() {
/** @returns whether the current partial trace is feasible. */
bool ModelChecker::isfeasible() {
/** @returns whether the current partial trace is feasible. */
bool ModelChecker::isfeasible() {
- return !mo_graph->checkForCycles() && !failed_promise;
+ return !mo_graph->checkForCycles() && !failed_promise
&& !too_many_reads
;
}
/** Returns whether the current completed trace is feasible. */
}
/** Returns whether the current completed trace is feasible. */
diff --git
a/model.h
b/model.h
index 990f559cc5af67fd368d5355bb890fc975a2c13d..5d34b4aa3e2694bcfd725e4170131592b884eba0 100644
(file)
--- a/
model.h
+++ b/
model.h
@@
-177,6
+177,7
@@
private:
*/
CycleGraph *mo_graph;
bool failed_promise;
*/
CycleGraph *mo_graph;
bool failed_promise;
+ bool too_many_reads;
bool asserted;
};
bool asserted;
};