From daacebfae30aab0bc230cfdb5767b20b8ef9eaec Mon Sep 17 00:00:00 2001 From: Brian Norris 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 > 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