From daacebfae30aab0bc230cfdb5767b20b8ef9eaec Mon Sep 17 00:00:00 2001
From: Brian Norris <banorris@uci.edu>
Date: Wed, 12 Dec 2012 19:40:56 -0800
Subject: [PATCH] model: remove snapshotted 'nextThread'
The 'nextThread' field is no longer needed, since I've simplified
take_step().
---
model.cc | 6 ++----
1 file changed, 2 insertions(+), 4 deletions(-)
diff --git a/model.cc b/model.cc
index a566831..717f4a8 100644
--- a/model.cc
+++ b/model.cc
@@ -43,7 +43,6 @@ struct model_snapshot_members {
/* First thread created will have id INITIAL_THREAD_ID */
next_thread_id(INITIAL_THREAD_ID),
used_sequence_numbers(0),
- nextThread(NULL),
next_backtrack(NULL),
bugs(),
stats(),
@@ -62,7 +61,6 @@ struct model_snapshot_members {
ModelAction *current_action;
unsigned int next_thread_id;
modelclock_t used_sequence_numbers;
- Thread *nextThread;
ModelAction *next_backtrack;
std::vector< bug_message *, SnapshotAlloc<bug_message *> > bugs;
struct execution_stats stats;
@@ -2707,12 +2705,12 @@ bool ModelChecker::take_step(ModelAction *curr)
Thread *curr_thrd = get_thread(curr);
ASSERT(curr_thrd->get_state() == THREAD_READY);
- priv->nextThread = check_current_action(curr);
+ Thread *next_thrd = check_current_action(curr);
if (curr_thrd->is_blocked() || curr_thrd->is_complete())
scheduler->remove_thread(curr_thrd);
- Thread *next_thrd = scheduler->next_thread(priv->nextThread);
+ next_thrd = scheduler->next_thread(next_thrd);
/* Infeasible -> don't take any more steps */
if (is_infeasible())
--
2.34.1