Fix TSO Bugs

[satcheck.git] / mcexecution.cc

diff --git a/mcexecution.cc b/mcexecution.cc
index 1166731c1b6758a88f3c0e5b680dbb147e6d32ed..36afe0b81f030112102e0f7a07e2ae1c9e69c09f 100644 (file)
--- a/mcexecution.cc
+++ b/mcexecution.cc
@@ -312,6 +312,9 @@ void MCExecution::doStore(thread_id_t tid) {
        SnapList<EPValue *> * list=(*storebuffer)[id_to_int(tid)];
        EPValue * epval=list->front();
        list->pop_front();
+       if (DBG_ENABLED()) {
+               model_print("tid = %lu: ", tid);
+       }
        doStore(epval);
 }
 
@@ -895,6 +898,9 @@ void MCExecution::exitLoop() {
        if (!currexecpoint->directInLoop()) {
                breakstate=getOrCreateCurrRecord(NONLOCALTRANS, NULL, 0, 0, 8, false);
                currexecpoint->incrementTop();
+       } else {
+               breakstate=getOrCreateCurrRecord(LOOPEXIT, NULL, 0, 0, 8, false);
+               currexecpoint->incrementTop();
        }
        
        /* Get Last Record */
@@ -927,9 +933,7 @@ void MCExecution::exitLoop() {
        if (loopenter->getNextRecord()==NULL) {
                loopenter->setNextRecord(labelrec);
        }
-       if (breakstate!=NULL) {
-               breakstate->setNextRecord(labelrec);
-       }
+       breakstate->setNextRecord(labelrec);
        currexecpoint->incrementTop();
 }