/*@-fcnuse*/
/*@-assignexpose*/
-constraint constraint_makeNew (void);
+/*@notnull@*/ constraint constraint_makeNew (void);
constraint makeConstraintParse (sRef x, lltok relOp, exprNode cconstant)
else if (relOp.tok == EQ_OP)
ret->ar = EQ;
else
- llfatalbug("Unsupported relational operator");
+ llfatalbug(message ("Unsupported relational operator") );
t = cstring_toCharsSafe (exprNode_unparse(cconstant));
int c;
constraint ret;
ret = constraint_makeNew();
- llassert (l);
+ llassert (l!=NULL);
if (!l)
return ret;
else if (relOp.tok == EQ_OP)
ret->ar = EQ;
else
- llfatalbug("Unsupported relational operator");
+ llfatalbug(message("Unsupported relational operator") );
t = cstring_toCharsSafe (exprNode_unparse(cconstant));
return ret;
}
+constraint constraint_same (constraint c1, constraint c2)
+{
+
+ if (c1->ar != c2->ar)
+ return FALSE;
+
+ if (!constraintExpr_similar (c1->lexpr, c2->lexpr) )
+ return FALSE;
+
+ if (!constraintExpr_similar (c1->expr, c2->expr) )
+ return FALSE;
+
+ return TRUE;
+}
constraint makeConstraintParse3 (constraintExpr l, lltok relOp, constraintExpr r)
{
constraint ret;
ret = constraint_makeNew();
- llassert (l);
+ llassert (l !=NULL);
if (!l)
return ret;
else if (relOp.tok == EQ_OP)
ret->ar = EQ;
else
- llfatalbug("Unsupported relational operator");
+ llfatalbug( message("Unsupported relational operator") );
ret->expr = constraintExpr_copy (r);
ret->post = TRUE;
+
+ ret->orig = constraint_copy(ret);
+
+ ret = constraint_simplify (ret);
+
// ret->orig = ret;
DPRINTF(("GENERATED CONSTRAINT:"));
DPRINTF( (message ("%s", constraint_print(ret) ) ) );
constraint constraint_copy (constraint c)
{
constraint ret;
+
+ llassert (c);
+
ret = constraint_makeNew();
ret->lexpr = constraintExpr_copy (c->lexpr);
ret->ar = c->ar;
ret->expr = constraintExpr_copy (c->expr);
ret->post = c->post;
- ret->generatingExpr = c->generatingExpr;
+ ret->generatingExpr = exprNode_fakeCopy(c->generatingExpr);
/*@i33 fix this*/
if (c->orig != NULL)
ret->orig = constraint_copy (c->orig);
else
ret->orig = NULL;
+
+ if (c->or != NULL)
+ ret->or = constraint_copy (c->or);
+ else
+ ret->or = NULL;
+
return ret;
}
c1->orig = constraint_copy (c2->orig);
else
c1->orig = NULL;
- c1->generatingExpr = c2->generatingExpr;
+
+ if (c2->or != NULL)
+ c1->or = constraint_copy (c2->or);
+ else
+ c1->or = NULL;
+
+ c1->generatingExpr = exprNode_fakeCopy (c2->generatingExpr );
}
bool constraint_resolve (/*@unused@*/ constraint c)
-constraint constraint_makeNew (void)
+/*@notnull@*/ constraint constraint_makeNew (void)
{
constraint ret;
ret = dmalloc(sizeof (*ret) );
ret->ar = LT;
ret->post = FALSE;
ret->orig = NULL;
+ ret->or = NULL;
ret->generatingExpr = NULL;
- /*@i23*/return ret;
+ return ret;
}
constraint constraint_addGeneratingExpr (/*@returned@*/ constraint c, exprNode e)
if (c->generatingExpr == NULL)
{
- c->generatingExpr = e;
+ c->generatingExpr = exprNode_fakeCopy(e);
DPRINTF ((message ("setting generatingExpr for %s to %s", constraint_print(c), exprNode_unparse(e) ) ));
}
else
bool constraint_hasMaxSet(constraint c)
{
- if (c->orig)
+ if (c->orig != NULL)
{
if (checkForMaxSet(c->orig) )
return TRUE;
return ret;
}
+constraint constraint_makeSRefReadSafeInt (sRef s, int ind)
+{
+ constraint ret = constraint_makeNew();
+
+
+ ret->lexpr = constraintExpr_makeSRefMaxRead (s);
+ ret->ar = GTE;
+ ret->expr = constraintExpr_makeValueInt (ind);
+ ret->post = TRUE;
+ /*@i1*/return ret;
+}
+
constraint constraint_makeEnsureMaxReadAtLeast (exprNode e1, exprNode t2, fileloc sequencePoint)
{
constraint ret = constraint_makeNew();
return ret;
}
+static constraint constraint_makeEnsuresOpConstraintExpr (constraintExpr c1, constraintExpr c2, fileloc sequencePoint, arithType ar)
+{
+
+ constraint ret;
+
+ llassert(c1 && c2);
+ // llassert(sequencePoint);
+
+ ret = constraint_makeNew();
+
+ ret->lexpr = c1;
+ ret->ar = ar;
+ ret->post = TRUE;
+ ret->expr = c2;
+ ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
+ return ret;
+}
static constraint constraint_makeEnsuresOp (exprNode e1, exprNode e2, fileloc sequencePoint, arithType ar)
{
- constraint ret = constraint_makeNew();
+ constraintExpr c1, c2;
+ constraint ret;
exprNode e;
-
- e = exprNode_fakeCopy(e1);
+
if (! (e1 && e2) )
{
llcontbug((message("null exprNode, Exprnodes are %s and %s",
exprNode_unparse(e1), exprNode_unparse(e2) )
));
}
-
- ret->lexpr = constraintExpr_makeValueExpr (e);
- ret->ar = ar;
- ret->post = TRUE;
- e = exprNode_fakeCopy(e2);
- ret->expr = constraintExpr_makeValueExpr (e);
+
+ // llassert (sequencePoint);
+
+ e = exprNode_fakeCopy(e1);
+ c1 = constraintExpr_makeValueExpr (e);
+
+ e = exprNode_fakeCopy(e2);
+ c2 = constraintExpr_makeValueExpr (e);
+
+ ret = constraint_makeEnsuresOpConstraintExpr (c1, c2, sequencePoint, ar);
- ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
return ret;
}
/*make constraint ensures e1 < e2 */
constraint constraint_makeEnsureLessThan (exprNode e1, exprNode e2, fileloc sequencePoint)
{
- return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, LT) );
+ 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)
constraint constraint_makeEnsureGreaterThan (exprNode e1, exprNode e2, fileloc sequencePoint)
{
- return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, GT) );
+ 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)
// }
-cstring arithType_print (arithType ar)
+cstring arithType_print (arithType ar) /*@*/
{
cstring st = cstring_undefined;
switch (ar)
errorLoc = loc;
if (constraint_getFileloc(c) )
- errorLoc = constraint_getFileloc(c);
-
+ /*@-branchstate@*/
+ errorLoc = constraint_getFileloc(c);
+ /*@=branchstate@*/
if (c->post)
{
if (!c->post)
{
- if (c->orig)
+ if (c->orig != NULL)
st = message ("Unresolved constraint:\nLclint is unable to resolve %s needed to satisfy %s", constraint_print (c), constraint_print(c->orig) );
else
st = message ("Unresolved constraint:\nLclint is unable to resolve %s", constraint_print (c));
}
else
{
- if (c->orig)
+ if (c->orig != NULL)
st = message ("Block Post condition:\nThis function block has the post condition %s\n based on %s", constraint_print (c), constraint_print(c->orig) );
else
st = message ("Block Post condition:\nThis function block has the post condition %s", constraint_print (c));
{
cstring st = cstring_undefined;
cstring type = cstring_undefined;
- llassert (c);
+ llassert (c !=NULL);
if (c->post)
{
type = cstring_makeLiteral ("Ensures: ");
return st;
}
-constraint constraint_doSRefFixBaseParam (constraint precondition,
+cstring constraint_printOr (constraint c) /*@*/
+{
+ cstring ret;
+ constraint temp;
+
+ ret = cstring_undefined;
+ temp = c;
+
+ ret = cstring_concat (ret, constraint_print(temp) );
+
+ temp = temp->or;
+
+ while (temp)
+ {
+ ret = cstring_concat (ret, cstring_makeLiteral (" OR ") );
+ ret = cstring_concat (ret, constraint_print(temp) );
+ temp = temp->or;
+ }
+
+ return ret;
+
+}
+
+/*@only@*/ constraint constraint_doSRefFixBaseParam (/*@returned@*/ /*@only@*/ constraint precondition,
exprNodeList arglist)
{
precondition->lexpr = constraintExpr_doSRefFixBaseParam (precondition->lexpr,
// return FALSE;
// }
-constraint constraint_preserveOrig (constraint c)
+/*@only@*/ constraint constraint_preserveOrig (/*@returned@*/ /*@only@*/ constraint c) /*@modifies c @*/
{
c->orig = constraint_copy (c);
return c;
andersk / splint.git / blobdiff