typedef enum
{
- LT, LTE, GT, GTE, EQ, NONNEGATIVE, POSITIVE
+ LT, LTE, GT, GTE, EQ, NONNEGATIVE, POSITIVE, CASTEQ
}
arithType;
struct s_constraint {
- constraint orig;
- constraint or;
- bool fcnPre;
+ arithType ar;
+ constraint orig;
+ constraint or;
+ bool fcnPre;
constraintExpr lexpr;
- arithType ar;
- constraintExpr expr;
+ constraintExpr expr;
bool post;
/*@exposed@*/ /*@dependent@*/ exprNode generatingExpr;
} ;
extern void exprNode_exprTraverse (exprNode p_e, bool p_definatelv, bool p_definaterv, /*@temp@*/ /*@observer@*/ fileloc p_sequencePoint);
extern /*@only@*/ constraintList
-exprNode_traversRequiresConstraints (exprNode p_e);
+exprNode_traverseRequiresConstraints (exprNode p_e);
extern /*@only@*/ constraintList
-exprNode_traversEnsuresConstraints (exprNode p_e);
+exprNode_traverseEnsuresConstraints (exprNode p_e);
extern constraint constraint_togglePost (/*@returned@*/ constraint p_c);
extern bool constraint_same (constraint p_c1, constraint p_c2) ;
binaryexpr,
unaryExpr,
term
-}
-constraintExprKind;
+} constraintExprKind;
struct s_constraintExpr {
constraintExprKind kind;
bool constraintExpr_search (/*@observer@*/ /*@temp@*/ constraintExpr p_c, /*@observer@*/ /*@temp@*/ constraintExpr p_old);
-/*@only@*/ fileloc constraintExpr_getFileloc (constraintExpr p_expr);
+/*@only@*/ fileloc constraintExpr_loc (constraintExpr p_expr);
/*@only@*/ constraintExpr constraintExpr_makeSRefMaxset ( /*@temp@*/ /*@observer@*/ sRef p_s);
extern void constraintList_printErrorPostConditions (constraintList p_s, fileloc p_loc) ;
extern void constraintList_printError (constraintList p_s, /*@observer@*/ fileloc p_loc) ;
-extern constraintList constraintList_sort (/*@returned@*/ constraintList p_ret) /*@modifies p_ret@*/ ;
+extern constraintList constraintList_sort (/*@returned@*/ constraintList p_ret)
+ /*@modifies p_ret@*/ ;
-void constraintList_dump (/*@observer@*/ constraintList p_c, FILE * p_f);
+extern void constraintList_castConstraints (constraintList p_c, ctype p_tfrom, ctype p_tto)
+ /*@modifies p_c@*/ ;
+
+extern void constraintList_dump (/*@observer@*/ constraintList p_c, FILE * p_f);
/*@only@*/ constraintList constraintList_undump (FILE * p_f);
/*@only@*/ constraintList constraintList_removeSurpressed (/*@only@*/ constraintList p_s);
bool constraintTerm_similar (constraintTerm p_term1, constraintTerm p_term2) /*@*/;
-bool constraintTerm_canGetValue (constraintTerm p_term)/*@*/;
-long constraintTerm_getValue (constraintTerm p_term) /*@*/;
+extern bool constraintTerm_canGetValue (constraintTerm p_term)/*@*/;
+extern long constraintTerm_getValue (constraintTerm p_term) /*@*/;
+extern void constraintTerm_setValue (constraintTerm p_term, long p_value) /*@modifies p_term@*/;
-fileloc constraintTerm_getFileloc (constraintTerm p_t) /*@*/;
+extern fileloc constraintTerm_getFileloc (constraintTerm p_t) /*@*/;
+extern bool constraintTerm_isIntLiteral (constraintTerm p_term) /*@*/;
-bool constraintTerm_isIntLiteral (constraintTerm p_term) /*@*/;
-
-constraintTerm constraintTerm_makesRef (/*@temp@*/ /*@observer@*/ sRef p_s) /*@*/;
+extern constraintTerm constraintTerm_makesRef (/*@temp@*/ /*@observer@*/ sRef p_s) /*@*/;
/*@unused@*/ bool constraintTerm_probSame (constraintTerm p_term1, constraintTerm p_term2) /*@*/;
fileloc loc;
/*@relnull@*/ exprData edata;
cstring etext;
- /*@notnull@*/ constraintList requiresConstraints;
+ /*@notnull@*/ constraintList requiresConstraints;
/*@notnull@*/ constraintList ensuresConstraints;
/*
extern bool ctype_isUnnamedSU (ctype p_c) /*@*/ ;
extern bool ctype_isUser (ctype p_c) /*@*/ ;
+extern int ctype_getSize (ctype p_c)
+ /* EFFECTS: Returns the expected size of type p_c. Various flags to control?
+ ** Returns -1 if the size is unknown (or should not be guessed).
+ */
+ /*@*/ ;
+
extern ctype ctype_biggerType (ctype p_c1, ctype p_c2)
/* EFFECTS: returns whichever of c1 or c2 is bigger (storage requirements).
If they are equal, returns c1. */
if (exprNode_isDefined (c->generatingExpr))
return (fileloc_copy (exprNode_loc (c->generatingExpr)));
- return (constraintExpr_getFileloc (c->lexpr));
+ return (constraintExpr_loc (c->lexpr));
}
static bool checkForMaxSet (constraint c)
constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
{
- return (constraint_makeEnsuresOp (e1, e2, sequencePoint, EQ));
+ if (FALSE) /* (!ctype_almostEqual (exprNode_getType (e1), exprNode_getType (e2))) */
+ {
+ /* If the types are not identical, need to be careful the element sizes may be different. */
+ //! return (constraint_makeEnsuresOp (e1, e2, sequencePoint, CASTEQ));
+ BADBRANCH;
+ }
+ else
+ {
+ return (constraint_makeEnsuresOp (e1, e2, sequencePoint, EQ));
+ }
}
/* make constraint ensures e1 < e2 */
case LT:
st = cstring_makeLiteral ("<");
break;
- case LTE:
+ case LTE:
st = cstring_makeLiteral ("<=");
break;
- case GT:
+ case GT:
st = cstring_makeLiteral (">");
break;
- case GTE:
+ case GTE:
st = cstring_makeLiteral (">=");
break;
- case EQ:
+ case EQ:
st = cstring_makeLiteral ("==");
break;
- case NONNEGATIVE:
+ case CASTEQ:
+ st = cstring_makeLiteral ("(!)==");
+ break;
+ case NONNEGATIVE:
st = cstring_makeLiteral ("NONNEGATIVE");
break;
- case POSITIVE:
+ case POSITIVE:
st = cstring_makeLiteral ("POSITIVE");
break;
default:
fileloc errorLoc, temp;
string = constraint_unparseDetailedPostCondition (c);
-
errorLoc = loc;
-
loc = NULL;
temp = constraint_getFileloc (c);
-
- if (context_getFlag (FLG_BOUNDSCOMPACTERRORMESSAGES ) )
+ if (context_getFlag (FLG_BOUNDSCOMPACTERRORMESSAGES))
{
- string = cstring_replaceChar(string, '\n', ' ');
+ string = cstring_replaceChar (string, '\n', ' ');
}
if (fileloc_isDefined (temp))
{
errorLoc = temp;
- voptgenerror ( FLG_CHECKPOST, string, errorLoc);
+ voptgenerror (FLG_CHECKPOST, string, errorLoc);
fileloc_free (temp);
}
else
{
- voptgenerror ( FLG_CHECKPOST, string, errorLoc);
+ voptgenerror (FLG_CHECKPOST, string, errorLoc);
}
}
errorLoc = constraint_getFileloc (c);
ret = message ("constraint: %q @ %q", string, fileloc_unparse (errorLoc));
-
fileloc_free (errorLoc);
return ret;
fileloc errorLoc, temp;
bool isLikely;
-
llassert (constraint_isDefined (c) );
else
{
llassert (FALSE);
- DPRINTF (("constraint %s had undefined fileloc %s", constraint_unparse (c), fileloc_unparse (temp)));
+ DPRINTF (("constraint %s had undefined fileloc %s",
+ constraint_unparse (c), fileloc_unparse (temp)));
fileloc_free (temp);
errorLoc = fileloc_copy (errorLoc);
}
- if (context_getFlag (FLG_BOUNDSCOMPACTERRORMESSAGES ) )
+ if (context_getFlag (FLG_BOUNDSCOMPACTERRORMESSAGES))
{
string = cstring_replaceChar(string, '\n', ' ');
}
/*drl added 12/19/2002 print
a different error fro "likely" bounds-errors*/
- isLikely = constraint_isConstantOnly(c);
+ isLikely = constraint_isConstantOnly (c);
if (isLikely)
{
else
{
st = cstring_concatFree (st, message ("derived from: %q",
- constraint_unparseDeep (c->orig)));
+ constraint_unparseDeep (c->orig)));
}
}
return st;
}
-/*@only@*/ cstring constraint_unparse (constraint c) /*@*/
+/*@only@*/ cstring constraint_unparse (constraint c) /*@*/
{
cstring st = cstring_undefined;
cstring type = cstring_undefined;
doFixResultTerm (/*@only@*/ constraintExpr p_e, /*@exposed@*/ exprNode p_fcnCall)
/*@modifies p_e@*/;
-static bool constraintExpr_canGetCType (constraintExpr p_e) /*@*/;
+static bool constraintExpr_canGetCType (constraintExpr p_e) /*@*/;
static ctype constraintExpr_getCType (constraintExpr p_e);
-static /*@only@*/ constraintExpr constraintExpr_adjustMaxSetForCast(/*@only@*/ constraintExpr p_e, ctype p_ct);
+static /*@only@*/ constraintExpr constraintExpr_adjustMaxSetForCast (/*@only@*/ constraintExpr p_e,
+ ctype p_tfrom, ctype p_tto,
+ fileloc loc);
/*@special@*/ /*@notnull@*/ static constraintExpr constraintExpr_makeBinaryOp (void)
/* @allocates result->data @ @sets result->kind @ */ ;
constraintExpr ret;
ret = constraintExpr_alloc();
ret->kind = unaryExpr;
- ret->data = dmalloc ( sizeof *(ret->data) );
+ ret->data = dmalloc (sizeof *(ret->data));
ret->data->unaryOp.expr = constraintExpr_undefined;
return ret;
}
}
-/*@only@*/ /*@notnull@*/static constraintExpr constraintExpr_makeUnaryOp (/*@only@*/ constraintExpr cexpr, constraintExprUnaryOpKind Op )
+/*@only@*/ /*@notnull@*/ static constraintExpr
+constraintExpr_makeUnaryOp (/*@only@*/ constraintExpr cexpr, constraintExprUnaryOpKind Op)
{
constraintExpr ret;
ret = makeUnaryOpGeneric();
}
-/*@only@*/ constraintExpr constraintExpr_searchandreplace (/*@only@*/ /*@unique@*/ constraintExpr c, /*@temp@*/ constraintExpr old, /*@temp@*/ constraintExpr newExpr )
+/*@only@*/ constraintExpr
+constraintExpr_searchandreplace (/*@only@*/ /*@unique@*/ constraintExpr c, /*@temp@*/ constraintExpr old,
+ /*@temp@*/ constraintExpr newExpr )
{
constraintExprKind kind;
constraintExpr temp;
constraintExpr ret;
- llassert(constraintExpr_isDefined (newExpr) && (constraintExpr_isDefined (old) && constraintExpr_isDefined(c) ) );
+ llassert (constraintExpr_isDefined (newExpr) && (constraintExpr_isDefined (old) && constraintExpr_isDefined(c) ) );
- if ( constraintExpr_similar (c, old) )
+ if (constraintExpr_similar (c, old))
{
-
- ctype newType, cType;
-
-
-
+ ctype newType = ctype_unknown;
+ ctype cType = ctype_unknown;
ret = constraintExpr_copy (newExpr);
llassert(constraintExpr_isDefined(ret) );
/*drl if newExpr != NULL then ret will != NULL*/
- DPRINTF((message ("Replacing %s with %s",
- constraintExpr_unparse(old), constraintExpr_unparse(newExpr)
- )));
+ DPRINTF (("Replacing %s with %s in %s",
+ constraintExpr_unparse (old), constraintExpr_unparse (newExpr),
+ constraintExpr_unparse (c)));
- if (constraintExpr_canGetCType(c) && constraintExpr_canGetCType(newExpr) )
+ if (constraintExpr_canGetCType (c) && constraintExpr_canGetCType (newExpr))
{
cType = constraintExpr_getCType(c);
- newType = constraintExpr_getCType(newExpr);
+ newType = constraintExpr_getCType (newExpr);
- if (ctype_match(cType,newType) )
+ if (ctype_match (cType,newType))
{
- DPRINTF(( message("constraintExpr_searchandreplace: replacing "
- " %s with type %s with %s with type %s",
- constraintExpr_print(c), ctype_unparse(cType),
- constraintExpr_print(newExpr), ctype_unparse(newType)
- )
- ));
+ DPRINTF (("constraintExpr_searchandreplace: replacing "
+ " %s with type %s with %s with type %s",
+ constraintExpr_unparse (c), ctype_unparse(cType),
+ constraintExpr_unparse (newExpr), ctype_unparse(newType)));
ret->ct = TRUE;
ret->origType = cType;
+ DPRINTF (("Type: %s", ctype_unparse (constraintExpr_getCType (ret))));
}
}
-
- if (constraintExpr_hasMaxSet(c) )
+
+ if (constraintExpr_hasMaxSet (c))
{
- if (constraintExpr_hasTypeChange(c))
- {
- DPRINTF(( message("constraintExpr_searchandreplace: encountered "
- "MaxSet with changed type %s ",
- constraintExpr_print(c) )
- ));
-
- /*fix this with a conversation */
- ret = constraintExpr_adjustMaxSetForCast(ret, constraintExpr_getOrigType(c));
- }
+ if (constraintExpr_hasTypeChange (c))
+ {
+ fileloc loc = constraintExpr_loc (c);
+ DPRINTF (("constraintExpr_searchandreplace: encountered "
+ "MaxSet with changed type %s ",
+ constraintExpr_unparse (c)));
+
+ if (c->kind == unaryExpr)
+ {
+ constraintExpr ce = constraintExprData_unaryExprGetExpr (c->data);
+ DPRINTF (("Its a unary! %s / %s",
+ ctype_unparse (constraintExpr_getCType (ce)),
+ ctype_unparse (constraintExpr_getOrigType (ce))));
+ ret = constraintExpr_adjustMaxSetForCast (ret, constraintExpr_getCType (ce),
+ constraintExpr_getOrigType (ce),
+ loc);
+ }
+ else
+ {
+ /* fix this with a conversation */
+ DPRINTF (("Types: %s / %s", ctype_unparse (newType), ctype_unparse (cType)));
+ ret = constraintExpr_adjustMaxSetForCast (ret, constraintExpr_getCType (c),
+ constraintExpr_getOrigType(c),
+ loc);
+ }
+ }
}
- constraintExpr_free(c);
-
+
+ constraintExpr_free (c);
+ DPRINTF (("ret: %s", constraintExpr_unparse (ret)));
return ret;
}
case term:
break;
case unaryExpr:
+ DPRINTF (("Making unary expression!"));
temp = constraintExprData_unaryExprGetExpr (c->data);
- temp = constraintExpr_copy(temp);
+ temp = constraintExpr_copy (temp);
temp = constraintExpr_searchandreplace (temp, old, newExpr);
c->data = constraintExprData_unaryExprSetExpr (c->data, temp);
break;
case binaryexpr:
-
+ DPRINTF (("Making binary expression!"));
temp = constraintExprData_binaryExprGetExpr1 (c->data);
- temp = constraintExpr_copy(temp);
+ temp = constraintExpr_copy (temp);
temp = constraintExpr_searchandreplace (temp, old, newExpr);
c->data = constraintExprData_binaryExprSetExpr1 (c->data, temp);
temp = constraintExprData_binaryExprGetExpr2 (c->data);
- temp = constraintExpr_copy(temp);
+ temp = constraintExpr_copy (temp);
temp = constraintExpr_searchandreplace (temp, old, newExpr);
c->data = constraintExprData_binaryExprSetExpr2 (c->data, temp);
break;
default:
- llassert(FALSE);
+ llassert (FALSE);
}
+
+ DPRINTF (("ret: %s", constraintExpr_unparse (c)));
return c;
}
}
/*@only@*/
-cstring constraintExpr_unparse (/*@temp@*/ /*@observer@*/ constraintExpr ex) /*@*/
+cstring constraintExpr_unparse (/*@temp@*/ constraintExpr ex) /*@*/
{
cstring st;
constraintExprKind kind;
switch (kind)
{
case term:
-
- if (context_getFlag (FLG_PARENCONSTRAINT) )
- {
- st = message ("(%q) ", constraintTerm_unparse (constraintExprData_termGetTerm (ex->data)));
- }
- else
- {
- st = message ("%q", constraintTerm_unparse (constraintExprData_termGetTerm (ex->data)));
- }
+ if (context_getFlag (FLG_PARENCONSTRAINT) )
+ {
+ st = message ("(%q) ", constraintTerm_unparse (constraintExprData_termGetTerm (ex->data)));
+ }
+ else
+ {
+ st = message ("%q", constraintTerm_unparse (constraintExprData_termGetTerm (ex->data)));
+ }
break;
case unaryExpr:
st = message ("%q(%q)",
if (context_getFlag (FLG_PARENCONSTRAINT) )
{
st = message ("(%q) %q (%q)",
- constraintExpr_unparse (constraintExprData_binaryExprGetExpr1 (ex->data) ),
- constraintExprBinaryOpKind_print (constraintExprData_binaryExprGetOp (ex->data)
- ),
- constraintExpr_unparse (constraintExprData_binaryExprGetExpr2 (ex->data) )
- );
+ constraintExpr_unparse (constraintExprData_binaryExprGetExpr1 (ex->data) ),
+ constraintExprBinaryOpKind_print (constraintExprData_binaryExprGetOp (ex->data)),
+ constraintExpr_unparse (constraintExprData_binaryExprGetExpr2 (ex->data) )
+ );
}
else
{
st = message ("%q %q %q",
- constraintExpr_unparse (constraintExprData_binaryExprGetExpr1 (ex->data) ),
- constraintExprBinaryOpKind_print (constraintExprData_binaryExprGetOp (ex->data)
- ),
- constraintExpr_unparse (constraintExprData_binaryExprGetExpr2 (ex->data) )
+ constraintExpr_unparse (constraintExprData_binaryExprGetExpr1 (ex->data)),
+ constraintExprBinaryOpKind_print (constraintExprData_binaryExprGetOp (ex->data)),
+ constraintExpr_unparse (constraintExprData_binaryExprGetExpr2 (ex->data))
);
}
BADEXIT;
}
-fileloc constraintExpr_getFileloc (constraintExpr expr)
+fileloc constraintExpr_loc (constraintExpr expr)
{
constraintExpr e;
constraintTerm t;
break;
case unaryExpr:
e = constraintExprData_unaryExprGetExpr (expr->data);
- return (constraintExpr_getFileloc (e) );
+ return (constraintExpr_loc (e) );
/*@notreached@*/
break;
case binaryexpr:
e = constraintExprData_binaryExprGetExpr1 (expr->data);
- return (constraintExpr_getFileloc (e) );
+ return (constraintExpr_loc (e) );
/*@notreached@*/
break;
}
}
-bool constraintExpr_canGetCType (constraintExpr e) /*@*/
+bool constraintExpr_canGetCType (constraintExpr e) /*@*/
{
- if (constraintExpr_isUndefined(e) )
+ if (constraintExpr_isUndefined(e))
return FALSE;
if (e->kind == term)
}
else
{
- DPRINTF(( message("constraintExpr_canGetCType: can't get type for %s ",
- constraintExpr_print(e) ) ));
+ DPRINTF (("constraintExpr_canGetCType: can't get type for %s", constraintExpr_unparse (e)));
return FALSE;
}
}
{
constraintTerm t;
- llassert(constraintExpr_isDefined(e) );
-
- llassert(constraintExpr_canGetCType(e) );
+ llassert (constraintExpr_isDefined (e));
+ llassert (constraintExpr_canGetCType (e));
switch (e->kind)
{
return (constraintTerm_getCType(t) );
/* assume that a unary expression will be an int ... */
case unaryExpr:
- return ctype_signedintegral;
-
+ return ctype_unknown; /* was ctype_signedintegral; */
/* drl for just return type of first operand */
case binaryexpr:
- return (
- constraintExpr_getCType
- (constraintExprData_binaryExprGetExpr1 (e->data) )
- );
+ return (constraintExpr_getCType (constraintExprData_binaryExprGetExpr1 (e->data)));
default:
BADEXIT;
}
/* drl add 10-5-001 */
-static bool constraintExpr_hasTypeChange(constraintExpr e)
+static bool constraintExpr_hasTypeChange (constraintExpr e)
{
- llassert(constraintExpr_isDefined(e) );
- if (constraintExpr_isDefined((e)) && (e->ct == TRUE) )
+ llassert(constraintExpr_isDefined(e));
+
+ if (constraintExpr_isDefined((e)) && (e->ct == TRUE))
{
return TRUE;
}
{
if (constraintExprData_unaryExprGetOp (e->data) == MAXSET)
{
- constraintExpr ce;
-
- ce = constraintExprData_unaryExprGetExpr(e->data);
-
- return (constraintExpr_hasTypeChange(ce) );
+ constraintExpr ce = constraintExprData_unaryExprGetExpr(e->data);
+ DPRINTF (("Unary type change: [%x] %s", ce, constraintExpr_unparse (ce)));
+ DPRINTF (("Types: %s / %s", ctype_unparse (constraintExpr_getCType (ce)),
+ ctype_unparse (constraintExpr_getOrigType (ce))));
+ return (constraintExpr_hasTypeChange(ce));
}
-
}
+
return FALSE;
}
static ctype constraintExpr_getOrigType (constraintExpr e)
{
-
- llassert(constraintExpr_isDefined(e) );
- llassert(constraintExpr_hasTypeChange(e) );
-
+ llassert (constraintExpr_isDefined (e));
+ llassert (constraintExpr_hasTypeChange (e));
if (e->ct == TRUE)
{
{
if (constraintExprData_unaryExprGetOp (e->data) == MAXSET)
{
- constraintExpr ce;
-
- ce = constraintExprData_unaryExprGetExpr(e->data);
-
- return (constraintExpr_getOrigType(ce) );
+ constraintExpr ce = constraintExprData_unaryExprGetExpr (e->data);
+ return (constraintExpr_getOrigType(ce));
}
}
/*drl added these around 10/18/001*/
-static /*@only@*/ constraintExpr constraintExpr_div (/*@only@*/ constraintExpr e, /*@unused@*/ ctype ct)
+static /*@only@*/ constraintExpr constraintExpr_div (/*@only@*/ constraintExpr e, ctype tfrom, ctype tto, fileloc loc)
{
+ int sizefrom = ctype_getSize (tfrom);
+ int sizeto = ctype_getSize (tto);
+
+ DPRINTF (("constraintExpr_div: %s", constraintExpr_unparse (e)));
+ DPRINTF (("Types: %s / %s",
+ ctype_unparse (tfrom),
+ ctype_unparse (tto)));
+
+ if (sizefrom == -1) {
+ llbug (message ("constraintExpr_div: type size unknown: %s", ctype_unparse (tfrom)));
+ }
+
+ if (sizeto == -1) {
+ llbug (message ("constraintExpr_div: type size unknown: %s", ctype_unparse (tto)));
+ }
+
+ if (sizeto == sizefrom)
+ {
+ ; /* Sizes match, a-ok */
+ }
+ else
+ {
+ float scale = (float) sizefrom / (float) sizeto;
+ constraintTerm ct;
+ long val;
+ float fnewval;
+ long newval;
+
+ llassert (e->kind == term);
+ ct = constraintExprData_termGetTerm (e->data);
+ llassert (constraintTerm_canGetValue (ct));
+ val = constraintTerm_getValue (ct);
+
+ DPRINTF (("Scaling constraints by: %ld * %f", val, scale));
+
+ // If scale * val is not an integer, give a warning
+ fnewval = val * scale;
+ newval = (long) fnewval;
+
+ DPRINTF (("Values: %f / %ld", fnewval, newval));
+ if ((fnewval - (float) newval) > FLT_EPSILON)
+ {
+ voptgenerror (FLG_ALLOCMISMATCH,
+ message ("Allocated memory is converted to type %s of (size %d), "
+ "which is not divisible into original allocation of space for %d elements of type %s (size %d)",
+ ctype_unparse (tto), sizeto,
+ val, ctype_unparse (tfrom), sizefrom),
+ loc);
+ }
+
+ constraintTerm_setValue (ct, newval);
+ }
+
+ DPRINTF (("After div: %s", constraintExpr_unparse (e)));
return e;
}
/*@access exprNode@*/
-static /*@only@*/ constraintExpr constraintTerm_simpleDivTypeExprNode(/*@only@*/ constraintExpr e, ctype ct)
+static /*@only@*/ constraintExpr constraintTerm_simpleDivTypeExprNode (/*@only@*/ constraintExpr e, ctype tfrom, ctype tto, fileloc loc)
{
exprData data;
exprNode t1, t2, expr;
lltok tok;
constraintTerm t;
- llassert(constraintExpr_isDefined(e) );
+ llassert (constraintExpr_isDefined(e) );
- DPRINTF((
- message("constraintTerm_simpleDivTypeExprNode e=%s, ct=%s",
- constraintExpr_print(e), ctype_unparse(ct)
- )
- ));
+ DPRINTF (("constraintTerm_simpleDivTypeExprNode e=%s [%s => %s]", constraintExpr_print(e),
+ ctype_unparse(tfrom), ctype_unparse (tto)));
- t = constraintExprData_termGetTerm(e->data);
+ t = constraintExprData_termGetTerm (e->data);
- expr = constraintTerm_getExprNode(t);
+ expr = constraintTerm_getExprNode (t);
- llassert(constraintExpr_isDefined(e) );
- llassert(exprNode_isDefined(expr) );
+ llassert (constraintExpr_isDefined(e));
+ llassert (exprNode_isDefined(expr));
if (expr->kind == XPR_OP)
{
t1 = exprData_getOpA (data);
t2 = exprData_getOpB (data);
tok = exprData_getOpTok (data);
- if (lltok_isMult(tok) )
+
+ if (lltok_isMult (tok))
{
- llassert(exprNode_isDefined(t1) && exprNode_isDefined(t2) );
+ llassert (exprNode_isDefined(t1) && exprNode_isDefined(t2) );
/*drl 3/2/2003 we know this from the fact that it's a
multiplication operation...*/
- if ((t1->kind == XPR_SIZEOF) || (t1->kind == XPR_SIZEOFT) )
+ if ((t1->kind == XPR_SIZEOF) || (t1->kind == XPR_SIZEOFT))
{
ctype ct2;
}
else
{
- exprNode tempE;
-
- tempE = exprData_getSingle (t1->edata);
-
- ct2 = exprNode_getType (tempE);
+ exprNode tempE = exprData_getSingle (t1->edata);
+ ct2 = exprNode_getType (tempE);
}
- if (ctype_match (ctype_makePointer(ct2), ct) )
+
+ if (ctype_match (ctype_makePointer(ct2), tfrom)) //!
{
/* this is a bit sloopy but ... */
- constraintExpr_free(e);
- return constraintExpr_makeExprNode(t2);
+ constraintExpr_free(e);
+ return constraintExpr_makeExprNode (t2);
+ }
+ else
+ {
+ /* nothing was here */
+ DPRINTF (("MISMATCHING TYPES!"));
}
}
-
-
- else if ((t2->kind == XPR_SIZEOF) || (t2->kind == XPR_SIZEOFT) )
+ else if ((t2->kind == XPR_SIZEOF) || (t2->kind == XPR_SIZEOFT))
{
ctype ct2;
exprTemp = exprData_getSingle (t2->edata);
- llassert(exprNode_isDefined(exprTemp) );
+ llassert (exprNode_isDefined (exprTemp));
eDTemp = exprTemp->edata;
- ct2 = qtype_getType (exprData_getType(eDTemp ) );
+ ct2 = qtype_getType (exprData_getType(eDTemp ));
}
- if (ctype_match (ctype_makePointer(ct2),ct) )
+
+ if (ctype_match (ctype_makePointer (ct2), tfrom))
{
/*a bit of a sloopy way to do this but... */
- constraintExpr_free(e);
- return constraintExpr_makeExprNode(t1);
+ constraintExpr_free(e);
+ return constraintExpr_makeExprNode (t1);
}
}
else
{
+ DPRINTF (("NOT A SIZEOF!"));
/*empty*/
}
}
}
- return (constraintExpr_div (e, ct) );
+
+ return (constraintExpr_div (e, tfrom, tto, loc));
}
/*@noaccess exprNode@*/
-static /*@only@*/ constraintExpr simpleDivType (/*@only@*/ constraintExpr e, ctype ct)
+static /*@only@*/ constraintExpr simpleDivType (/*@only@*/ constraintExpr e, ctype tfrom, ctype tto, fileloc loc)
{
- DPRINTF(( (message("simpleDiv got %s ", constraintExpr_unparse(e) ) )
- ));
+ DPRINTF (("simpleDiv got %s", constraintExpr_unparse(e)));
+ DPRINTF (("Types: %s / %s",
+ ctype_unparse (tfrom),
+ ctype_unparse (tto)));
- llassert(constraintExpr_isDefined(e) );
+ llassert (constraintExpr_isDefined(e));
switch (e->kind)
{
case term:
-
{
- constraintTerm t;
+ constraintTerm t = constraintExprData_termGetTerm (e->data);
- t = constraintExprData_termGetTerm(e->data);
-
+ DPRINTF (("Term: %s", constraintTerm_unparse (t)));
- if (constraintTerm_isExprNode (t) )
- {
- return constraintTerm_simpleDivTypeExprNode(e, ct);
-
- /* search for * size of ct and remove */
- }
- return constraintExpr_div (e, ct);
+ if (constraintTerm_isExprNode (t))
+ {
+ return constraintTerm_simpleDivTypeExprNode (e, tfrom, tto, loc);
+
+ /* search for * size of ct and remove */
+ }
+ DPRINTF (("Here: %s / %s -> %s", constraintExpr_unparse (e), ctype_unparse (tfrom), ctype_unparse (tto)));
+ return constraintExpr_div (e, tfrom, tto, loc);
}
case binaryexpr:
temp = constraintExprData_binaryExprGetExpr1 (e->data);
temp = constraintExpr_copy(temp);
- temp = simpleDivType (temp, ct);
+ temp = simpleDivType (temp, tfrom, tto, loc);
e->data = constraintExprData_binaryExprSetExpr1 (e->data, temp);
temp = constraintExprData_binaryExprGetExpr2 (e->data);
temp = constraintExpr_copy(temp);
- temp = simpleDivType (temp, ct);
+ temp = simpleDivType (temp, tfrom, tto, loc);
e->data = constraintExprData_binaryExprSetExpr2 (e->data, temp);
- DPRINTF(( (message("simpleDiv binaryexpr returning %s ", constraintExpr_unparse(e) ) )
- ));
-
+ DPRINTF (("simpleDiv binaryexpr returning %s ", constraintExpr_unparse(e)));
return e;
}
case unaryExpr:
- return constraintExpr_div (e, ct);
+ {
+ return constraintExpr_div (e, tfrom, tto, loc);
+ }
default:
BADEXIT;
}
}
-static /*@only@*/ constraintExpr constraintExpr_adjustMaxSetForCast(/*@only@*/ constraintExpr e, ctype ct)
+static /*@only@*/ constraintExpr constraintExpr_adjustMaxSetForCast (/*@only@*/ constraintExpr e, ctype tfrom,
+ ctype tto, fileloc loc)
{
-
- DPRINTF(( (message("constraintExpr_adjustMaxSetForCast got %s ", constraintExpr_unparse(e) ) )
- ));
-
- e = constraintExpr_makeIncConstraintExpr(e);
-
- e = constraintExpr_simplify(e);
-
-
- e = simpleDivType (e, ct);
-
- e = constraintExpr_makeDecConstraintExpr(e);
+ DPRINTF (("constraintExpr_adjustMaxSetForCast got %s [%s => %s]", constraintExpr_unparse(e),
+ ctype_unparse (tfrom), ctype_unparse (tto)));
- e = constraintExpr_simplify(e);
+ e = constraintExpr_makeIncConstraintExpr (e);
+ e = constraintExpr_simplify (e);
+ e = simpleDivType (e, tfrom, tto, loc);
+ e = constraintExpr_makeDecConstraintExpr (e);
+ e = constraintExpr_simplify (e);
- DPRINTF(( (message("constraintExpr_adjustMaxSetForCast returning %s ", constraintExpr_unparse(e) ) )
- ));
-
+ DPRINTF (("constraintExpr_adjustMaxSetForCast returning %s ", constraintExpr_unparse(e)));
return e;
}
-bool constraintExpr_isConstantOnly ( constraintExpr e )
+bool constraintExpr_isConstantOnly (constraintExpr e)
{
- DPRINTF(( (message("constraintExpr_isConstantOnly %s ",
- constraintExpr_unparse(e) ) )
- ));
-
- llassert(constraintExpr_isDefined(e) );
+ DPRINTF (("constraintExpr_isConstantOnly %s ", constraintExpr_unparse(e)));
+ llassert (constraintExpr_isDefined(e));
switch (e->kind)
{
case term:
{
- constraintTerm t;
-
- t = constraintExprData_termGetTerm(e->data);
+ constraintTerm t = constraintExprData_termGetTerm(e->data);
-
- if (constraintTerm_isConstantOnly (t) )
+ if (constraintTerm_isConstantOnly (t))
{
return TRUE;
}
case binaryexpr:
{
- constraintExpr temp1, temp2;
-
- temp1 = constraintExprData_binaryExprGetExpr1 (e->data);
-
- temp2 = constraintExprData_binaryExprGetExpr2 (e->data);
+ constraintExpr temp1 = constraintExprData_binaryExprGetExpr1 (e->data);
+ constraintExpr temp2 = constraintExprData_binaryExprGetExpr2 (e->data);
if (constraintExpr_isConstantOnly(temp1) &&
constraintExpr_isConstantOnly(temp2) )
static void exprNode_stmt (/*@temp@*/ /*@temp@*/ exprNode p_e);
static void exprNode_multiStatement (/*@temp@*/ exprNode p_e);
-static constraintList exprNode_traversTrueEnsuresConstraints (/*@temp@*/ exprNode p_e);
-static constraintList exprNode_traversFalseEnsuresConstraints (/*@temp@*/ exprNode p_e);
+static constraintList exprNode_traverseTrueEnsuresConstraints (/*@temp@*/ exprNode p_e);
+static constraintList exprNode_traverseFalseEnsuresConstraints (/*@temp@*/ exprNode p_e);
static void checkArgumentList (/*@out@*/ exprNode p_temp, exprNodeList p_arglist, fileloc p_sequencePoint) /*@modifies p_temp @*/;
return FALSE;
}
- DPRINTF((message ("exprNode_generateConstraints Analysising %s at %s", exprNode_unparse(e),
- fileloc_unparse(exprNode_getfileloc(e)))));
-
+ DPRINTF ((message ("exprNode_generateConstraints Analyzing %s at %s", exprNode_unparse(e),
+ fileloc_unparse(exprNode_loc (e)))));
+
if (exprNode_isMultiStatement (e))
{
exprNode_multiStatement(e);
}
else
{
-/* fileloc loc; */
+ /* fileloc loc; */
-/* loc = exprNode_getNextSequencePoint(e); */
-/* exprNode_exprTraverse(e, FALSE, FALSE, loc); */
+ /* loc = exprNode_getNextSequencePoint(e); */
+ /* exprNode_exprTraverse(e, FALSE, FALSE, loc); */
+
+ /* fileloc_free(loc); */
-/* fileloc_free(loc); */
-
exprNode_stmt(e);
return FALSE;
{
constraintList c;
-
+
c = constraintList_makeFixedArrayConstraints (e->uses);
e->requiresConstraints = constraintList_reflectChangesFreePre (e->requiresConstraints, c);
constraintList_free(c);
}
-
- DPRINTF ((message ("e->requiresConstraints %s", constraintList_unparseDetailed (e->requiresConstraints))));
+
+ DPRINTF ((message ("e->requiresConstraints %s",
+ constraintList_unparseDetailed (e->requiresConstraints))));
return FALSE;
}
{
exprNode snode;
fileloc loc;
- cstring s;
+ //! cstring s;
+ DPRINTF (("Generating constraint for: %s", exprNode_unparse (e)));
+
if (exprNode_isError(e))
{
return;
/*e->requiresConstraints = constraintList_makeNew();
e->ensuresConstraints = constraintList_makeNew(); */
-
- DPRINTF(("expNode_stmt: STMT:"));
- s = exprNode_unparse(e);
- DPRINTF ((message("exprNode_stmt: STMT: %s ", s)));
+
+ /*!! s = exprNode_unparse (e); */
if (e->kind == XPR_INIT)
{
constraintList tempList;
- DPRINTF (("Init"));
- DPRINTF ((message ("%s ", exprNode_unparse (e))));
- loc = exprNode_getNextSequencePoint(e); /* reduces to an expression */
+ DPRINTF (("Init: %s ", exprNode_unparse (e)));
+ loc = exprNode_getNextSequencePoint (e); /* reduces to an expression */
+ DPRINTF (("Location: %s", fileloc_unparse (loc)));
+ DPRINTF (("Ensures before: %s", constraintList_unparse (e->ensuresConstraints)));
exprNode_exprTraverse (e, FALSE, FALSE, loc);
+ DPRINTF (("Ensures after: %s", constraintList_unparse (e->ensuresConstraints)));
+ DPRINTF (("After traversing..."));
fileloc_free(loc);
-
+
tempList = e->requiresConstraints;
- e->requiresConstraints = exprNode_traversRequiresConstraints(e);
+ DPRINTF (("Requires before: %s", constraintList_unparse (e->requiresConstraints)));
+ e->requiresConstraints = exprNode_traverseRequiresConstraints (e);
+ DPRINTF (("Requires after: %s", constraintList_unparse (e->requiresConstraints)));
constraintList_free(tempList);
tempList = e->ensuresConstraints;
- e->ensuresConstraints = exprNode_traversEnsuresConstraints(e);
+ DPRINTF (("Ensures before: %s", constraintList_unparse (e->ensuresConstraints)));
+ e->ensuresConstraints = exprNode_traverseEnsuresConstraints(e);
+ DPRINTF (("Ensures before: %s", constraintList_unparse (e->ensuresConstraints)));
constraintList_free(tempList);
return;
}
fileloc_free(loc);
tempList = e->requiresConstraints;
- e->requiresConstraints = exprNode_traversRequiresConstraints(e);
+ e->requiresConstraints = exprNode_traverseRequiresConstraints(e);
constraintList_free(tempList);
}
if (e->kind != XPR_STMT)
{
-
DPRINTF (("Not Stmt"));
DPRINTF ((message ("%s ", exprNode_unparse (e))));
fileloc_free(loc);
constraintList_free (e->requiresConstraints);
- e->requiresConstraints = exprNode_traversRequiresConstraints(snode);
+ e->requiresConstraints = exprNode_traverseRequiresConstraints(snode);
constraintList_free (e->ensuresConstraints);
- e->ensuresConstraints = exprNode_traversEnsuresConstraints(snode);
-
+ e->ensuresConstraints = exprNode_traverseEnsuresConstraints(snode);
+
DPRINTF ((message ("smtlist constraints are: pre: %s \n and \t post %s\n",
constraintList_unparse(e->requiresConstraints),
constraintList_unparse(e->ensuresConstraints))));
DPRINTF ((message ("doIf: %s ", exprNode_unparse(e))));
- llassert(exprNode_isDefined(test));
+ llassert (exprNode_isDefined(test));
llassert (exprNode_isDefined (e));
llassert (exprNode_isDefined (body));
-
- DPRINTF((message ("ensures constraints for %s are %s", exprNode_unparse(e), constraintList_unparseDetailed(e->ensuresConstraints))));
+ DPRINTF((message ("ensures constraints for %s are %s", exprNode_unparse(e), constraintList_unparseDetailed(e->ensuresConstraints))));
DPRINTF((message ("Requires constraints for %s are %s", exprNode_unparse(e), constraintList_unparseDetailed(e->ensuresConstraints))));
temp = test->trueEnsuresConstraints;
- test->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(test);
+ test->trueEnsuresConstraints = exprNode_traverseTrueEnsuresConstraints(test);
constraintList_free(temp);
temp = test->ensuresConstraints;
- test->ensuresConstraints = exprNode_traversEnsuresConstraints (test);
+ test->ensuresConstraints = exprNode_traverseEnsuresConstraints (test);
constraintList_free(temp);
temp = test->requiresConstraints;
- test->requiresConstraints = exprNode_traversRequiresConstraints (test);
+ test->requiresConstraints = exprNode_traverseRequiresConstraints (test);
constraintList_free(temp);
Precondition
This function assumes that p, trueBranch, falseBranch have have all been traversed
- for constraints i.e. we assume that exprNode_traversEnsuresConstraints,
- exprNode_traversRequiresConstraints, exprNode_traversTrueEnsuresConstraints,
- exprNode_traversFalseEnsuresConstraints have all been run
+ for constraints i.e. we assume that exprNode_traverseEnsuresConstraints,
+ exprNode_traverseRequiresConstraints, exprNode_traverseTrueEnsuresConstraints,
+ exprNode_traverseFalseEnsuresConstraints have all been run
*/
static exprNode doIfElse (/*@returned@*/ exprNode e, /*@dependent@*/ exprNode p, /*@dependent@*/ exprNode trueBranch, /*@dependent@*/ exprNode falseBranch)
{
constraintList temp2;
temp2 = test->trueEnsuresConstraints;
- test->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(test);
+ test->trueEnsuresConstraints = exprNode_traverseTrueEnsuresConstraints(test);
constraintList_free(temp2);
}
llassert (exprNode_isDefined (p));
temp = p->ensuresConstraints;
- p->ensuresConstraints = exprNode_traversEnsuresConstraints (p);
+ p->ensuresConstraints = exprNode_traverseEnsuresConstraints (p);
constraintList_free(temp);
temp = p->requiresConstraints;
- p->requiresConstraints = exprNode_traversRequiresConstraints (p);
+ p->requiresConstraints = exprNode_traverseRequiresConstraints (p);
constraintList_free(temp);
temp = p->trueEnsuresConstraints;
- p->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(p);
+ p->trueEnsuresConstraints = exprNode_traverseTrueEnsuresConstraints(p);
constraintList_free(temp);
));
temp = p->falseEnsuresConstraints;
- p->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(p);
+ p->falseEnsuresConstraints = exprNode_traverseFalseEnsuresConstraints(p);
constraintList_free(temp);
/*See comment on trueEnsures*/
}
}
-void exprNode_exprTraverse (/*@dependent@*/ exprNode e, bool definatelv, bool definaterv, /*@observer@*/ /*@temp@*/ fileloc sequencePoint)
+void exprNode_exprTraverse (/*@dependent@*/ exprNode e,
+ bool definatelv, bool definaterv,
+ /*@observer@*/ /*@temp@*/ fileloc sequencePoint)
{
exprNode t1, t2, fcn;
lltok tok;
- bool handledExprNode;
exprData data;
constraint cons;
-
constraintList temp;
if (exprNode_isError(e))
return;
}
- DPRINTF((message ("exprNode_exprTraverset Analysising %s %s at", exprNode_unparse(e),
- fileloc_unparse(exprNode_getfileloc(e)))));
+ DPRINTF (("exprNode_exprTraverse analyzing %s at %s",
+ exprNode_unparse (e),
+ fileloc_unparse (exprNode_loc (e))));
- /*e->requiresConstraints = constraintList_makeNew();
- e->ensuresConstraints = constraintList_makeNew();
- e->trueEnsuresConstraints = constraintList_makeNew();;
- e->falseEnsuresConstraints = constraintList_makeNew();;
- */
-
if (exprNode_isUnhandled (e))
- {
- return;
- }
-
- handledExprNode = TRUE;
+ {
+ return;
+ }
data = e->edata;
break;
case XPR_INIT:
{
- /*
- idDecl t;
-
- uentry ue;
- exprNode lhs;
-
- t = exprData_getInitId (data);
- ue = usymtab_lookup (idDecl_observeId (t));
- lhs = exprNode_createId (ue);
- */
t2 = exprData_getInitNode (data);
-
- /* DPRINTF(((message("initialization: %s = %s",
- exprNode_unparse(lhs),
- exprNode_unparse(t2)
- )
- ))); */
+
+ DPRINTF (("initialization ==> %s",exprNode_unparse (t2)));
exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint);
- /* this test is nessecary because some expressions generate a null expression node. function pointer do that -- drl */
- if ((!exprNode_isError (e)) && (!exprNode_isError(t2)))
+ /* This test is nessecary because some expressions generate a null expression node.
+ function pointer do that -- drl */
+
+ if (!exprNode_isError (e) && !exprNode_isError (t2))
{
cons = constraint_makeEnsureEqual (e, t2, sequencePoint);
e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
case XPR_ASSIGN:
t1 = exprData_getOpA (data);
t2 = exprData_getOpB (data);
+ DPRINTF (("Assignment constraints t1: %s", constraintList_unparse (t1->ensuresConstraints)));
+ DPRINTF (("Assignment constraints t2: %s", constraintList_unparse (t2->ensuresConstraints)));
exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint);
+ DPRINTF (("Assignment constraints t1: %s", constraintList_unparse (t1->ensuresConstraints)));
+ DPRINTF (("Assignment constraints t2: %s", constraintList_unparse (t2->ensuresConstraints)));
exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint);
+ DPRINTF (("Assignment constraints t1: %s", constraintList_unparse (t1->ensuresConstraints)));
+ DPRINTF (("Assignment constraints t2: %s", constraintList_unparse (t2->ensuresConstraints)));
- /* this test is nessecary because some expressions generate a null expression node. function pointer do that -- drl */
- if ((!exprNode_isError (t1)) && (!exprNode_isError(t2)))
+ /* this test is nessecary because some expressions generate a null expression node.
+ function pointer do that -- drl */
+
+ if ((!exprNode_isError (t1)) && (!exprNode_isError(t2)))
{
- cons = constraint_makeEnsureEqual (t1, t2, sequencePoint);
- e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
+ cons = constraint_makeEnsureEqual (t1, t2, sequencePoint);
+ DPRINTF (("Ensure equal constraint: %s", constraint_unparse (cons)));
+ e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
+ DPRINTF (("Assignment constraints: %s", constraintList_unparse (e->ensuresConstraints)));
}
break;
case XPR_OP:
fcn = exprData_getFcn(data);
exprNode_exprTraverse (fcn, definatelv, definaterv, sequencePoint);
- DPRINTF ((message ("Got call that %s (%s) ", exprNode_unparse(fcn), exprNodeList_unparse (exprData_getArgs (data)))));
+ DPRINTF (("Got call that %s (%s)",
+ exprNode_unparse(fcn), exprNodeList_unparse (exprData_getArgs (data))));
llassert( exprNode_isDefined(fcn) );
-
- fcn->requiresConstraints = constraintList_addListFree (fcn->requiresConstraints,
- checkCall (fcn, exprData_getArgs (data) ));
-
- fcn->ensuresConstraints = constraintList_addListFree (fcn->ensuresConstraints,
- exprNode_getPostConditions(fcn, exprData_getArgs (data),e ));
-
+
+ fcn->requiresConstraints =
+ constraintList_addListFree (fcn->requiresConstraints,
+ checkCall (fcn, exprData_getArgs (data) ));
+
+ fcn->ensuresConstraints =
+ constraintList_addListFree (fcn->ensuresConstraints,
+ exprNode_getPostConditions(fcn, exprData_getArgs (data),e ));
+
t1 = exprNode_createNew (exprNode_getType (e));
checkArgumentList (t1, exprData_getArgs(data), sequencePoint);
exprNode_mergeResolve (e, t1, fcn);
exprNode_exprTraverse (pred, FALSE, TRUE, sequencePoint);
temp = pred->ensuresConstraints;
- pred->ensuresConstraints = exprNode_traversEnsuresConstraints(pred);
+ pred->ensuresConstraints = exprNode_traverseEnsuresConstraints(pred);
constraintList_free(temp);
temp = pred->requiresConstraints;
- pred->requiresConstraints = exprNode_traversRequiresConstraints(pred);
+ pred->requiresConstraints = exprNode_traverseRequiresConstraints(pred);
constraintList_free(temp);
temp = pred->trueEnsuresConstraints;
- pred->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(pred);
+ pred->trueEnsuresConstraints = exprNode_traverseTrueEnsuresConstraints(pred);
constraintList_free(temp);
temp = pred->falseEnsuresConstraints;
- pred->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(pred);
+ pred->falseEnsuresConstraints = exprNode_traverseFalseEnsuresConstraints(pred);
constraintList_free(temp);
exprNode_exprTraverse (trueBranch, FALSE, TRUE, sequencePoint);
temp = trueBranch->ensuresConstraints;
- trueBranch->ensuresConstraints = exprNode_traversEnsuresConstraints(trueBranch);
+ trueBranch->ensuresConstraints = exprNode_traverseEnsuresConstraints(trueBranch);
constraintList_free(temp);
temp = trueBranch->requiresConstraints;
- trueBranch->requiresConstraints = exprNode_traversRequiresConstraints(trueBranch);
+ trueBranch->requiresConstraints = exprNode_traverseRequiresConstraints(trueBranch);
constraintList_free(temp);
-
- temp = trueBranch->trueEnsuresConstraints;
- trueBranch->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(trueBranch);
+ temp = trueBranch->trueEnsuresConstraints;
+ trueBranch->trueEnsuresConstraints = exprNode_traverseTrueEnsuresConstraints(trueBranch);
constraintList_free(temp);
- temp = trueBranch->falseEnsuresConstraints;
- trueBranch->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(trueBranch);
+ temp = trueBranch->falseEnsuresConstraints;
+ trueBranch->falseEnsuresConstraints = exprNode_traverseFalseEnsuresConstraints(trueBranch);
constraintList_free(temp);
exprNode_exprTraverse (falseBranch, FALSE, TRUE, sequencePoint);
temp = falseBranch->ensuresConstraints;
- falseBranch->ensuresConstraints = exprNode_traversEnsuresConstraints(falseBranch);
+ falseBranch->ensuresConstraints = exprNode_traverseEnsuresConstraints(falseBranch);
constraintList_free(temp);
temp = falseBranch->requiresConstraints;
- falseBranch->requiresConstraints = exprNode_traversRequiresConstraints(falseBranch);
+ falseBranch->requiresConstraints = exprNode_traverseRequiresConstraints(falseBranch);
constraintList_free(temp);
temp = falseBranch->trueEnsuresConstraints;
- falseBranch->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(falseBranch);
+ falseBranch->trueEnsuresConstraints = exprNode_traverseTrueEnsuresConstraints(falseBranch);
constraintList_free(temp);
temp = falseBranch->falseEnsuresConstraints;
- falseBranch->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(falseBranch);
+ falseBranch->falseEnsuresConstraints = exprNode_traverseFalseEnsuresConstraints(falseBranch);
constraintList_free(temp);
/* if pred is true e equals true otherwise pred equals false */
llassert(FALSE);
t1 = exprData_getPairA (data);
t2 = exprData_getPairB (data);
- /* we essiantially treat this like expr1; expr2
- of course sequencePoint isn't adjusted so this isn't completely accurate
- problems../ */
+ /* we essiantially treat this like expr1; expr2
+ of course sequencePoint isn't adjusted so this isn't completely accurate
+ problems...
+ */
exprNode_exprTraverse (t1, FALSE, FALSE, sequencePoint);
exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint);
exprNode_mergeResolve (e, t1, t2);
break;
default:
- handledExprNode = FALSE;
+ break;
}
- e->requiresConstraints = constraintList_preserveOrig (e->requiresConstraints);
- e->ensuresConstraints = constraintList_preserveOrig (e->ensuresConstraints);
+ e->requiresConstraints = constraintList_preserveOrig (e->requiresConstraints);
+ e->ensuresConstraints = constraintList_preserveOrig (e->ensuresConstraints);
e->requiresConstraints = constraintList_addGeneratingExpr (e->requiresConstraints, e);
-
- e->ensuresConstraints = constraintList_addGeneratingExpr (e->ensuresConstraints, e);
-
-
- e->requiresConstraints = constraintList_removeSurpressed(e->requiresConstraints);
+ e->ensuresConstraints = constraintList_addGeneratingExpr (e->ensuresConstraints, e);
+ e->requiresConstraints = constraintList_removeSurpressed (e->requiresConstraints);
- DPRINTF((message ("ensures constraints for %s are %s", exprNode_unparse(e), constraintList_unparseDetailed(e->ensuresConstraints))));
-
- DPRINTF((message ("Requires constraints for %s are %s", exprNode_unparse(e), constraintList_unparseDetailed(e->ensuresConstraints))));
+ DPRINTF (("ensures constraints for %s are %s",
+ exprNode_unparse(e), constraintList_unparseDetailed (e->ensuresConstraints)));
- DPRINTF((message ("trueEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_unparseDetailed(e->trueEnsuresConstraints))));
-
- DPRINTF((message ("falseEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_unparseDetailed(e->falseEnsuresConstraints))));
+ DPRINTF (("Requires constraints for %s are %s", exprNode_unparse(e),
+ constraintList_unparseDetailed(e->ensuresConstraints)));
+ DPRINTF (("trueEnsures constraints for %s are %s", exprNode_unparse(e),
+ constraintList_unparseDetailed(e->trueEnsuresConstraints)));
+
+ DPRINTF (("falseEnsures constraints for %s are %s", exprNode_unparse(e),
+ constraintList_unparseDetailed(e->falseEnsuresConstraints)));
return;
}
-constraintList exprNode_traversTrueEnsuresConstraints (exprNode e)
+constraintList exprNode_traverseTrueEnsuresConstraints (exprNode e)
{
exprNode t1;
{
case XPR_WHILEPRED:
t1 = exprData_getSingle (data);
- ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints (t1));
+ ret = constraintList_addListFree (ret, exprNode_traverseTrueEnsuresConstraints (t1));
break;
case XPR_FETCH:
ret = constraintList_addListFree (ret,
- exprNode_traversTrueEnsuresConstraints
+ exprNode_traverseTrueEnsuresConstraints
(exprData_getPairA (data)));
ret = constraintList_addListFree (ret,
- exprNode_traversTrueEnsuresConstraints
+ exprNode_traverseTrueEnsuresConstraints
(exprData_getPairB (data)));
break;
case XPR_PREOP:
ret = constraintList_addListFree (ret,
- exprNode_traversTrueEnsuresConstraints
+ exprNode_traverseTrueEnsuresConstraints
(exprData_getUopNode (data)));
break;
case XPR_PARENS:
- ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints
+ ret = constraintList_addListFree (ret, exprNode_traverseTrueEnsuresConstraints
(exprData_getUopNode (data)));
break;
case XPR_INIT:
ret = constraintList_addListFree (ret,
- exprNode_traversTrueEnsuresConstraints
+ exprNode_traverseTrueEnsuresConstraints
(exprData_getInitNode (data)));
break;
case XPR_ASSIGN:
ret = constraintList_addListFree (ret,
- exprNode_traversTrueEnsuresConstraints
+ exprNode_traverseTrueEnsuresConstraints
(exprData_getOpA (data)));
ret = constraintList_addListFree (ret,
- exprNode_traversTrueEnsuresConstraints
+ exprNode_traverseTrueEnsuresConstraints
(exprData_getOpB (data)));
break;
case XPR_OP:
ret = constraintList_addListFree (ret,
- exprNode_traversTrueEnsuresConstraints
+ exprNode_traverseTrueEnsuresConstraints
(exprData_getOpA (data)));
ret = constraintList_addListFree (ret,
- exprNode_traversTrueEnsuresConstraints
+ exprNode_traverseTrueEnsuresConstraints
(exprData_getOpB (data)));
break;
case XPR_SIZEOFT:
case XPR_SIZEOF:
ret = constraintList_addListFree (ret,
- exprNode_traversTrueEnsuresConstraints
+ exprNode_traverseTrueEnsuresConstraints
(exprData_getSingle (data)));
break;
case XPR_CALL:
ret = constraintList_addListFree (ret,
- exprNode_traversTrueEnsuresConstraints
+ exprNode_traverseTrueEnsuresConstraints
(exprData_getFcn (data)));
break;
case XPR_RETURN:
ret = constraintList_addListFree (ret,
- exprNode_traversTrueEnsuresConstraints
+ exprNode_traverseTrueEnsuresConstraints
(exprData_getSingle (data)));
break;
case XPR_FACCESS:
ret = constraintList_addListFree (ret,
- exprNode_traversTrueEnsuresConstraints
+ exprNode_traverseTrueEnsuresConstraints
(exprData_getFieldNode (data)));
break;
case XPR_ARROW:
ret = constraintList_addListFree (ret,
- exprNode_traversTrueEnsuresConstraints
+ exprNode_traverseTrueEnsuresConstraints
(exprData_getFieldNode (data)));
break;
case XPR_POSTOP:
ret = constraintList_addListFree (ret,
- exprNode_traversTrueEnsuresConstraints
+ exprNode_traverseTrueEnsuresConstraints
(exprData_getUopNode (data)));
break;
case XPR_CAST:
ret = constraintList_addListFree (ret,
- exprNode_traversTrueEnsuresConstraints
+ exprNode_traverseTrueEnsuresConstraints
(exprData_getCastNode (data)));
break;
return ret;
}
-constraintList exprNode_traversFalseEnsuresConstraints (exprNode e)
+constraintList exprNode_traverseFalseEnsuresConstraints (exprNode e)
{
exprNode t1;
bool handledExprNode;
{
case XPR_WHILEPRED:
t1 = exprData_getSingle (data);
- ret = constraintList_addListFree (ret,exprNode_traversFalseEnsuresConstraints (t1));
+ ret = constraintList_addListFree (ret,exprNode_traverseFalseEnsuresConstraints (t1));
break;
case XPR_FETCH:
ret = constraintList_addListFree (ret,
- exprNode_traversFalseEnsuresConstraints
+ exprNode_traverseFalseEnsuresConstraints
(exprData_getPairA (data)));
ret = constraintList_addListFree (ret,
- exprNode_traversFalseEnsuresConstraints
+ exprNode_traverseFalseEnsuresConstraints
(exprData_getPairB (data)));
break;
case XPR_PREOP:
ret = constraintList_addListFree (ret,
- exprNode_traversFalseEnsuresConstraints
+ exprNode_traverseFalseEnsuresConstraints
(exprData_getUopNode (data)));
break;
case XPR_PARENS:
- ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints
+ ret = constraintList_addListFree (ret, exprNode_traverseFalseEnsuresConstraints
(exprData_getUopNode (data)));
break;
case XPR_INIT:
ret = constraintList_addListFree (ret,
- exprNode_traversFalseEnsuresConstraints
+ exprNode_traverseFalseEnsuresConstraints
( exprData_getInitNode (data)));
break;
case XPR_ASSIGN:
ret = constraintList_addListFree (ret,
- exprNode_traversFalseEnsuresConstraints
+ exprNode_traverseFalseEnsuresConstraints
(exprData_getOpA (data)));
ret = constraintList_addListFree (ret,
- exprNode_traversFalseEnsuresConstraints
+ exprNode_traverseFalseEnsuresConstraints
(exprData_getOpB (data)));
break;
case XPR_OP:
ret = constraintList_addListFree (ret,
- exprNode_traversFalseEnsuresConstraints
+ exprNode_traverseFalseEnsuresConstraints
(exprData_getOpA (data)));
ret = constraintList_addListFree (ret,
- exprNode_traversFalseEnsuresConstraints
+ exprNode_traverseFalseEnsuresConstraints
(exprData_getOpB (data)));
break;
case XPR_SIZEOFT:
case XPR_SIZEOF:
ret = constraintList_addListFree (ret,
- exprNode_traversFalseEnsuresConstraints
+ exprNode_traverseFalseEnsuresConstraints
(exprData_getSingle (data)));
break;
case XPR_CALL:
ret = constraintList_addListFree (ret,
- exprNode_traversFalseEnsuresConstraints
+ exprNode_traverseFalseEnsuresConstraints
(exprData_getFcn (data)));
break;
case XPR_RETURN:
ret = constraintList_addListFree (ret,
- exprNode_traversFalseEnsuresConstraints
+ exprNode_traverseFalseEnsuresConstraints
(exprData_getSingle (data)));
break;
case XPR_FACCESS:
ret = constraintList_addListFree (ret,
- exprNode_traversFalseEnsuresConstraints
+ exprNode_traverseFalseEnsuresConstraints
(exprData_getFieldNode (data)));
break;
case XPR_ARROW:
ret = constraintList_addListFree (ret,
- exprNode_traversFalseEnsuresConstraints
+ exprNode_traverseFalseEnsuresConstraints
(exprData_getFieldNode (data)));
break;
case XPR_POSTOP:
ret = constraintList_addListFree (ret,
- exprNode_traversFalseEnsuresConstraints
+ exprNode_traverseFalseEnsuresConstraints
(exprData_getUopNode (data)));
break;
case XPR_CAST:
ret = constraintList_addListFree (ret,
- exprNode_traversFalseEnsuresConstraints
+ exprNode_traverseFalseEnsuresConstraints
(exprData_getCastNode (data)));
break;
/* walk down the tree and get all requires Constraints in each subexpression*/
-/*@only@*/ constraintList exprNode_traversRequiresConstraints (exprNode e)
+/*@only@*/ constraintList exprNode_traverseRequiresConstraints (exprNode e)
{
exprNode t1;
{
case XPR_WHILEPRED:
t1 = exprData_getSingle (data);
- ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints (t1));
+ ret = constraintList_addListFree (ret, exprNode_traverseRequiresConstraints (t1));
break;
case XPR_FETCH:
ret = constraintList_addListFree (ret,
- exprNode_traversRequiresConstraints
+ exprNode_traverseRequiresConstraints
(exprData_getPairA (data)));
ret = constraintList_addListFree (ret,
- exprNode_traversRequiresConstraints
+ exprNode_traverseRequiresConstraints
(exprData_getPairB (data)));
break;
case XPR_PREOP:
ret = constraintList_addListFree (ret,
- exprNode_traversRequiresConstraints
+ exprNode_traverseRequiresConstraints
(exprData_getUopNode (data)));
break;
case XPR_PARENS:
- ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints
+ ret = constraintList_addListFree (ret, exprNode_traverseRequiresConstraints
(exprData_getUopNode (data)));
break;
case XPR_INIT:
ret = constraintList_addListFree (ret,
- exprNode_traversRequiresConstraints
+ exprNode_traverseRequiresConstraints
(exprData_getInitNode (data)));
break;
case XPR_ASSIGN:
ret = constraintList_addListFree (ret,
- exprNode_traversRequiresConstraints
+ exprNode_traverseRequiresConstraints
(exprData_getOpA (data)));
ret = constraintList_addListFree (ret,
- exprNode_traversRequiresConstraints
+ exprNode_traverseRequiresConstraints
(exprData_getOpB (data)));
break;
case XPR_OP:
ret = constraintList_addListFree (ret,
- exprNode_traversRequiresConstraints
+ exprNode_traverseRequiresConstraints
(exprData_getOpA (data)));
ret = constraintList_addListFree (ret,
- exprNode_traversRequiresConstraints
+ exprNode_traverseRequiresConstraints
(exprData_getOpB (data)));
break;
case XPR_SIZEOFT:
case XPR_SIZEOF:
ret = constraintList_addListFree (ret,
- exprNode_traversRequiresConstraints
+ exprNode_traverseRequiresConstraints
(exprData_getSingle (data)));
break;
case XPR_CALL:
ret = constraintList_addListFree (ret,
- exprNode_traversRequiresConstraints
+ exprNode_traverseRequiresConstraints
(exprData_getFcn (data)));
break;
case XPR_RETURN:
ret = constraintList_addListFree (ret,
- exprNode_traversRequiresConstraints
+ exprNode_traverseRequiresConstraints
(exprData_getSingle (data)));
break;
case XPR_FACCESS:
ret = constraintList_addListFree (ret,
- exprNode_traversRequiresConstraints
+ exprNode_traverseRequiresConstraints
(exprData_getFieldNode (data)));
break;
case XPR_ARROW:
ret = constraintList_addListFree (ret,
- exprNode_traversRequiresConstraints
+ exprNode_traverseRequiresConstraints
(exprData_getFieldNode (data)));
break;
case XPR_POSTOP:
ret = constraintList_addListFree (ret,
- exprNode_traversRequiresConstraints
+ exprNode_traverseRequiresConstraints
(exprData_getUopNode (data)));
break;
case XPR_CAST:
ret = constraintList_addListFree (ret,
- exprNode_traversRequiresConstraints
+ exprNode_traverseRequiresConstraints
(exprData_getCastNode (data)));
break;
/* walk down the tree and get all Ensures Constraints in each subexpression*/
-/*@only@*/ constraintList exprNode_traversEnsuresConstraints (exprNode e)
+/*@only@*/ constraintList exprNode_traverseEnsuresConstraints (exprNode e)
{
exprNode t1;
{
case XPR_WHILEPRED:
t1 = exprData_getSingle (data);
- ret = constraintList_addListFree (ret,exprNode_traversEnsuresConstraints (t1));
+ ret = constraintList_addListFree (ret,exprNode_traverseEnsuresConstraints (t1));
break;
case XPR_FETCH:
ret = constraintList_addListFree (ret,
- exprNode_traversEnsuresConstraints
+ exprNode_traverseEnsuresConstraints
(exprData_getPairA (data)));
ret = constraintList_addListFree (ret,
- exprNode_traversEnsuresConstraints
+ exprNode_traverseEnsuresConstraints
(exprData_getPairB (data)));
break;
case XPR_PREOP:
ret = constraintList_addListFree (ret,
- exprNode_traversEnsuresConstraints
+ exprNode_traverseEnsuresConstraints
(exprData_getUopNode (data)));
break;
case XPR_PARENS:
- ret = constraintList_addListFree (ret, exprNode_traversEnsuresConstraints
+ ret = constraintList_addListFree (ret, exprNode_traverseEnsuresConstraints
(exprData_getUopNode (data)));
break;
case XPR_INIT:
ret = constraintList_addListFree (ret,
- exprNode_traversEnsuresConstraints
+ exprNode_traverseEnsuresConstraints
(exprData_getInitNode (data)));
break;
case XPR_ASSIGN:
ret = constraintList_addListFree (ret,
- exprNode_traversEnsuresConstraints
+ exprNode_traverseEnsuresConstraints
(exprData_getOpA (data)));
ret = constraintList_addListFree (ret,
- exprNode_traversEnsuresConstraints
+ exprNode_traverseEnsuresConstraints
(exprData_getOpB (data)));
break;
case XPR_OP:
ret = constraintList_addListFree (ret,
- exprNode_traversEnsuresConstraints
+ exprNode_traverseEnsuresConstraints
(exprData_getOpA (data)));
ret = constraintList_addListFree (ret,
- exprNode_traversEnsuresConstraints
+ exprNode_traverseEnsuresConstraints
(exprData_getOpB (data)));
break;
case XPR_SIZEOFT:
case XPR_SIZEOF:
ret = constraintList_addListFree (ret,
- exprNode_traversEnsuresConstraints
+ exprNode_traverseEnsuresConstraints
(exprData_getSingle (data)));
break;
case XPR_CALL:
ret = constraintList_addListFree (ret,
- exprNode_traversEnsuresConstraints
+ exprNode_traverseEnsuresConstraints
(exprData_getFcn (data)));
break;
case XPR_RETURN:
ret = constraintList_addListFree (ret,
- exprNode_traversEnsuresConstraints
+ exprNode_traverseEnsuresConstraints
(exprData_getSingle (data)));
break;
case XPR_NULLRETURN:
break;
case XPR_FACCESS:
ret = constraintList_addListFree (ret,
- exprNode_traversEnsuresConstraints
+ exprNode_traverseEnsuresConstraints
(exprData_getFieldNode (data)));
break;
case XPR_ARROW:
ret = constraintList_addListFree (ret,
- exprNode_traversEnsuresConstraints
+ exprNode_traverseEnsuresConstraints
(exprData_getFieldNode (data)));
break;
case XPR_STRINGLITERAL:
break;
case XPR_POSTOP:
ret = constraintList_addListFree (ret,
- exprNode_traversEnsuresConstraints
+ exprNode_traverseEnsuresConstraints
(exprData_getUopNode (data)));
break;
case XPR_CAST:
ret = constraintList_addListFree (ret,
- exprNode_traversEnsuresConstraints
+ exprNode_traverseEnsuresConstraints
(exprData_getCastNode (data)));
break;
default:
exprNode_exprTraverse (el, FALSE, FALSE, sequencePoint);
temp2 = el->requiresConstraints;
- el->requiresConstraints = exprNode_traversRequiresConstraints(el);
+ el->requiresConstraints = exprNode_traverseRequiresConstraints(el);
constraintList_free(temp2);
temp2 = el->ensuresConstraints;
- el->ensuresConstraints = exprNode_traversEnsuresConstraints(el);
+ el->ensuresConstraints = exprNode_traverseEnsuresConstraints(el);
constraintList_free(temp2);
temp->requiresConstraints = constraintList_addList(temp->requiresConstraints,
/*drl7x */
- if (constraintList_resolve (el, s) )
+ if (constraintList_resolve (el, s))
{
+ DPRINTF (("Resolved constraint: %s", constraint_unparse (el)));
constraint_free (el);
return s;
}
+
+ DPRINTF (("Adding constraint: %s", constraint_unparse (el)));
if (s->nspace <= 0)
constraintList_grow (s);
/*@only@*/ constraintList constraintList_addList (/*@only@*/ /*@returned@*/ constraintList s, /*@observer@*/ /*@temp@*/ constraintList newList)
{
- llassert(constraintList_isDefined(s) );
- llassert(constraintList_isDefined(newList) );
+ llassert(constraintList_isDefined (s));
+ llassert(constraintList_isDefined (newList));
if (newList == constraintList_undefined)
return s;
constraintList_elements (newList, elem)
{
- s = constraintList_add (s, constraint_copy(elem) );
+ s = constraintList_add (s, constraint_copy(elem));
}
end_constraintList_elements;
end_constraintList_elements; ;
}
+//! don't use this!
+void constraintList_castConstraints (constraintList c, ctype tfrom, ctype tto)
+{
+ if (TRUE) /* flag to allow casting */
+ {
+ int fsize = ctype_getSize (tfrom);
+ int tsize = ctype_getSize (tto);
+
+ DPRINTF (("Sizes: [%s] [%s] %d / %d", ctype_unparse (tfrom),
+ ctype_unparse (tto), fsize, tsize));
+
+ if (fsize == tsize)
+ {
+ return; /* Sizes match, no change to constraints */
+ }
+ else
+ {
+ float scale = fsize / tsize;
+
+ DPRINTF (("Scaling constraints by: %f", scale));
+
+ constraintList_elements (c, el)
+ {
+ DPRINTF (("Scale: %s", constraint_unparse (el)));
+ // constraint_scaleSize (el, scale);
+ DPRINTF ((" ==> %s", constraint_unparse (el)));
+ }
+ end_constraintList_elements;
+ }
+ }
+}
+
constraintList constraintList_sort (/*@returned@*/ constraintList ret)
{
# include "exprChecks.h"
# include "exprNodeSList.h"
-
/*@access constraint, exprNode @*/ /*!!! NO! Don't do this so recklessly - design your code more carefully so you don't need to! */
-static constraint inequalitySubstitute (/*@returned@*/ constraint p_c, constraintList p_p);
-
-
+static constraint inequalitySubstitute (/*@returned@*/ constraint p_c, constraintList p_p);
static bool rangeCheck (arithType p_ar1, /*@observer@*/ constraintExpr p_expr1, arithType p_ar2, /*@observer@*/ constraintExpr p_expr2);
-static constraint inequalitySubstituteUnsound (/*@returned@*/ constraint p_c, constraintList p_p);
-
-static constraint inequalitySubstituteStrong (/*@returned@*/ constraint p_c, constraintList p_p);
+static constraint inequalitySubstituteUnsound (/*@returned@*/ constraint p_c, constraintList p_p);
+static constraint inequalitySubstituteStrong (/*@returned@*/ constraint p_c, constraintList p_p);
static constraint constraint_searchandreplace (/*@returned@*/ constraint p_c, constraintExpr p_old, constraintExpr p_newExpr);
-
static constraint constraint_addOr (/*@returned@*/ constraint p_orig, /*@observer@*/ constraint p_orConstr);
static bool resolveOr (/*@temp@*/constraint p_c, /*@observer@*/ /*@temp@*/ constraintList p_list);
) ) );
}
-
-
-
/*@only@*/ constraintList constraintList_subsumeEnsures (constraintList list1, constraintList list2)
{
return ret;
}
-
-
/* tries to resolve constraints in list pre2 using post1 */
static /*@only@*/ constraintList reflectChangesNoOr (/*@observer@*/ /*@temp@*/ constraintList pre2, /*@observer@*/ /*@temp@*/ constraintList post1)
constraint ret;
constraint next;
constraint curr;
-
DPRINTF(( message("doResolveOr: constraint %s and list %s", constraint_printOr(c), constraintList_print(post1) ) ));
-
+ *resolved = FALSE;
- *resolved = FALSE;
-
llassert(constraint_isDefined(c) );
ret = constraint_copy(c);
llassert(constraint_isDefined(c1) );
llassert(constraint_isDefined(c2) );
- if (constraintExpr_similar(c1->lexpr, c2->lexpr) )
+ if (constraintExpr_similar (c1->lexpr, c2->lexpr))
{
if (c1->ar == EQ)
if (c1->ar == c2->ar)
{
- DPRINTF ((message ("%s conflicts with %s ", constraint_print (c1), constraint_print(c2) ) ) );
+ DPRINTF (("%s conflicts with %s", constraint_unparse (c1), constraint_unparse (c2)));
return TRUE;
}
}
- /* This is a slight kludg to prevent circular constraints like
+ /* This is a slight kludge to prevent circular constraints like
strlen(str) == maxRead(s) + strlen(str);
*/
{
llassert(constraint_isDefined(conflicting) );
- if (conflicting->ar ==EQ )
+ if (conflicting->ar == EQ)
{
- llassert(constraint_isDefined(good) );
+ llassert (constraint_isDefined(good));
+ DPRINTF (("Replacing here!"));
good->expr = constraintExpr_searchandreplace (good->expr, conflicting->lexpr, conflicting->expr);
good = constraint_simplify (good);
}
return ret;
}
-/*returns true if constraint post satifies cosntriant pre */
-static bool satifies (constraint pre, constraint post)
+/*returns true if constraint post satisfies cosntriant pre */
+
+static bool constraintResolve_satisfies (constraint pre, constraint post)
{
- llassert(constraint_isDefined(pre) );
- llassert(constraint_isDefined(post) );
+ llassert (constraint_isDefined(pre));
+ llassert (constraint_isDefined(post));
- if (constraint_isAlwaysTrue (pre) )
+ if (constraint_isAlwaysTrue (pre))
return TRUE;
if (!constraintExpr_similar (pre->lexpr, post->lexpr) )
{
return FALSE;
}
+
if (constraintExpr_isUndefined(post->expr))
{
llassert(FALSE);
return FALSE;
}
-
+
return rangeCheck (pre->ar, pre->expr, post->ar, post->expr);
}
-bool constraintList_resolve (/*@temp@*/ /*@observer@*/ constraint c, /*@temp@*/ /*@observer@*/ constraintList p)
+bool constraintList_resolve (/*@temp@*/ /*@observer@*/ constraint c,
+ /*@temp@*/ /*@observer@*/ constraintList p)
{
+ DPRINTF (("[resolve] Trying to resolve constraint: %s using %s",
+ constraint_unparse (c),
+ constraintList_unparse (p)));
+
constraintList_elements (p, el)
{
- if ( satifies (c, el) )
+ if (constraintResolve_satisfies (c, el))
{
- DPRINTF ((message ("\n%s Satifies %s\n ", constraint_print(el), constraint_print(c) ) ) );
+ DPRINTF (("constraintList_resolve: %s satifies %s",
+ constraint_unparse (el), constraint_unparse (c)));
return TRUE;
}
- DPRINTF ((message ("\n%s does not satify %s\n ", constraint_print(el), constraint_print(c) ) ) );
+
+ DPRINTF (("constraintList_resolve: %s does not satify %s\n ",
+ constraint_unparse (el), constraint_unparse (c)));
}
end_constraintList_elements;
- DPRINTF ((message ("no constraints satify %s", constraint_print(c) ) ));
+
+ DPRINTF (("No constraints satify: %s", constraint_unparse (c)));
return FALSE;
}
{
case GTE:
case GT:
- if ((ar2 == GT) || (ar2 == GTE) || (ar2 == EQ) )
+ if ((ar2 == GT) || (ar2 == GTE) || (ar2 == EQ))
{
return TRUE;
}
case LT:
case LTE:
- if ((ar2 == LT) || (ar2 == LTE) || (ar2 == EQ) )
+ if ((ar2 == LT) || (ar2 == LTE) || (ar2 == EQ))
return TRUE;
break;
default:
}
/*checks for the case expr2 == sizeof buf1 and buf1 is a fixed array*/
-static bool sizeofBufComp(constraintExpr buf1, constraintExpr expr2)
+static bool sizeofBufComp(constraintExpr buf1, constraintExpr expr2)
{
constraintTerm ct;
exprNode e, t;
e = constraintTerm_getExprNode(ct);
- llassert(exprNode_isDefined(e) );
+ llassert (exprNode_isDefined(e));
- if (! (exprNode_isDefined(e) ) )
+ if (! (exprNode_isDefined(e)))
return FALSE;
if (e->kind != XPR_SIZEOF)
}
}
- if (constraintExpr_similar (l,r) )
+ if (constraintExpr_similar (l,r))
{
switch (c->ar)
{
+ case CASTEQ:
case EQ:
case GTE:
case LTE:
if (constraintExpr_similar (l,r) && (rHasConstant ) )
{
- DPRINTF(( message("constraint_IsAlwaysTrue: after removing constants %s and %s are similar", constraintExpr_unparse(l), constraintExpr_unparse(r) ) ));
- DPRINTF(( message("constraint_IsAlwaysTrue: rconstant is %d", rConstant ) ));
+ DPRINTF(( message("constraint_IsAlwaysTrue: after removing constants %s and %s are similar", constraintExpr_unparse(l), constraintExpr_unparse(r) ) ));
+ DPRINTF(( message("constraint_IsAlwaysTrue: rconstant is %d", rConstant ) ));
constraintExpr_free(l);
constraintExpr_free(r);
static bool rangeCheck (arithType ar1, /*@observer@*/ constraintExpr expr1, arithType ar2, /*@observer@*/ constraintExpr expr2)
{
- DPRINTF ((message ("Doing Range CHECK %s and %s", constraintExpr_unparse(expr1), constraintExpr_unparse(expr2) ) ));
+ DPRINTF (("Doing range check %s and %s",
+ constraintExpr_unparse (expr1), constraintExpr_unparse (expr2)));
- if (! arithType_canResolve (ar1, ar2) )
+ if (!arithType_canResolve (ar1, ar2))
return FALSE;
switch (ar1)
- {
- case GTE:
- if (constraintExpr_similar (expr1, expr2) )
- return TRUE;
- /*@fallthrough@*/
- case GT:
- if (! (constraintExpr_canGetValue (expr1) &&
- constraintExpr_canGetValue (expr2) ) )
- {
- constraintExpr e1, e2;
- bool p1, p2;
- int const1, const2;
-
- e1 = constraintExpr_copy(expr1);
- e2 = constraintExpr_copy(expr2);
-
- e1 = constraintExpr_propagateConstants (e1, &p1, &const1);
-
- e2 = constraintExpr_propagateConstants (e2, &p2, &const2);
-
- if (p1 || p2)
- {
- if (!p1)
- const1 = 0;
-
- if (!p2)
- const2 = 0;
-
- if (const1 <= const2)
- if (constraintExpr_similar (e1, e2) )
- {
- constraintExpr_free(e1);
- constraintExpr_free(e2);
- return TRUE;
- }
- }
- DPRINTF(("Can't Get value"));
-
- constraintExpr_free(e1);
- constraintExpr_free(e2);
- return FALSE;
- }
-
- if (constraintExpr_compare (expr2, expr1) >= 0)
- return TRUE;
-
- return FALSE;
- case EQ:
- if (constraintExpr_similar (expr1, expr2) )
- return TRUE;
-
- return FALSE;
- case LTE:
- if (constraintExpr_similar (expr1, expr2) )
- return TRUE;
- /*@fallthrough@*/
- case LT:
- if (! (constraintExpr_canGetValue (expr1) &&
- constraintExpr_canGetValue (expr2) ) )
- {
- constraintExpr e1, e2;
- bool p1, p2;
- int const1, const2;
-
- e1 = constraintExpr_copy(expr1);
- e2 = constraintExpr_copy(expr2);
-
- e1 = constraintExpr_propagateConstants (e1, &p1, &const1);
-
- e2 = constraintExpr_propagateConstants (e2, &p2, &const2);
-
- if (p1 || p2)
- {
- if (!p1)
- const1 = 0;
-
- if (!p2)
- const2 = 0;
-
- if (const1 >= const2)
- if (constraintExpr_similar (e1, e2) )
- {
- constraintExpr_free(e1);
- constraintExpr_free(e2);
- return TRUE;
- }
- }
- constraintExpr_free(e1);
- constraintExpr_free(e2);
-
- DPRINTF(("Can't Get value"));
- return FALSE;
- }
-
- if (constraintExpr_compare (expr2, expr1) <= 0)
- return TRUE;
-
- return FALSE;
-
- default:
+ {
+ case GTE:
+ if (constraintExpr_similar (expr1, expr2) )
+ return TRUE;
+ /*@fallthrough@*/
+ case GT:
+ if (! (constraintExpr_canGetValue (expr1) &&
+ constraintExpr_canGetValue (expr2) ) )
+ {
+ constraintExpr e1, e2;
+ bool p1, p2;
+ int const1, const2;
+
+ e1 = constraintExpr_copy(expr1);
+ e2 = constraintExpr_copy(expr2);
+
+ e1 = constraintExpr_propagateConstants (e1, &p1, &const1);
+ e2 = constraintExpr_propagateConstants (e2, &p2, &const2);
+
+ if (p1 || p2)
+ {
+ if (!p1)
+ const1 = 0;
+
+ if (!p2)
+ const2 = 0;
+
+ if (const1 <= const2)
+ if (constraintExpr_similar (e1, e2) )
+ {
+ constraintExpr_free(e1);
+ constraintExpr_free(e2);
+ return TRUE;
+ }
+ }
+ DPRINTF(("Can't Get value"));
+
+ constraintExpr_free(e1);
+ constraintExpr_free(e2);
+ return FALSE;
+ }
+
+ if (constraintExpr_compare (expr2, expr1) >= 0)
+ return TRUE;
+
+ return FALSE;
+ case EQ:
+ if (constraintExpr_similar (expr1, expr2) )
+ return TRUE;
+
+ return FALSE;
+ case LTE:
+ if (constraintExpr_similar (expr1, expr2) )
+ return TRUE;
+ /*@fallthrough@*/
+ case LT:
+ if (! (constraintExpr_canGetValue (expr1) &&
+ constraintExpr_canGetValue (expr2) ) )
+ {
+ constraintExpr e1, e2;
+ bool p1, p2;
+ int const1, const2;
+
+ e1 = constraintExpr_copy(expr1);
+ e2 = constraintExpr_copy(expr2);
+
+ e1 = constraintExpr_propagateConstants (e1, &p1, &const1);
+
+ e2 = constraintExpr_propagateConstants (e2, &p2, &const2);
+
+ if (p1 || p2)
+ {
+ if (!p1)
+ const1 = 0;
+
+ if (!p2)
+ const2 = 0;
+
+ if (const1 >= const2)
+ if (constraintExpr_similar (e1, e2) )
+ {
+ constraintExpr_free(e1);
+ constraintExpr_free(e2);
+ return TRUE;
+ }
+ }
+ constraintExpr_free(e1);
+ constraintExpr_free(e2);
+
+ DPRINTF(("Can't Get value"));
+ return FALSE;
+ }
+
+ if (constraintExpr_compare (expr2, expr1) <= 0)
+ return TRUE;
+
+ return FALSE;
+
+ default:
llcontbug((message("Unhandled case in switch: %q", arithType_print(ar1) ) ) );
- }
+ }
BADEXIT;
}
static constraint constraint_searchandreplace (/*@returned@*/ constraint c, constraintExpr old, constraintExpr newExpr)
{
- llassert (constraint_isDefined(c) );
-
- DPRINTF (("Doing replace for lexpr") );
+ llassert (constraint_isDefined(c));
+ DPRINTF (("Starting replace lexpr [%p]: %s < %s ==> %s > in %s", c,
+ constraintExpr_unparse (c->lexpr),
+ constraintExpr_unparse (old), constraintExpr_unparse (newExpr),
+ constraint_unparse (c)));
c->lexpr = constraintExpr_searchandreplace (c->lexpr, old, newExpr);
- DPRINTF (("Doing replace for expr") );
+ DPRINTF (("Finished replace lexpr [%p]: %s", c, constraintExpr_unparse (c->lexpr)));
c->expr = constraintExpr_searchandreplace (c->expr, old, newExpr);
return c;
}
bool ret;
ret = FALSE;
- llassert (constraint_isDefined(c) );
+ llassert (constraint_isDefined (c));
ret = constraintExpr_search (c->lexpr, old);
ret = ret || constraintExpr_search (c->expr, old);
llassert(constraint_isDefined(old));
loc1 = constraint_getFileloc (old);
- loc2 = constraintExpr_getFileloc (substitute->lexpr);
- loc3 = constraintExpr_getFileloc (substitute->expr);
+ loc2 = constraintExpr_loc (substitute->lexpr);
+ loc3 = constraintExpr_loc (substitute->expr);
/* special case of an equality that "contains itself" */
if (constraintExpr_search (substitute->expr, substitute->lexpr) )
}
}
+void constraintTerm_setValue (constraintTerm term, long value)
+{
+ if (term->kind == CTT_INTLITERAL)
+ {
+ term->value.intlit = value;
+ }
+ else
+ {
+ BADBRANCH;
+ }
+}
+
long constraintTerm_getValue (constraintTerm term)
{
llassert (constraintTerm_canGetValue (term));
FLG_NESTEDEXTERN,
FLG_NUMLITERAL,
FLG_ZEROBOOL,
+
/* memchecks flags */
FLG_NULLDEREF,
FLG_NULLSTATE, FLG_NULLASSIGN,
FLG_NULLPASS, FLG_NULLRET,
+ FLG_ALLOCMISMATCH,
FLG_COMPDEF, FLG_COMPMEMPASS, FLG_UNIONDEF,
FLG_RETSTACK,
FLG_NULLSTATE, FLG_NULLDEREF, FLG_NULLASSIGN,
FLG_NULLPASS, FLG_NULLRET,
+ FLG_ALLOCMISMATCH,
FLG_COMPDEF, FLG_COMPMEMPASS, FLG_UNIONDEF, FLG_RETSTACK,
/* memchecks flags */
FLG_NULLSTATE, FLG_NULLDEREF, FLG_NULLASSIGN,
FLG_NULLPASS, FLG_NULLRET,
-
+ FLG_ALLOCMISMATCH,
FLG_COMPDEF, FLG_COMPMEMPASS, FLG_UNIONDEF,
+ /* memory checking flags */
+ FLG_BOUNDSREAD, FLG_BOUNDSWRITE,
+ FLG_LIKELYBOUNDSREAD, FLG_LIKELYBOUNDSWRITE,
+ FLG_CHECKPOST,
+
/* memtrans flags */
FLG_EXPOSETRANS,
FLG_OBSERVERTRANS,
return FALSE;
}
}
+
+int ctbase_getSize (ctbase ct)
+{
+ if (ct == NULL)
+ {
+ return 0;
+ }
+
+ switch (ct->type)
+ {
+ case CT_UNKNOWN:
+ case CT_BOOL:
+ case CT_PRIM:
+ {
+ cprim cp = ct->contents.prim;
+ int nbits = cprim_getExpectedBits (cp);
+ return nbits;
+ }
+ case CT_USER:
+ case CT_ABST:
+ case CT_NUMABST:
+ case CT_EXPFCN:
+ {
+ return 0;
+ }
+ case CT_PTR:
+ {
+ /* Malloc returns void *, but they are bytes. Normal void * is pointer size. */
+ if (ctype_isVoid (ct->contents.base))
+ {
+ return 8;
+ }
+ else
+ {
+ return ctype_getSize (ct->contents.base);
+ }
+ }
+ case CT_FIXEDARRAY: //!
+ case CT_ARRAY:
+ case CT_FCN:
+ case CT_STRUCT:
+ case CT_UNION:
+ case CT_ENUM:
+ case CT_CONJ:
+ break;
+ BADDEFAULT;
+ }
+
+ return 0;
+
+}
ctype ctype_biggerType (ctype c1, ctype c2)
{
- if (ctbase_isBigger (ctype_getCtbaseSafe (c2), ctype_getCtbaseSafe (c1)) )
+ if (ctbase_isBigger (ctype_getCtbaseSafe (c2), ctype_getCtbaseSafe (c1)))
{
return c2;
}
return c1;
}
}
+
+int ctype_getSize (ctype c)
+{
+ return ctbase_getSize (ctype_getCtbaseSafe (ctype_realType (c)));
+}
context_getFlag(FLG_CHECKPOST) ))
{
exprNode_free (body);
- context_exitInnerPlain();
-
+ context_exitInnerPlain();
return;
}
}
exprNode_generateConstraints (body); /* evans 2002-03-02: this should not be declared to take a
dependent... fix it! */
- c = uentry_getFcnPreconditions (ue);
- DPRINTF(("function constraints\n"));
- DPRINTF (("\n\n\n\n\n\n\n"));
+ c = uentry_getFcnPreconditions (ue);
- if (constraintList_isDefined(c) )
+ if (constraintList_isDefined (c))
{
- DPRINTF ((message ("Function preconditions are %s \n\n\n\n\n", constraintList_printDetailed (c) ) ) );
+ DPRINTF ((message ("Function preconditions are %s \n\n\n\n\n",
+ constraintList_unparseDetailed (c) ) ) );
- body->requiresConstraints = constraintList_reflectChangesFreePre (body->requiresConstraints, c);
+ body->requiresConstraints =
+ constraintList_reflectChangesFreePre (body->requiresConstraints, c);
c2 = constraintList_copy (c);
fix = constraintList_makeFixedArrayConstraints (body->uses);
c2 = constraintList_reflectChangesFreePre (c2, fix);
+
constraintList_free (fix);
if (context_getFlag (FLG_ORCONSTRAINT))
}
constraintList_free (body->requiresConstraints);
- DPRINTF ((message ("The body has the required constraints: %s", constraintList_printDetailed (t) ) ) );
+ DPRINTF ((message ("The body has the required constraints: %s", constraintList_unparseDetailed (t) ) ) );
body->requiresConstraints = t;
constraintList_free(body->ensuresConstraints);
body->ensuresConstraints = t;
-
- DPRINTF ((message ("The body has the ensures constraints: %s", constraintList_printDetailed (t) ) ) );
+
+ DPRINTF ((message ("The body has the ensures constraints: %s", constraintList_unparseDetailed (t) ) ) );
constraintList_free(c2);
}
if (constraintList_isDefined(c))
{
DPRINTF ((message ("The Function %s has the preconditions %s",
- uentry_unparse(ue), constraintList_printDetailed(c))));
+ uentry_unparse(ue), constraintList_unparseDetailed(c))));
}
else
{
constraintList post2;
DPRINTF ((message ("The declared function postconditions are %s \n\n\n\n\n",
- constraintList_printDetailed (post) ) ) );
+ constraintList_unparseDetailed (post) ) ) );
post = constraintList_reflectChangesFreePre (post, body->ensuresConstraints);
ConPrint (message ("Splint has found function post conditions:\n%s", constraintList_printDetailed(body->ensuresConstraints) ), g_currentloc);
printf ("The required constraints are:\n%s", constraintList_printDetailed(body->requiresConstraints) );
- printf ("The ensures constraints are:\n%s", constraintList_printDetailed(body->ensuresConstraints) );
+ printf ("The ensures constraints are:\n%s", constraintList_unparseDetailed(body->ensuresConstraints) );
*/
if (constraintList_isDefined(c) )
constraintList_free(c);
context_exitInnerPlain();
-
- /*is it okay not to free this?*/
- exprNode_free (body);
- }
+
+ /* is it okay not to free this? */
+ DPRINTF (("Done checking constraints..."));
+ exprNode_free (body);
+}
void exprChecks_checkEmptyMacroBody (void)
{
ret->edata = exprData_makeCast (tok, e, q);
ret->sref = sRef_copy (e->sref);
-
- DPRINTF (("Cast 2: -> %s", sRef_unparseFull (ret->sref)));
+ DPRINTF (("Cast: -> %s", sRef_unparseFull (ret->sref)));
+
+ constraintList_castConstraints (ret->requiresConstraints, t, c);
+ constraintList_castConstraints (ret->ensuresConstraints, t, c);
+
if (!sRef_isConst (e->sref))
{
usymtab_addForceMustAlias (ret->sref, e->sref);
"Memory read or write may be out of bounds of allocated storage.", 0, 0
},
{
- FK_BOUNDS, FK_MEMORY, plainFlag,
+ FK_BOUNDS, FK_MEMORY, modeFlag,
"likelyboundsread",
FLG_LIKELYBOUNDSREAD,
"likely out of bounds read",
0, 0
},
{
- FK_BOUNDS, FK_MEMORY, plainFlag,
+ FK_BOUNDS, FK_MEMORY, modeFlag,
"likelyboundswrite",
FLG_LIKELYBOUNDSWRITE,
"likely buffer overflow from an out of bounds write",
},
{
- FK_BOUNDS, FK_MEMORY, plainFlag,
+ FK_BOUNDS, FK_MEMORY, modeFlag,
"boundsread",
FLG_BOUNDSREAD,
"possible out of bounds read",
0, 0
},
{
- FK_BOUNDS, FK_MEMORY, plainFlag,
+ FK_BOUNDS, FK_MEMORY, modeFlag,
"boundswrite",
FLG_BOUNDSWRITE,
"possible buffer overflow from an out of bounds write",
{
FK_BOUNDS, FK_MEMORY, plainFlag,
- "implictconstraint",
+ "impboundsconstraints",
FLG_IMPLICTCONSTRAINT,
"generate implicit constraints for functions",
NULL,
0, 0
}, /*drl added flag 4/26/01*/
+ { /* evans added 2003-06-08 */
+ FK_BOUNDS, FK_MEMORY, modeFlag,
+ "allocmismatch",
+ FLG_ALLOCMISMATCH,
+ "type conversion involves storage of non-divisble size",
+ NULL, 0, 0
+ },
+
/*
** 10. Extensible Checking
*/
andersk / splint.git / commitdiff
