X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satcheck.git;a=blobdiff_plain;f=eprecord.cc;h=30ece3bb1d706803e32d4028aa4bac305737ab8a;hp=c7bf25f67ad8c68554433b661711e997e9399140;hb=dda2d5d103b32f8505374712936af1daf42ec061;hpb=44e8eabc8f7a0ab23c29037a770463d8a2de7b4a;ds=sidebyside

diff --git a/eprecord.cc b/eprecord.cc
index c7bf25f..30ece3b 100644
--- a/eprecord.cc
+++ b/eprecord.cc
@@ -83,6 +83,8 @@ const char * eventToStr(EventType event) {
 		return "yield";
 	case NONLOCALTRANS:
 		return "nonlocal";
+	case LOOPEXIT:
+		return "loopexit";
 	case LABEL:
 		return "label";
 	case LOOPENTER:
@@ -115,6 +117,7 @@ IntHashSet * EPRecord::getReturnValueSet() {
 	case YIELD:
 	case FENCE:
 	case NONLOCALTRANS:
+	case LOOPEXIT:
 	case LABEL:
 	case LOOPENTER:
 	case LOOPSTART:
@@ -129,13 +132,13 @@ IntHashSet * EPRecord::getReturnValueSet() {
 void EPRecord::print(int f) {
 	if (event==RMW) {
 		if (op==ADD)
-			dprintf(f, "add");
+			model_dprintf(f, "add");
 		else if (op==EXC)
-			dprintf(f, "exc");
+			model_dprintf(f, "exc");
 		else
-			dprintf(f, "cas");
+			model_dprintf(f, "cas");
 	} else
-		dprintf(f, "%s",eventToStr(event));
+		model_dprintf(f, "%s",eventToStr(event));
 	IntHashSet *i=NULL;
 	switch(event) {
 	case LOAD:
@@ -150,14 +153,14 @@ void EPRecord::print(int f) {
 	case FUNCTION: {
 		if (!getPhi()) {
 			CGoalIterator *cit=completed->iterator();
-			dprintf(f, "{");
+			model_dprintf(f, "{");
 			while(cit->hasNext()) {
 				CGoal *goal=cit->next();
-				dprintf(f,"(");
+				model_dprintf(f,"(");
 				for(uint i=0;i<getNumFuncInputs();i++) {
-					dprintf(f,"%lu ", goal->getValue(i+VC_BASEINDEX));
+					model_dprintf(f,"%llu ", goal->getValue(i+VC_BASEINDEX));
 				}
-				dprintf(f,"=> %lu)", goal->getOutput());
+				model_dprintf(f,"=> %llu)", goal->getOutput());
 			}
 			delete cit;
 		}
@@ -168,28 +171,27 @@ void EPRecord::print(int f) {
 	}
 	if (i!=NULL) {
 		IntIterator *it=i->iterator();
-		dprintf(f, "{");
+		model_dprintf(f, "{");
 
 		while(it->hasNext()) {
-			dprintf(f, "%lu ", it->next());
+			model_dprintf(f, "%llu ", it->next());
 		}
-		dprintf(f, "}");
+		model_dprintf(f, "}");
 		delete it;
 	}
 
 	for(uint i=0;i<numinputs;i++) {
 		IntIterator *it=setarray[i]->iterator();
-		dprintf(f,"{");
+		model_dprintf(f,"{");
 		while(it->hasNext()) {
 			uint64_t v=it->next();
-			dprintf(f,"%lu ", v);
+			model_dprintf(f,"%llu ", v);
 		}
-		dprintf(f,"}");
+		model_dprintf(f,"}");
 		delete it;
 	}
-	dprintf(f, "}");
 
-	
+
 	execpoint->print(f);
 }