From: root <root@plrg-1.ics.uci.edu>
Date: Fri, 20 Dec 2019 06:40:53 +0000 (-0800)
Subject: Fix bug Weiyu found
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=6e33d79ca8cddb7cf10c8b44d470286c63cdf6d5;p=c11tester.git

Fix bug Weiyu found
---

diff --git a/model.cc b/model.cc
index 7ae63b69..4f8a0324 100644
--- a/model.cc
+++ b/model.cc
@@ -30,7 +30,6 @@ void placeholder(void *) {
 ModelChecker::ModelChecker() :
 	/* Initialize default scheduler */
 	params(),
-	restart_flag(false),
 	scheduler(new Scheduler()),
 	history(new ModelHistory()),
 	execution(new ModelExecution(this, scheduler)),
@@ -237,7 +236,7 @@ void ModelChecker::print_execution(bool printbugs) const
  * @return If there are more executions to explore, return true. Otherwise,
  * return false.
  */
-bool ModelChecker::next_execution()
+void ModelChecker::finish_execution(bool more_executions)
 {
 	DBG();
 	/* Is this execution a feasible execution that's worth bug-checking? */
@@ -259,15 +258,11 @@ bool ModelChecker::next_execution()
 	else
 		clear_program_output();
 
-	if (restart_flag) {
-		do_restart();
-		return true;
-	}
 // test code
 	execution_number ++;
-	reset_to_initial_state();
+	if (more_executions)
+	  reset_to_initial_state();
 	history->set_new_exec_flag();
-	return false;
 }
 
 /** @brief Run trace analyses on complete trace */
@@ -371,21 +366,6 @@ bool ModelChecker::should_terminate_execution()
 	return false;
 }
 
-/** @brief Restart ModelChecker upon returning to the run loop of the
- *	model checker. */
-void ModelChecker::restart()
-{
-	restart_flag = true;
-}
-
-void ModelChecker::do_restart()
-{
-	restart_flag = false;
-	reset_to_initial_state();
-	memset(&stats,0,sizeof(struct execution_stats));
-	execution_number = 1;
-}
-
 /** @brief Run ModelChecker for the user program */
 void ModelChecker::run()
 {
@@ -472,7 +452,7 @@ void ModelChecker::run()
 			t->set_pending(NULL);
 			t = execution->take_step(curr);
 		} while (!should_terminate_execution());
-		next_execution();
+		finish_execution((exec+1) < params.maxexecutions);
 		//restore random number generator state after rollback
 		setstate(random_state);
 	}
diff --git a/model.h b/model.h
index c5a5aa78..62b227e4 100644
--- a/model.h
+++ b/model.h
@@ -35,9 +35,6 @@ public:
 	model_params * getParams();
 	void run();
 
-	/** Restart the model checker, intended for pluggins. */
-	void restart();
-
 	/** Exit the model checker, intended for pluggins. */
 	void exit_model_checker();
 
@@ -69,9 +66,6 @@ public:
 	Scheduler * getScheduler() {return scheduler;}
 	MEMALLOC
 private:
-	/** Flag indicates whether to restart the model checker. */
-	bool restart_flag;
-
 	/** Snapshot id we return to restart. */
 	snapshot_id snapshot;
 
@@ -85,7 +79,7 @@ private:
 
 	unsigned int get_num_threads() const;
 
-	bool next_execution();
+	void finish_execution(bool moreexecutions);
 	bool should_terminate_execution();
 
 	Thread * get_next_thread();
@@ -95,8 +89,6 @@ private:
 
 	ModelVector<TraceAnalysis *> trace_analyses;
 
-	/** @bref Implement restart. */
-	void do_restart();
 	/** @bref Plugin that can inspect new actions. */
 	TraceAnalysis *inspect_plugin;
 	/** @brief The cumulative execution stats */