X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=d7b87f6359a94d3107421521f0f46ec5927ab58a;hb=05d91de8ac8098425d51e9af2704eb91e04a7f9b;hp=e4b6431336050c89043f45851214c632b2e943ce;hpb=fab8621e4bf6acafc04dbaf786e2de6263d892f6;p=model-checker.git

diff --git a/model.cc b/model.cc
index e4b6431..d7b87f6 100644
--- a/model.cc
+++ b/model.cc
@@ -1293,11 +1293,10 @@ void ModelChecker::check_curr_backtracking(ModelAction *curr)
 
 bool ModelChecker::promises_expired() const
 {
-	for (unsigned int promise_index = 0; promise_index < promises->size(); promise_index++) {
-		Promise *promise = (*promises)[promise_index];
-		if (promise->get_expiration()<priv->used_sequence_numbers) {
+	for (unsigned int i = 0; i < promises->size(); i++) {
+		Promise *promise = (*promises)[i];
+		if (promise->get_expiration() < priv->used_sequence_numbers)
 			return true;
-		}
 	}
 	return false;
 }
@@ -2680,15 +2679,19 @@ bool ModelChecker::is_enabled(thread_id_t tid) const
  * @param act The current action that will be explored. May be NULL only if
  * trace is exiting via an assertion (see ModelChecker::set_assert and
  * ModelChecker::has_asserted).
- * @return Return status from the 'swap' call (i.e., success/fail, 0/-1)
+ * @return Return the value returned by the current action
  */
-int ModelChecker::switch_to_master(ModelAction *act)
+uint64_t ModelChecker::switch_to_master(ModelAction *act)
 {
 	DBG();
 	Thread *old = thread_current();
 	set_current_action(act);
 	old->set_state(THREAD_READY);
-	return Thread::swap(old, &system_context);
+	if (Thread::swap(old, &system_context) < 0) {
+		perror("swap threads");
+		exit(EXIT_FAILURE);
+	}
+	return old->get_return_value();
 }
 
 /**