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:
728a295
)
main: take/revert snapshots
author
Brian Norris
<banorris@uci.edu>
Thu, 24 May 2012 18:33:36 +0000
(11:33 -0700)
committer
Brian Norris
<banorris@uci.edu>
Sat, 26 May 2012 01:02:43 +0000
(18:02 -0700)
Use basic snapshotting for 'reset_to_initial_state()'.
main.cc
patch
|
blob
|
history
model.cc
patch
|
blob
|
history
diff --git
a/main.cc
b/main.cc
index c5b6028f27536551078a0447d0c57e4d1bb15542..8db63e6d1733d1204e9855575c49d06dafc6d9a6 100644
(file)
--- a/
main.cc
+++ b/
main.cc
@@
-53,6
+53,8
@@
void real_main() {
model->set_system_context(&main_context);
+ snapshotObject->snapshotStep(0);
+
do {
/* Start user program */
model->add_thread(new Thread(&user_thread, (void (*)(void *)) &user_main, NULL));
diff --git
a/model.cc
b/model.cc
index 09ee4b4a91d07e2667738a0867782061ed97fb97..4db55728db7e347383fcdb70b070c7ac8f94a4f4 100644
(file)
--- a/
model.cc
+++ b/
model.cc
@@
-59,6
+59,7
@@
void ModelChecker::reset_to_initial_state()
nextThread = 0;
next_backtrack = NULL;
/* scheduler reset ? */
+ snapshotObject->backTrackBeforeStep(0);
}
thread_id_t ModelChecker::get_next_id()