/*@i33*/
-/*@access exprNode @*/
-
+/*@access exprNode@*/ /* !!! NO! Don't do this recklessly! */
+/*@-nullderef@*/ /* !!! DRL needs to fix this code! */
+/*@-nullstate@*/ /* !!! DRL needs to fix this code! */
+/*@-temptrans@*/ /* !!! DRL needs to fix this code! */
static /*@only@*/ cstring constraint_printDetailedPostCondition (/*@observer@*/ /*@temp@*/ constraint p_c);
ret->lexpr = constraintExpr_copy (l);
- if (relOp.tok == GE_OP)
+ if (lltok_getTok (relOp) == GE_OP)
+ {
ret->ar = GTE;
- else if (relOp.tok == LE_OP)
- ret->ar = LTE;
- else if (relOp.tok == EQ_OP)
- ret->ar = EQ;
+ }
+ else if (lltok_getTok (relOp) == LE_OP)
+ {
+ ret->ar = LTE;
+ }
+ else if (lltok_getTok (relOp) == EQ_OP)
+ {
+ ret->ar = EQ;
+ }
else
- llfatalbug ( message ("Unsupported relational operator"));
+ llfatalbug ( message ("Unsupported relational operator"));
ret->expr = constraintExpr_copy (r);
return FALSE;
}
-constraint constraint_makeReadSafeExprNode ( exprNode po, exprNode ind)
+constraint constraint_makeReadSafeExprNode (exprNode po, exprNode ind)
{
constraint ret = constraint_makeNew ();
constraint constraint_makeEnsureLessThan (exprNode e1, exprNode e2, fileloc sequencePoint)
{
constraintExpr t1, t2;
+ constraint t3;
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));
+
+ t3 = constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, LTE);
+
+ t3 = constraint_simplify(t3);
+ return (t3);
}
constraint constraint_makeEnsureLessThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
constraint constraint_makeEnsureGreaterThan (exprNode e1, exprNode e2, fileloc sequencePoint)
{
constraintExpr t1, t2;
+ constraint t3;
t1 = constraintExpr_makeValueExpr (e1);
t2 = constraintExpr_makeValueExpr (e2);
/* change this to e1 >= (e2 + 1) */
t2 = constraintExpr_makeIncConstraintExpr (t2);
+ t3 = constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, GTE);
+
+ t3 = constraint_simplify(t3);
- return ( constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, GTE));
+ return t3;
}
constraint constraint_makeEnsureGreaterThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
precondition->expr = constraintExpr_doSRefFixConstraintParam (precondition->expr, arglist);
precondition->fcnPre = FALSE;
- return precondition;
+ return constraint_simplify(precondition);
}
constraint constraint_preserveOrig (/*@returned@*/ constraint c) /*@modifies c @*/