Constraint *l2=getRetValueEncoding(r, constval);
Constraint *functionimplication2=new Constraint(IMPLIES, outputtrue, l2);
ADDCONSTRAINT(functionimplication2,"equalsimpl");
+ return;
}
IntIterator *iit=record->getSet(VC_BASEINDEX)->iterator();
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);
--- /dev/null
+#include <threads.h>
+#include <inttypes.h>
+#include "libinterface.h"
+
+static int zero;
+
+int user_main(int argc, char **argv)
+{
+ store_32(&zero, 0);
+
+ int val = load_32(&zero);
+
+ int val2 = 0;
+ MCID _mval2 = MCID_NODEP;
+
+ /** this equality check contains one NODEP and should work. **/
+ if(val == val2)
+ {
+ return 1;
+ }
+
+ return 0;
+}
\ No newline at end of file