** constraintList.c
*/
+//#define DEBUGPRINT 1
+
# include <ctype.h> /* for isdigit */
# include "lclintMacros.nf"
# include "basic.h"
int c;
constraint ret;
ret = constraint_makeNew();
- llassert (x);
- if (!x)
+ llassert (sRef_isValid(x) );
+ if (!sRef_isValid(x))
return ret;
ret->ar = c->ar;
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);
c1->orig = constraint_copy (c2->orig);
else
c1->orig = NULL;
-
+ c1->generatingExpr = c2->generatingExpr;
}
bool constraint_resolve (/*@unused@*/ constraint c)
ret->ar = LT;
ret->post = FALSE;
ret->orig = NULL;
+ ret->generatingExpr = NULL;
/*@i23*/return ret;
}
+constraint constraint_addGeneratingExpr (/*@returned@*/ constraint c, exprNode e)
+{
+
+ 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;
+}
+
fileloc constraint_getFileloc (constraint c)
{
+ 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;
+
+ return FALSE;
+}
+
+bool constraint_hasMaxSet(constraint c)
+{
+ if (c->orig)
+ {
+ if (checkForMaxSet(c->orig) )
+ return TRUE;
+ }
+
+ return (checkForMaxSet(c) );
+}
+
constraint constraint_makeReadSafeExprNode ( exprNode po, exprNode ind)
{
constraint ret = constraint_makeNew();
ret->expr = constraintExpr_makeValueInt (ind);
/*@i1*/return ret;
}
-
+
+constraint constraint_makeSRefSetBufferSize (sRef s, int size)
+{
+ constraint ret = constraint_makeNew();
+ ret->lexpr = constraintExpr_makeSRefMaxset (s);
+ ret->ar = EQ;
+ ret->expr = constraintExpr_makeValueInt (size);
+ ret->post = TRUE;
+ /*@i1*/return ret;
+}
+
+constraint constraint_makeSRefWriteSafeInt (sRef s, int ind)
+{
+ constraint ret = constraint_makeNew();
+
+
+ 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();
ret->expr = constraintExpr_makeValueExpr (ind);
/*@i1*/return ret;
}
-
+
+
constraint constraint_makeReadSafeInt ( exprNode po, int ind)
{
constraint ret = constraint_makeNew();
}
-/* make constraint ensures e1 == e2 */
-
-constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
+static constraint constraint_makeEnsuresOp (exprNode e1, exprNode e2, fileloc sequencePoint, arithType ar)
{
constraint ret = constraint_makeNew();
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 = EQ;
+ ret->ar = ar;
ret->post = TRUE;
e = exprNode_fakeCopy(e2);
ret->expr = constraintExpr_makeValueExpr (e);
ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
-// fileloc_incColumn ( ret->lexpr->term->loc);
-// fileloc_incColumn ( ret->lexpr->term->loc);
return ret;
}
-exprNode exprNode_copyConstraints (exprNode dst, exprNode src)
+/* 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)
+{
+ 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) );
+}
+
+
+exprNode exprNode_copyConstraints (/*@returned@*/ exprNode dst, exprNode src)
{
dst->ensuresConstraints = constraintList_copy (src->ensuresConstraints );
dst->requiresConstraints = constraintList_copy (src->requiresConstraints );
return dst;
}
+constraint constraint_makeMaxSetSideEffectPostDecrement (exprNode e, fileloc sequencePoint)
+{
+ constraint ret = constraint_makeNew();
+ //constraintTerm term;
+
+ e = exprNode_fakeCopy(e);
+ ret->lexpr = constraintExpr_makeValueExpr (e);
+ ret->ar = EQ;
+ ret->post = TRUE;
+ ret->expr = constraintExpr_makeValueExpr (e);
+ ret->expr = constraintExpr_makeDecConstraintExpr (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_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
{
constraint ret = constraint_makeNew();
return st;
}
+void constraint_printError (constraint c, fileloc loc)
+{
+ cstring string;
+ fileloc errorLoc;
+
+ string = constraint_printDetailed (c);
+
+ errorLoc = loc;
+
+ if (constraint_getFileloc(c) )
+ errorLoc = constraint_getFileloc(c);
+
+
+ if (c->post)
+ {
+ voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
+ }
+ else
+ {
+ voptgenerror (FLG_FUNCTIONCONSTRAINT, string, errorLoc);
+ }
+
+}
cstring constraint_printDetailed (constraint c)
{
cstring st = cstring_undefined;
+
if (!c->post)
{
if (c->orig)
- st = message ("Unresolved constraint:\nLclint is unable to resolve %s needed to satisy %s", constraint_print (c), constraint_print(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));
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) )
+ {
+ cstring temp2;
+ temp2 = message ("\nHas MaxSet\n");
+ st = cstring_concat (st, temp2);
+ }
+ }
return st;
}
-cstring constraint_print (constraint c)
+cstring constraint_print (constraint c) /*@*/
{
cstring st = cstring_undefined;
cstring type = cstring_undefined;
}
+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) ) ) );
andersk / splint.git / blobdiff