Fix apparent bug...

[satcheck.git] / mcexecution.cc

diff --git a/mcexecution.cc b/mcexecution.cc
index 573b0b2de0907fca36710561a2e96a315249e523..d986f517ae751336a97434f06b2c329a9b5567b8 100644 (file)
--- a/mcexecution.cc
+++ b/mcexecution.cc
@@ -212,7 +212,7 @@ uint64_t MCExecution::rmw(enum atomicop op, void *addr, uint len, uint64_t currv
        uint64_t newval;
        uint64_t retval=dormwaction(op, addr, len, currval, oldval, valarg, &newval);
        if (DBG_ENABLED()) {
-               model_print("RMW %p oldval=%lu valarg=%lu retval=%lu", addr, oldval, valarg, retval);
+               model_print("RMW %p oldval=%llu valarg=%llu retval=%llu", addr, oldval, valarg, retval);
                currexecpoint->print();
                model_print("\n");
        }
@@ -313,7 +313,7 @@ void MCExecution::doStore(thread_id_t tid) {
        EPValue * epval=list->front();
        list->pop_front();
        if (DBG_ENABLED()) {
-               model_print("tid = %lu: ", tid);
+               model_print("tid = %d: ", tid);
        }
        doStore(epval);
 }
@@ -323,7 +323,7 @@ void MCExecution::doStore(EPValue *epval) {
        uint64_t val=epval->getValue();
        int len=epval->getLen();
        if (DBG_ENABLED()) {
-               model_print("flushing %d bytes *(%p) = %lu", len, addr, val);
+               model_print("flushing %d bytes *(%p) = %llu", len, addr, val);
                currexecpoint->print();
                model_print("\n");
        }
@@ -405,7 +405,7 @@ void MCExecution::store(void *addr, uint64_t val, int len) {
 #endif
 
        if (DBG_ENABLED()) {
-               model_print("STORE *%p=%lu ", addr, val);
+               model_print("STORE *%p=%llu ", addr, val);
                currexecpoint->print();
                model_print("\n");
        }
@@ -515,7 +515,7 @@ uint64_t MCExecution::load(const void *addr, int len) {
 #endif
 
        if (DBG_ENABLED()) {
-               model_print("%lu(mid=%u)=LOAD %p ", val, id_retval, addr);
+               model_print("%llu(mid=%u)=LOAD %p ", val, id_retval, addr);
                currexecpoint->print();
                model_print("\n");
        }
@@ -654,6 +654,15 @@ uint64_t MCExecution::equals(MCID op1, uint64_t val1, MCID op2, uint64_t val2, M
                recordFunctionChange(record, 0);
                recordFunctionChange(record, 1);
        }
+
+       if(op1 == MCID_NODEP) {
+               record->getSet(VC_BASEINDEX + 0)->add(val1);
+       }
+
+       if(op2 == MCID_NODEP) {
+               record->getSet(VC_BASEINDEX + 1)->add(val2);
+       }
+
        MCID eqmcid=getNextMCID();
        ASSERT(EPList->size()==eqmcid);
        EPList->push_back(epvalue);
@@ -842,6 +851,9 @@ void MCExecution::threadFinish() {
 void MCExecution::threadYield() {
        getOrCreateCurrRecord(YIELD, NULL, 0, 0, 8, false);
        currexecpoint->incrementTop();
+       if (model->params.noexecyields) {
+               threadFinish();
+       }
 }
 
 /** @brief Thread yield. */