+/*@noaccess exprNode@*/
+
+void exprNode_forLoopHeuristics ( exprNode e, exprNode forPred, exprNode forBody)
+{
+ forLoopHeuristicsImpl (e, forPred, forBody);
+}
+
+ /*@access constraintExpr @*/
+
+static bool isInc (/*@observer@*/ constraintExpr c) /*@*/
+{
+
+ llassert (constraintExpr_isDefined (c) );
+ if (c->kind == binaryexpr )
+ {
+ constraintExprBinaryOpKind binOP;
+ constraintExpr t1, t2;
+ t1 = constraintExprData_binaryExprGetExpr1 (c->data);
+ t2 = constraintExprData_binaryExprGetExpr2 (c->data);
+
+ binOP = constraintExprData_binaryExprGetOp (c->data);
+ if (binOP == BINARYOP_PLUS)
+ if (constraintExpr_isLit (t2) && constraintExpr_getValue (t2) == 1 )
+ {
+ return TRUE;
+ }
+ }
+
+ return FALSE;
+}
+ /*@noaccess constraintExpr @*/
+
+ /*@access constraintExpr @*/
+/* look for constraints like cexrp = cexrp + 1 */
+static bool incVar (/*@notnull@*/ constraint c) /*@*/
+{
+ constraintExpr t1;
+ if (c->ar != EQ)
+ {
+ return FALSE;
+ }
+ if (! isInc (c->expr ) )
+ return FALSE;
+
+ llassert (constraintExpr_isDefined (c->expr) );
+ llassert (c->expr->kind == binaryexpr);
+
+ t1 = constraintExprData_binaryExprGetExpr1 (c->expr->data);
+ if (constraintExpr_similar (c->lexpr, t1) )
+ return TRUE;
+
+ return FALSE;
+}
+/*@noaccess constraintExpr @*/
+
+