+ e = exprNode_fakeCopy(e1);
+ c1 = constraintExpr_makeValueExpr (e);
+
+ e = exprNode_fakeCopy(e2);
+ c2 = constraintExpr_makeValueExpr (e);
+
+ ret = constraint_makeEnsuresOpConstraintExpr (c1, c2, sequencePoint, ar);
+
+ return ret;
+}
+
+
+/* make constraint ensures e1 == e2 */
+
+constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
+{
+ return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, EQ) );
+}
+
+/*make constraint ensures e1 < e2 */
+constraint constraint_makeEnsureLessThan (exprNode e1, exprNode e2, fileloc sequencePoint)
+{
+ constraintExpr t1, t2;
+
+ t1 = constraintExpr_makeValueExpr (e1);
+ t2 = constraintExpr_makeValueExpr (e2);
+
+ /*change this to e1 <= (e2 -1) */
+
+ t2 = constraintExpr_makeDecConstraintExpr (t2);
+
+ return ( constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, LTE) );
+}
+
+constraint constraint_makeEnsureLessThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
+{
+ return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, LTE) );
+}
+
+constraint constraint_makeEnsureGreaterThan (exprNode e1, exprNode e2, fileloc sequencePoint)
+{
+ constraintExpr t1, t2;
+
+ t1 = constraintExpr_makeValueExpr (e1);
+ t2 = constraintExpr_makeValueExpr (e2);
+
+
+ /* change this to e1 >= (e2 + 1) */
+ t2 = constraintExpr_makeIncConstraintExpr (t2);
+
+
+ return ( constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, GTE) );
+}
+
+constraint constraint_makeEnsureGreaterThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
+{
+ return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, GTE) );
+}
+
+
+exprNode exprNode_copyConstraints (/*@returned@*/ exprNode dst, exprNode src)
+{
+ constraintList_free(dst->ensuresConstraints);
+ constraintList_free(dst->requiresConstraints);
+ constraintList_free(dst->trueEnsuresConstraints);
+ constraintList_free(dst->falseEnsuresConstraints);
+
+ dst->ensuresConstraints = constraintList_copy (src->ensuresConstraints );
+ dst->requiresConstraints = constraintList_copy (src->requiresConstraints );
+ dst->trueEnsuresConstraints = constraintList_copy (src->trueEnsuresConstraints );
+ dst->falseEnsuresConstraints = constraintList_copy (src->falseEnsuresConstraints );
+ return dst;
+}
+
+/* Makes the constraint e = e + f */
+constraint constraint_makeAddAssign (exprNode e, exprNode f, fileloc sequencePoint)
+{
+ constraintExpr x1, x2, y;
+ constraint ret;
+
+ ret = constraint_makeNew();
+
+ x1 = constraintExpr_makeValueExpr (e);
+ x2 = constraintExpr_copy(x1);
+ y = constraintExpr_makeValueExpr (f);
+
+ ret->lexpr = x1;
+ ret->ar = EQ;