** constraintList.c
*/
+//#define DEBUGPRINT 1
+
# include <ctype.h> /* for isdigit */
# include "lclintMacros.nf"
# include "basic.h"
# include "exprChecks.h"
# include "aliasChecks.h"
# include "exprNodeSList.h"
-# include "exprData.i"
+//# include "exprData.i"
/*@i33*/
/*@-fcnuse*/
/*@-assignexpose*/
+constraint constraint_makeNew (void);
+
+
+constraint makeConstraintParse (sRef x, lltok relOp, exprNode cconstant)
+
+{
+ char *t;
+ int c;
+ constraint ret;
+ ret = constraint_makeNew();
+ llassert (sRef_isValid(x) );
+ if (!sRef_isValid(x))
+ return ret;
+
+
+ ret->lexpr = constraintExpr_makeTermsRef (x);
+ #warning fix abstraction
+
+ if (relOp.tok == GE_OP)
+ ret->ar = GTE;
+ else if (relOp.tok == LE_OP)
+ ret->ar = LTE;
+ else if (relOp.tok == EQ_OP)
+ ret->ar = EQ;
+ else
+ llfatalbug("Unsupported relational operator");
+
+
+ t = cstring_toCharsSafe (exprNode_unparse(cconstant));
+ c = atoi( t );
+ ret->expr = constraintExpr_makeIntLiteral (c);
+
+ ret->post = TRUE;
+ // ret->orig = ret;
+ DPRINTF(("GENERATED CONSTRAINT:"));
+ DPRINTF( (message ("%s", constraint_print(ret) ) ) );
+ return ret;
+}
+
+constraint makeConstraintParse2 (constraintExpr l, lltok relOp, exprNode cconstant)
+
+{
+ char *t;
+ int c;
+ constraint ret;
+ ret = constraint_makeNew();
+ llassert (l);
+ if (!l)
+ return ret;
+
+
+ ret->lexpr = constraintExpr_copy (l);
+ #warning fix abstraction
+
+ if (relOp.tok == GE_OP)
+ ret->ar = GTE;
+ else if (relOp.tok == LE_OP)
+ ret->ar = LTE;
+ else if (relOp.tok == EQ_OP)
+ ret->ar = EQ;
+ else
+ llfatalbug("Unsupported relational operator");
+
+
+ t = cstring_toCharsSafe (exprNode_unparse(cconstant));
+ c = atoi( t );
+ ret->expr = constraintExpr_makeIntLiteral (c);
+
+ ret->post = TRUE;
+ // ret->orig = ret;
+ DPRINTF(("GENERATED CONSTRAINT:"));
+ DPRINTF( (message ("%s", constraint_print(ret) ) ) );
+ return ret;
+}
+
+
+constraint makeConstraintParse3 (constraintExpr l, lltok relOp, constraintExpr r)
+{
+ constraint ret;
+ ret = constraint_makeNew();
+ llassert (l);
+ if (!l)
+ return ret;
+
+
+ ret->lexpr = constraintExpr_copy (l);
+ #warning fix abstraction
+
+ if (relOp.tok == GE_OP)
+ ret->ar = GTE;
+ else if (relOp.tok == LE_OP)
+ ret->ar = LTE;
+ else if (relOp.tok == EQ_OP)
+ ret->ar = EQ;
+ else
+ llfatalbug("Unsupported relational operator");
+
+ ret->expr = constraintExpr_copy (r);
+
+ ret->post = TRUE;
+ // ret->orig = ret;
+ DPRINTF(("GENERATED CONSTRAINT:"));
+ DPRINTF( (message ("%s", constraint_print(ret) ) ) );
+ return ret;
+}
+
constraint constraint_copy (constraint c)
{
constraint ret;
ret = constraint_makeNew();
- ret->c1 = c->c1;
- ret->t1 = c->t1;
+ ret->lexpr = constraintExpr_copy (c->lexpr);
ret->ar = c->ar;
- ret->e1 = c->e1;
+ ret->expr = constraintExpr_copy (c->expr);
ret->post = c->post;
+ ret->generatingExpr = c->generatingExpr;
+
+ /*@i33 fix this*/
+ if (c->orig != NULL)
+ ret->orig = constraint_copy (c->orig);
+ else
+ ret->orig = NULL;
return ret;
}
+/*like copy expect it doesn't allocate memory for the constraint*/
+
+void constraint_overWrite (constraint c1, constraint c2)
+{
+ c1->lexpr = constraintExpr_copy (c2->lexpr);
+ c1->ar = c2->ar;
+ c1->expr = constraintExpr_copy (c2->expr);
+ c1->post = c2->post;
+ /*@i33 fix this*/
+ if (c2->orig != NULL)
+ c1->orig = constraint_copy (c2->orig);
+ else
+ c1->orig = NULL;
+ c1->generatingExpr = c2->generatingExpr;
+}
+
bool constraint_resolve (/*@unused@*/ constraint c)
{
return FALSE;
}
-/*@notnull@*/
-/*@special@*/ constraint constraint_makeNew (void)
- /*@post:isnull result->t1, result->e1, result->c1@*/
- /*@defines result->ar, result->post@*/
+
+
+constraint constraint_makeNew (void)
{
constraint ret;
ret = dmalloc(sizeof (*ret) );
- ret->t1 = NULL;
- ret->e1 = NULL;
- ret->c1 = NULL;
+ ret->lexpr = NULL;
+ ret->expr = NULL;
ret->ar = LT;
ret->post = FALSE;
+ ret->orig = NULL;
+ ret->generatingExpr = NULL;
/*@i23*/return ret;
}
-/*@-czechfcns@*/
-/*@out@*/ constraintTerm new_constraintTermExpr (void)
+constraint constraint_addGeneratingExpr (/*@returned@*/ constraint c, exprNode e)
{
- constraintTerm ret;
- ret = dmalloc (sizeof (* ret ) );
-
- return ret;
+
+ if (c->generatingExpr == NULL)
+ {
+ c->generatingExpr = e;
+ DPRINTF ((message ("setting generatingExpr for %s to %s", constraint_print(c), exprNode_unparse(e) ) ));
+ }
+ else
+ {
+ DPRINTF ((message ("Not setting generatingExpr for %s to %s", constraint_print(c), exprNode_unparse(e) ) ));
+ }
+ return c;
}
-constraintTerm exprNode_makeConstraintTerm (/*@only@*/ exprNode e)
+fileloc constraint_getFileloc (constraint c)
{
- constraintTerm ret = new_constraintTermExpr();
- ret->loc = exprNode_getfileloc(e);
- ret->value.expr = e;
- ret->kind = EXPRNODE;
- return ret;
+ if (c->generatingExpr)
+ return (exprNode_getfileloc (c->generatingExpr) );
+
+ return (constraintExpr_getFileloc (c->lexpr) );
+
+
}
+static bool checkForMaxSet (constraint c)
+{
+ if (constraintExpr_hasMaxSet(c->lexpr) || constraintExpr_hasMaxSet(c->expr) )
+ return TRUE;
-constraintTerm intLit_makeConstraintTerm (int i)
+ return FALSE;
+}
+
+bool constraint_hasMaxSet(constraint c)
{
- constraintTerm ret = new_constraintTermExpr();
- ret->value.intlit = i;
- ret->kind = INTLITERAL;
- ret->loc = fileloc_undefined;
- return ret;
+ if (c->orig)
+ {
+ if (checkForMaxSet(c->orig) )
+ return TRUE;
+ }
+
+ return (checkForMaxSet(c) );
}
-
-/*@special@*/ constraintExpr makeConstraintExpr (/*@only@*/ /*@notnull@*/ constraintTerm term)
- /*@post:isnull result->e1@*/
- /*@post:notnull result->t1@*/
- /*@defines result->e1, result->t1, result->c1@, result->op*/
-{
- constraintExpr ret;
- ret = dmalloc (sizeof (*ret) );
- ret->t1 = term;
- ret->e1 = NULL;
- ret->c1 = UNDEFINED;
- ret->op = PLUS;
+constraint constraint_makeReadSafeExprNode ( exprNode po, exprNode ind)
+{
+ constraint ret = constraint_makeNew();
+ // constraintTerm term;
+ po = exprNode_fakeCopy(po);
+ ind = exprNode_fakeCopy(ind);
+ ret->lexpr = constraintExpr_makeMaxReadExpr(po);
+ ret->ar = GTE;
+ ret->expr = constraintExpr_makeValueExpr (ind);
return ret;
}
+constraint constraint_makeWriteSafeInt (exprNode po, int ind)
+{
+ constraint ret = constraint_makeNew();
- constraintExpr makeConstraintExprIntlit (int i)
+
+ ret->lexpr =constraintExpr_makeMaxSetExpr(po);
+ ret->ar = GTE;
+ ret->expr = constraintExpr_makeValueInt (ind);
+ /*@i1*/return ret;
+}
+
+constraint constraint_makeSRefSetBufferSize (sRef s, int size)
{
- constraintExpr ret;
- ret = dmalloc (sizeof (*ret) );
- ret->t1 = intLit_makeConstraintTerm (i);
- ret->e1 = NULL;
- ret->c1 = VALUE;
- ret->op = PLUS;
- /*@i1*/ return ret;
+ constraint ret = constraint_makeNew();
+ ret->lexpr = constraintExpr_makeSRefMaxset (s);
+ ret->ar = EQ;
+ ret->expr = constraintExpr_makeValueInt (size);
+ ret->post = TRUE;
+ /*@i1*/return ret;
}
-
-/*@i33*/
-/*@null@*/ constraint constraint_makeReadSafeExprNode ( exprNode po, exprNode ind)
+constraint constraint_makeSRefWriteSafeInt (sRef s, int ind)
{
constraint ret = constraint_makeNew();
- constraintTerm term;
- po = exprNode_fakeCopy(po);
- ind = exprNode_fakeCopy(ind);
- printf ("Requires maxr(%s) >= %s\n", cstring_toCharsSafe (exprNode_unparse (po ) ),
- cstring_toCharsSafe ( exprNode_unparse (ind) ) );
- ret->t1 = exprNode_makeConstraintTerm(po);
- ret->c1 = MAXREAD;
- ret->ar = GTE;
- term = exprNode_makeConstraintTerm (ind);
-
- ret->e1 = makeConstraintExpr (term);
- ret->e1->c1 = VALUE;
+
+ ret->lexpr = constraintExpr_makeSRefMaxset (s);
+ ret->ar = GTE;
+ ret->expr = constraintExpr_makeValueInt (ind);
+ ret->post = TRUE;
/*@i1*/return ret;
}
+/* drl added 01/12/2000
+
+ makes the constraint: Ensures index <= MaxRead(buffer) */
+
+constraint constraint_makeEnsureLteMaxRead(exprNode index, exprNode buffer)
+{
+ constraint ret = constraint_makeNew();
+
+ ret->lexpr = constraintExpr_makeValueExpr (index);
+ ret->ar = LTE;
+ ret->expr = constraintExpr_makeMaxReadExpr(buffer);
+ ret->post = TRUE;
+ return ret;
+}
+
constraint constraint_makeWriteSafeExprNode (exprNode po, exprNode ind)
{
constraint ret = constraint_makeNew();
- constraintTerm term;
- printf ("Requires maxw(%s) >= %s\n", cstring_toCharsSafe (exprNode_unparse (po ) ),
- cstring_toCharsSafe( exprNode_unparse (ind) ) );
- ret->t1 = exprNode_makeConstraintTerm(po);
- ret->c1 = MAXSET;
- ret->ar = GTE;
- term = exprNode_makeConstraintTerm(ind);
-
- ret->e1 = makeConstraintExpr (term);
- ret->e1->c1 = VALUE;
+
+ ret->lexpr =constraintExpr_makeMaxSetExpr(po);
+ ret->ar = GTE;
+ ret->expr = constraintExpr_makeValueExpr (ind);
/*@i1*/return ret;
}
-constraint constraint_makeReadSafeInt (exprNode t1, int index)
+constraint constraint_makeReadSafeInt ( exprNode po, int ind)
{
constraint ret = constraint_makeNew();
- constraintTerm term;
- printf ("Ensures maxr((valueof(%s)) >= %d\n", cstring_toCharsSafe (exprNode_unparse (t1 ) ),
- index );
- t1 = exprNode_fakeCopy(t1);
- ret->t1 = exprNode_makeConstraintTerm(t1);
- ret->c1 = MAXREAD;
- ret->ar = GTE;
- ret->post = TRUE;
- term = intLit_makeConstraintTerm(index);
+
+ po = exprNode_fakeCopy(po);
- ret->e1 = makeConstraintExpr (term);
- ret->e1->c1 = VALUE;
- /*make this refer to element after preconditions */
- fileloc_incColumn (ret->t1->loc);
- /*@i1*/ return ret;
+ ret->lexpr = constraintExpr_makeMaxReadExpr(po);
+ ret->ar = GTE;
+ ret->expr = constraintExpr_makeValueInt (ind);
+ return ret;
}
-
-constraint constraint_makeEnsureMaxReadAtLeast (exprNode t1, exprNode t2, fileloc sequencePoint)
+constraint constraint_makeEnsureMaxReadAtLeast (exprNode e1, exprNode t2, fileloc sequencePoint)
{
constraint ret = constraint_makeNew();
- constraintTerm term;
- t1 = exprNode_fakeCopy (t1);
+
+ e1 = exprNode_fakeCopy (e1);
t2 = exprNode_fakeCopy (t2);
- ret->t1 = exprNode_makeConstraintTerm(t1);
+ ret = constraint_makeReadSafeExprNode(e1, t2);
- if (ret->t1->loc != NULL)
- fileloc_free(ret->t1->loc);
+ ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
- ret->t1->loc = fileloc_copy (sequencePoint);
- ret->c1 = MAXREAD;
- ret->ar = GTE;
ret->post = TRUE;
- term = exprNode_makeConstraintTerm (t2);
-
- ret->e1 = makeConstraintExpr (term);
- ret->e1->c1 = VALUE;
- /*make this refer to element after preconditions */
- fileloc_incColumn (ret->t1->loc);
- /*@i1*/ return ret;
+
+ // fileloc_incColumn (ret->lexpr->term->loc);
+ return ret;
}
-constraint constraint_makeEnsureMinReadAtMost (exprNode po, exprNode ind, fileloc sequencePoint)
+
+static constraint constraint_makeEnsuresOp (exprNode e1, exprNode e2, fileloc sequencePoint, arithType ar)
{
constraint ret = constraint_makeNew();
- constraintTerm term;
-
- po = exprNode_fakeCopy (po);
- ind = exprNode_fakeCopy (ind);
+ exprNode e;
- ret->t1 = exprNode_makeConstraintTerm(po);
- ret->c1 = MINREAD;
- ret->ar = LTE;
+ 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;
- term = exprNode_makeConstraintTerm (ind);
+ e = exprNode_fakeCopy(e2);
+ ret->expr = constraintExpr_makeValueExpr (e);
- ret->e1 = makeConstraintExpr (term);
- ret->e1->c1 = VALUE;
- /*make this refer to element after preconditions */
- fileloc_incColumn (ret->t1->loc);
- /*@i1*/ return ret;
+ ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
+ return ret;
}
-constraintExpr makePostOpInc (exprNode t1)
+
+/* make constraint ensures e1 == e2 */
+
+constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
{
- constraintExpr ret;
- constraintTerm term;
+ return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, EQ) );
+}
- t1 = exprNode_fakeCopy (t1);
- term = exprNode_makeConstraintTerm(t1);
- ret = makeConstraintExpr (term);
- ret->op = PLUS;
- ret->c1 = VALUE;
- ret->e1 = makeConstraintExprIntlit (1);
- return ret;
+/*make constraint ensures e1 < e2 */
+constraint constraint_makeEnsureLessThan (exprNode e1, exprNode e2, fileloc sequencePoint)
+{
+ return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, LT) );
+}
+
+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)
+{
+ return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, GT) );
+}
+
+constraint constraint_makeEnsureGreaterThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
+{
+ return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, GTE) );
}
-constraint constraint_makeSideEffectPostIncrement (exprNode t1, fileloc sequencePoint)
+
+exprNode exprNode_copyConstraints (/*@returned@*/ exprNode dst, exprNode src)
+{
+ 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;
+}
+
+constraint constraint_makeMaxSetSideEffectPostDecrement (exprNode e, fileloc sequencePoint)
{
constraint ret = constraint_makeNew();
//constraintTerm term;
- exprNode t2;
- t1 = exprNode_fakeCopy(t1);
- t2 = exprNode_fakeCopy(t1);
-
- ret->t1 = exprNode_makeConstraintTerm(t1);
- ret->c1 = VALUE;
+
+ e = exprNode_fakeCopy(e);
+ ret->lexpr = constraintExpr_makeValueExpr (e);
ret->ar = EQ;
ret->post = TRUE;
- ret->e1 = makePostOpInc(t2);
+ ret->expr = constraintExpr_makeValueExpr (e);
+ ret->expr = constraintExpr_makeDecConstraintExpr (ret->expr);
- fileloc_incColumn ( ret->t1->loc);
- fileloc_incColumn ( ret->t1->loc);
-
- /*@i6*/return ret;
+ ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
+// fileloc_incColumn ( ret->lexpr->term->loc);
+// fileloc_incColumn ( ret->lexpr->term->loc);
+ return ret;
}
+constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
+{
+ constraint ret = constraint_makeNew();
+ //constraintTerm term;
-void constraintType_print (constraintType c1)
+ e = exprNode_fakeCopy(e);
+ ret->lexpr = constraintExpr_makeValueExpr (e);
+ ret->ar = EQ;
+ ret->post = TRUE;
+ ret->expr = constraintExpr_makeValueExpr (e);
+ ret->expr = constraintExpr_makeIncConstraintExpr (ret->expr);
+
+ ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
+// fileloc_incColumn ( ret->lexpr->term->loc);
+// fileloc_incColumn ( ret->lexpr->term->loc);
+ return ret;
+}
+
+
+
+// constraint constraint_makeMaxReadSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
+// {
+// constraint ret = constraint_makeNew();
+// //constraintTerm term;
+
+// e = exprNode_fakeCopy(e);
+// ret->lexpr = constraintExpr_makeMaxReadExpr(e);
+// ret->ar = EQ;
+// ret->post = TRUE;
+// ret->expr = constraintExpr_makeIncConstraintExpr (e);
+// ret->lexpr = constraintExpr_setFileLoc (ret->lexpr, sequencePoint);
+// return ret;
+// }
+
+
+cstring arithType_print (arithType ar)
{
- switch (c1)
+ cstring st = cstring_undefined;
+ switch (ar)
{
- case VALUE:
- printf("VALUE");
- break;
- case CALLSAFE:
- printf("CALLSAFE");
+ case LT:
+ st = cstring_makeLiteral (" < ");
break;
- case MAXSET:
- printf ("MAXSET");
+ case LTE:
+ st = cstring_makeLiteral (" <= ");
break;
- case MINSET:
- printf ("MINSET");
+ case GT:
+ st = cstring_makeLiteral (" > ");
break;
- case MAXREAD:
- printf ("MAXREAD");
+ case GTE:
+ st = cstring_makeLiteral (" >= ");
break;
- case MINREAD:
- printf ("MINREAD");
+ case EQ:
+ st = cstring_makeLiteral (" == ");
break;
- case NULLTERMINATED:
- printf ("NULLTERMINATED");
+ case NONNEGATIVE:
+ st = cstring_makeLiteral (" NONNEGATIVE ");
break;
- case UNDEFINED:
- TPRINTF(("Unhandled value for constraintType"));
- llassert(FALSE);
+ case POSITIVE:
+ st = cstring_makeLiteral (" POSITIVE ");
break;
default:
- TPRINTF(("Unhandled value for constraintType"));
llassert(FALSE);
+ break;
}
+ return st;
}
-void constraintTerm_print (constraintTerm term)
+
+void constraint_printError (constraint c, fileloc loc)
{
- cstring s;
+ cstring string;
+ fileloc errorLoc;
+
+ string = constraint_printDetailed (c);
- llassert (term != NULL);
- switch (term->kind)
- {
- case EXPRNODE:
- s = exprNode_unparse (term->value.expr);
- printf(" %s", cstring_toCharsSafe(s) );
- s = fileloc_unparse (term->loc);
- printf("@ %s", cstring_toCharsSafe(s) );
- cstring_free(s);
- break;
- case INTLITERAL:
+ errorLoc = loc;
+
+ if (constraint_getFileloc(c) )
+ errorLoc = constraint_getFileloc(c);
+
+
+ if (c->post)
{
- char * buf = malloc (15);
- /*@i1*/snprintf (buf, 14, "intliteral(%d)", term->value.intlit);
- /*@i1*/ printf(" %s ", buf);
- free (buf);
- break;
+ voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
}
- case SREF:
- TPRINTF( ("Not Implemented\n"));
- llassert(FALSE);
- break;
+ else
+ {
+ voptgenerror (FLG_FUNCTIONCONSTRAINT, string, errorLoc);
}
- /*@-unreachable*/
- return;
- /*@=unreachable*/
+
}
-void arithType_print (arithType ar)
+cstring constraint_printDetailed (constraint c)
{
- switch (ar)
+ cstring st = cstring_undefined;
+
+
+ if (!c->post)
{
- case LT:
- printf(" < ");
- return;
- case LTE:
- printf(" <= ");
- return;
- case GT:
- printf(" > ");
- return;
- case GTE:
- printf(" <= ");
- return;
- case EQ:
- printf(" == ");
- return;
- case NONNEGATIVE:
- printf(" NONNEGATIVE ");
- return;
- case POSITIVE:
- printf(" POSITIVE ");
- return;
- default:
- llassert(FALSE);
+ if (c->orig)
+ 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));
+
}
-}
-
-void constraintExpr_print (constraintExpr ex)
-{
- llassert (ex != NULL);
- constraintType_print (ex->c1 );
- constraintTerm_print (ex->t1);
- if (ex->e1 != NULL)
+ else
{
- if (ex->op == PLUS)
- {
- printf(" + ");
- }
+ if (c->orig)
+ 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));
+ }
+
+ if (context_getFlag (FLG_CONSTRAINTLOCATION) )
+ {
+ cstring temp;
+ // llassert (c->generatingExpr);
+ temp = message ("\nOriginal Generating expression %s: %s\n", fileloc_unparse( exprNode_getfileloc (c->generatingExpr) ),
+ exprNode_unparse(c->generatingExpr) );
+ st = cstring_concat (st, temp);
+
+ if (constraint_hasMaxSet(c) )
{
- printf (" - ");
+ cstring temp2;
+ temp2 = message ("\nHas MaxSet\n");
+ st = cstring_concat (st, temp2);
}
-
- constraintExpr_print (ex->e1);
}
-
+ return st;
}
-
-void constraint_print (constraint c)
+cstring constraint_print (constraint c) /*@*/
{
+ cstring st = cstring_undefined;
+ cstring type = cstring_undefined;
+ llassert (c);
if (c->post)
{
- printf("Ensures: ");
+ type = cstring_makeLiteral ("Ensures: ");
}
else
{
- printf("requires: ");
+ type = cstring_makeLiteral ("Requires: ");
}
-
- constraintType_print (c->c1);
- constraintTerm_print (c->t1);
- arithType_print(c->ar);
- constraintExpr_print(c->e1);
- printf("\n");
+ st = message ("%s: %s %s %s",
+ type,
+ constraintExpr_print (c->lexpr),
+ arithType_print(c->ar),
+ constraintExpr_print(c->expr)
+ );
+ return st;
+}
+
+constraint constraint_doSRefFixBaseParam (constraint precondition,
+ exprNodeList arglist)
+{
+ precondition->lexpr = constraintExpr_doSRefFixBaseParam (precondition->lexpr,
+ arglist);
+ precondition->expr = constraintExpr_doSRefFixBaseParam (precondition->expr,
+ arglist);
+
+ return precondition;
}
+
+constraint constraint_doFixResult (constraint postcondition, exprNode fcnCall)
+{
+ postcondition = constraint_copy (postcondition);
+ postcondition->lexpr = constraintExpr_doFixResult (postcondition->lexpr, fcnCall);
+ postcondition->expr = constraintExpr_doFixResult (postcondition->expr, fcnCall);
+
+ return postcondition;
+}
+
+constraint constraint_doSRefFixConstraintParam (constraint precondition,
+ exprNodeList arglist)
+{
+
+ precondition = constraint_copy (precondition);
+ precondition->lexpr = constraintExpr_doSRefFixConstraintParam (precondition->lexpr, arglist);
+ precondition->expr = constraintExpr_doSRefFixConstraintParam (precondition->expr, arglist);
+
+ return precondition;
+}
+
+// bool constraint_hasTerm (constraint c, constraintTerm term)
+// {
+// DPRINTF((message ("Constraint %s", constraint_print (c) ) ) );
+
+// if (constraintExpr_includesTerm (c->lexpr, term) )
+// return TRUE;
+
+// if (constraintExpr_includesTerm (c->expr, term) )
+// return TRUE;
+
+// return FALSE;
+// }
+
+constraint constraint_preserveOrig (constraint c)
+{
+ c->orig = constraint_copy (c);
+ return c;
+}
/*@=fcnuse*/
/*@=assignexpose*/
/*@=czechfcns@*/
-
andersk / splint.git / blobdiff