From: Brian Norris <banorris@uci.edu>
Date: Sat, 19 Jan 2013 00:30:26 +0000 (-0800)
Subject: schedule: allow Schedule::print() even in non-DEBUG build
X-Git-Tag: oopsla2013~354
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=1ec752235b9629b1608babda6a9582fc9a0dd1a7;p=model-checker.git

schedule: allow Schedule::print() even in non-DEBUG build

For instance, printing from w/in gdb
---

diff --git a/schedule.cc b/schedule.cc
index 444e1a8..602cdb7 100644
--- a/schedule.cc
+++ b/schedule.cc
@@ -184,7 +184,8 @@ Thread * Scheduler::next_thread(Thread *t)
 				break;
 			}
 			if (curr_thread_index == old_curr_thread) {
-				print();
+				if (DBG_ENABLED())
+					print();
 				return NULL;
 			}
 		}
@@ -196,7 +197,8 @@ Thread * Scheduler::next_thread(Thread *t)
 	}
 
 	current = t;
-	print();
+	if (DBG_ENABLED())
+		print();
 	return t;
 }
 
@@ -216,7 +218,7 @@ Thread * Scheduler::get_current_thread() const
 void Scheduler::print() const
 {
 	if (current)
-		DEBUG("Current thread: %d\n", id_to_int(current->get_id()));
+		model_print("Current thread: %d\n", id_to_int(current->get_id()));
 	else
-		DEBUG("No current thread\n");
+		model_print("No current thread\n");
 }