Fix apparent bug...

[satcheck.git] / loadrf.cc

diff --git a/loadrf.cc b/loadrf.cc
index f536c1bf336d2340012f4dd3231d99dc58d18e47..52a08fb0b162de198c037c3853eecd38e2fb2278 100644 (file)
--- a/loadrf.cc
+++ b/loadrf.cc
@@ -18,7 +18,7 @@
 LoadRF::LoadRF(EPRecord *_load, ConstGen *cg) : load(_load) {
        RecordSet *mrfSet=cg->getMayReadFromSet(load);
        uint numstores=mrfSet->getSize();
-       numvars=NUMBITS(numstores-1);
+       numvars=NUMBITS(numstores); 
        vars=(Constraint **)model_malloc(numvars*sizeof(Constraint *));
        cg->getArrayNewVars(numvars, vars);
 }
@@ -33,7 +33,7 @@ void LoadRF::genConstraints(ConstGen *cg) {
        StoreLoadSet * sls=cg->getStoreLoadSet(load);
        uint numvalvars=sls->getNumValVars();
        uint numaddrvars=sls->getNumAddrVars();
-       Constraint ** loadvalvars=(load->getType()==RMW)?sls->getRMWRValVars(cg, load):sls->getValVars(cg, load);
+       Constraint ** loadvalvars=(load->getType()==RMW) ? sls->getRMWRValVars(cg, load) : sls->getValVars(cg, load);
        Constraint ** loadaddrvars=sls->getAddrVars(cg, load);
 
        RecordIterator *sri=mrfSet->iterator();
@@ -42,7 +42,7 @@ void LoadRF::genConstraints(ConstGen *cg) {
                Constraint ** storevalvars=sls->getValVars(cg, store);
 
 
-               Constraint *rfconst=(numvars==0)?&ctrue:generateConstraint(numvars, vars, storeindex);
+               Constraint *rfconst=(numvars==0) ? &ctrue : generateConstraint(numvars, vars, storeindex);
                //if we read from a store, it should happen before us
 #ifdef TSO
                Constraint *storebeforeload;
@@ -76,7 +76,7 @@ void LoadRF::genConstraints(ConstGen *cg) {
                //ordered between the load and store
 
                RecordSet *conflictSet=cg->computeConflictSet(store, load, mrfSet);
-               RecordIterator *sit=conflictSet!=NULL?conflictSet->iterator():mrfSet->iterator();
+               RecordIterator *sit=conflictSet!=NULL ? conflictSet->iterator() : mrfSet->iterator();
 
                while(sit->hasNext()) {
                        EPRecord *conflictstore=sit->next();
@@ -100,7 +100,7 @@ void LoadRF::genConstraints(ConstGen *cg) {
                                continue;
                        }
 #else
-                       Constraint * conflictbeforeload=cg->getOrderConstraint(conflictstore, load);    
+                       Constraint * conflictbeforeload=cg->getOrderConstraint(conflictstore, load);
                        if (conflictbeforeload->isFalse()) {
                                storebeforeconflict->freerec();
                                continue;
@@ -111,10 +111,10 @@ void LoadRF::genConstraints(ConstGen *cg) {
                                                                                                         conflictbeforeload,
                                                                                                         rfconst,
                                                                                                         cg->getExecutionConstraint(conflictstore)};
-                       Constraint *confstore=new Constraint(IMPLIES, 
+                       Constraint *confstore=new Constraint(IMPLIES,
                                                                                                                                                                         new Constraint(AND, 4, array),
                                                                                                                                                                         generateEquivConstraint(numaddrvars, loadaddrvars, confstoreaddrvars)->negate());
-                       
+
                        ADDCONSTRAINT2(cg, confstore, "confstore");
                }
                delete sit;