From: evans1629 Date: Mon, 9 Jun 2003 06:09:57 +0000 (+0000) Subject: Changes to fix malloc size problem. X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/commitdiff_plain/ae13359213220016611ceaf93109dac6849be88b Changes to fix malloc size problem. Changed strict mode to set bounds checking. This reveals some other problems in the test suite which have not yet been addressed. --- diff --git a/src/Headers/constraint.h b/src/Headers/constraint.h index 05c7ddf..8c82f9d 100644 --- a/src/Headers/constraint.h +++ b/src/Headers/constraint.h @@ -4,17 +4,17 @@ 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; } ; @@ -114,10 +114,10 @@ extern bool constraint_hasMaxSet(constraint p_c); 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) ; diff --git a/src/Headers/constraintExpr.h b/src/Headers/constraintExpr.h index 34def74..a3d262f 100644 --- a/src/Headers/constraintExpr.h +++ b/src/Headers/constraintExpr.h @@ -7,8 +7,7 @@ typedef enum binaryexpr, unaryExpr, term -} -constraintExprKind; +} constraintExprKind; struct s_constraintExpr { constraintExprKind kind; @@ -70,7 +69,7 @@ int constraintExpr_compare (constraintExpr p_expr1, constraintExpr p_expr2) /*@* 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); diff --git a/src/Headers/constraintList.h b/src/Headers/constraintList.h index dc8861c..c9f455c 100644 --- a/src/Headers/constraintList.h +++ b/src/Headers/constraintList.h @@ -83,9 +83,13 @@ extern /*@only@*/ constraintList constraintList_makeFixedArrayConstraints ( /*@o 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); diff --git a/src/Headers/constraintTerm.h b/src/Headers/constraintTerm.h index 1bebd5b..1ecd622 100644 --- a/src/Headers/constraintTerm.h +++ b/src/Headers/constraintTerm.h @@ -41,15 +41,15 @@ constraintTerm constraintTerm_copy (constraintTerm p_term) /*@*/; 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) /*@*/; diff --git a/src/Headers/exprNode.h b/src/Headers/exprNode.h index 12ae15a..eec7b77 100644 --- a/src/Headers/exprNode.h +++ b/src/Headers/exprNode.h @@ -160,7 +160,7 @@ struct s_exprNode fileloc loc; /*@relnull@*/ exprData edata; cstring etext; - /*@notnull@*/ constraintList requiresConstraints; + /*@notnull@*/ constraintList requiresConstraints; /*@notnull@*/ constraintList ensuresConstraints; /* diff --git a/src/Headers/lctype.h b/src/Headers/lctype.h index 3dfd47b..41de16e 100644 --- a/src/Headers/lctype.h +++ b/src/Headers/lctype.h @@ -257,6 +257,12 @@ extern ctype ctype_createUser (typeId p_u) ; 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. */ diff --git a/src/constraint.c b/src/constraint.c index e5f7896..674dee5 100644 --- a/src/constraint.c +++ b/src/constraint.c @@ -261,7 +261,7 @@ fileloc constraint_getFileloc (constraint c) 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) @@ -423,7 +423,16 @@ constraint_makeEnsuresOp (/*@dependent@*/ exprNode e1, /*@dependent@*/ exprNode 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 */ @@ -575,22 +584,25 @@ cstring arithType_print (arithType ar) /*@*/ 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: @@ -606,28 +618,25 @@ void constraint_printErrorPostCondition (constraint c, fileloc loc) 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); } } @@ -642,7 +651,6 @@ cstring constraint_printLocation (/*@observer@*/ /*@temp@*/ constraint c) /*@*/ errorLoc = constraint_getFileloc (c); ret = message ("constraint: %q @ %q", string, fileloc_unparse (errorLoc)); - fileloc_free (errorLoc); return ret; @@ -656,7 +664,6 @@ void constraint_printError (constraint c, fileloc loc) fileloc errorLoc, temp; bool isLikely; - llassert (constraint_isDefined (c) ); @@ -680,13 +687,14 @@ void constraint_printError (constraint c, fileloc loc) 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', ' '); } @@ -694,7 +702,7 @@ void constraint_printError (constraint c, fileloc loc) /*drl added 12/19/2002 print a different error fro "likely" bounds-errors*/ - isLikely = constraint_isConstantOnly(c); + isLikely = constraint_isConstantOnly (c); if (isLikely) { @@ -762,7 +770,7 @@ static cstring constraint_unparseDeep (constraint c) else { st = cstring_concatFree (st, message ("derived from: %q", - constraint_unparseDeep (c->orig))); + constraint_unparseDeep (c->orig))); } } @@ -858,7 +866,7 @@ cstring constraint_unparseDetailed (constraint c) return st; } -/*@only@*/ cstring constraint_unparse (constraint c) /*@*/ +/*@only@*/ cstring constraint_unparse (constraint c) /*@*/ { cstring st = cstring_undefined; cstring type = cstring_undefined; diff --git a/src/constraintExpr.c b/src/constraintExpr.c index f6284c6..74a97ee 100644 --- a/src/constraintExpr.c +++ b/src/constraintExpr.c @@ -54,11 +54,13 @@ static /*@only@*/ constraintExpr 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 @ */ ; @@ -609,7 +611,7 @@ constraintExpr constraintExpr_makeTermsRef (/*@temp@*/ sRef s) 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; } @@ -631,7 +633,8 @@ constraintExpr constraintExpr_makeTermsRef (/*@temp@*/ sRef s) } -/*@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(); @@ -1098,64 +1101,79 @@ constraintExpr_search (/*@observer@*/ constraintExpr c, } -/*@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; } @@ -1166,26 +1184,29 @@ constraintExpr_search (/*@observer@*/ constraintExpr c, 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; } @@ -1526,7 +1547,7 @@ static /*@only@*/ constraintExpr constraintExpr_simplifyunaryExpr (/*@only@*/ co } /*@only@*/ -cstring constraintExpr_unparse (/*@temp@*/ /*@observer@*/ constraintExpr ex) /*@*/ +cstring constraintExpr_unparse (/*@temp@*/ constraintExpr ex) /*@*/ { cstring st; constraintExprKind kind; @@ -1538,15 +1559,14 @@ cstring constraintExpr_unparse (/*@temp@*/ /*@observer@*/ constraintExpr ex) /*@ 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)", @@ -1558,19 +1578,17 @@ cstring constraintExpr_unparse (/*@temp@*/ /*@observer@*/ constraintExpr ex) /*@ 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)) ); } @@ -1843,7 +1861,7 @@ bool constraintExpr_canGetValue (constraintExpr expr) BADEXIT; } -fileloc constraintExpr_getFileloc (constraintExpr expr) +fileloc constraintExpr_loc (constraintExpr expr) { constraintExpr e; constraintTerm t; @@ -1867,12 +1885,12 @@ 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; } @@ -2343,9 +2361,9 @@ int constraintExpr_getDepth (constraintExpr ex) } -bool constraintExpr_canGetCType (constraintExpr e) /*@*/ +bool constraintExpr_canGetCType (constraintExpr e) /*@*/ { - if (constraintExpr_isUndefined(e) ) + if (constraintExpr_isUndefined(e)) return FALSE; if (e->kind == term) @@ -2354,8 +2372,7 @@ bool constraintExpr_canGetCType (constraintExpr e) /*@*/ } 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; } } @@ -2364,9 +2381,8 @@ ctype constraintExpr_getCType (constraintExpr e) /*@*/ { constraintTerm t; - llassert(constraintExpr_isDefined(e) ); - - llassert(constraintExpr_canGetCType(e) ); + llassert (constraintExpr_isDefined (e)); + llassert (constraintExpr_canGetCType (e)); switch (e->kind) { @@ -2375,14 +2391,10 @@ ctype constraintExpr_getCType (constraintExpr e) /*@*/ 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; } @@ -2391,10 +2403,11 @@ ctype constraintExpr_getCType (constraintExpr e) /*@*/ /* 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; } @@ -2403,14 +2416,14 @@ static bool constraintExpr_hasTypeChange(constraintExpr e) { 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; } @@ -2418,10 +2431,8 @@ static bool constraintExpr_hasTypeChange(constraintExpr e) 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) { @@ -2432,11 +2443,8 @@ static ctype constraintExpr_getOrigType (constraintExpr e) { 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)); } } @@ -2446,34 +2454,85 @@ static ctype constraintExpr_getOrigType (constraintExpr e) /*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) { @@ -2482,13 +2541,14 @@ static /*@only@*/ constraintExpr constraintTerm_simpleDivTypeExprNode(/*@only@* 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; @@ -2498,22 +2558,23 @@ static /*@only@*/ constraintExpr constraintTerm_simpleDivTypeExprNode(/*@only@* } 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; @@ -2528,54 +2589,58 @@ static /*@only@*/ constraintExpr constraintTerm_simpleDivTypeExprNode(/*@only@* 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: @@ -2584,70 +2649,57 @@ static /*@only@*/ constraintExpr simpleDivType (/*@only@*/ constraintExpr e, cty 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; } @@ -2659,11 +2711,8 @@ bool constraintExpr_isConstantOnly ( constraintExpr e ) 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) ) diff --git a/src/constraintGeneration.c b/src/constraintGeneration.c index 7595c14..aa8657e 100644 --- a/src/constraintGeneration.c +++ b/src/constraintGeneration.c @@ -48,8 +48,8 @@ static /*@nullwhentrue@*/ bool exprNode_handleError (/*@temp@*/ exprNode p_e); 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 @*/; @@ -117,22 +117,22 @@ bool /*@alt void@*/ exprNode_generateConstraints (/*@temp@*/ exprNode e) 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; @@ -140,13 +140,14 @@ bool /*@alt void@*/ exprNode_generateConstraints (/*@temp@*/ exprNode e) { 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; } @@ -154,8 +155,10 @@ static void exprNode_stmt (/*@temp@*/ exprNode e) { exprNode snode; fileloc loc; - cstring s; + //! cstring s; + DPRINTF (("Generating constraint for: %s", exprNode_unparse (e))); + if (exprNode_isError(e)) { return; @@ -163,26 +166,31 @@ static void exprNode_stmt (/*@temp@*/ exprNode e) /*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; } @@ -199,13 +207,12 @@ static void exprNode_stmt (/*@temp@*/ exprNode e) 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)))); @@ -246,11 +253,11 @@ static void exprNode_stmt (/*@temp@*/ exprNode 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)))); @@ -304,12 +311,11 @@ static exprNode doIf (/*@returned@*/ exprNode e, /*@dependent@*/ exprNode test, 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)))); @@ -330,15 +336,15 @@ static exprNode doIf (/*@returned@*/ exprNode e, /*@dependent@*/ exprNode test, 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); @@ -381,9 +387,9 @@ static exprNode doIf (/*@returned@*/ exprNode e, /*@dependent@*/ exprNode test, 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) @@ -881,7 +887,7 @@ void exprNode_multiStatement (/*@dependent@*/ exprNode e) { constraintList temp2; temp2 = test->trueEnsuresConstraints; - test->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(test); + test->trueEnsuresConstraints = exprNode_traverseTrueEnsuresConstraints(test); constraintList_free(temp2); } @@ -927,15 +933,15 @@ void exprNode_multiStatement (/*@dependent@*/ exprNode e) 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); @@ -952,7 +958,7 @@ void exprNode_multiStatement (/*@dependent@*/ exprNode e) )); temp = p->falseEnsuresConstraints; - p->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(p); + p->falseEnsuresConstraints = exprNode_traverseFalseEnsuresConstraints(p); constraintList_free(temp); /*See comment on trueEnsures*/ @@ -1170,14 +1176,14 @@ static void exprNode_booleanTraverse (/*@dependent@*/ exprNode e, /*@unused@*/ b } } -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)) @@ -1185,21 +1191,14 @@ void exprNode_exprTraverse (/*@dependent@*/ exprNode e, bool definatelv, bool de 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; @@ -1243,28 +1242,16 @@ void exprNode_exprTraverse (/*@dependent@*/ exprNode e, bool definatelv, bool de 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); @@ -1275,14 +1262,24 @@ void exprNode_exprTraverse (/*@dependent@*/ exprNode e, bool definatelv, bool de 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: @@ -1333,16 +1330,19 @@ void exprNode_exprTraverse (/*@dependent@*/ exprNode e, bool definatelv, bool de 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); @@ -1489,57 +1489,56 @@ void exprNode_exprTraverse (/*@dependent@*/ exprNode e, bool definatelv, bool de 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 */ @@ -1557,40 +1556,41 @@ void exprNode_exprTraverse (/*@dependent@*/ exprNode e, bool definatelv, bool de 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; @@ -1614,54 +1614,54 @@ constraintList exprNode_traversTrueEnsuresConstraints (exprNode e) { 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: @@ -1670,19 +1670,19 @@ constraintList exprNode_traversTrueEnsuresConstraints (exprNode e) 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; @@ -1691,13 +1691,13 @@ constraintList exprNode_traversTrueEnsuresConstraints (exprNode e) 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; @@ -1709,14 +1709,14 @@ constraintList exprNode_traversTrueEnsuresConstraints (exprNode e) 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; @@ -1727,7 +1727,7 @@ constraintList exprNode_traversTrueEnsuresConstraints (exprNode e) return ret; } -constraintList exprNode_traversFalseEnsuresConstraints (exprNode e) +constraintList exprNode_traverseFalseEnsuresConstraints (exprNode e) { exprNode t1; bool handledExprNode; @@ -1748,52 +1748,52 @@ constraintList exprNode_traversFalseEnsuresConstraints (exprNode e) { 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: @@ -1802,19 +1802,19 @@ constraintList exprNode_traversFalseEnsuresConstraints (exprNode e) 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; @@ -1823,13 +1823,13 @@ constraintList exprNode_traversFalseEnsuresConstraints (exprNode e) 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; @@ -1841,14 +1841,14 @@ constraintList exprNode_traversFalseEnsuresConstraints (exprNode e) 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; @@ -1861,7 +1861,7 @@ constraintList exprNode_traversFalseEnsuresConstraints (exprNode e) /* 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; @@ -1883,52 +1883,52 @@ constraintList exprNode_traversFalseEnsuresConstraints (exprNode e) { 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: @@ -1937,19 +1937,19 @@ constraintList exprNode_traversFalseEnsuresConstraints (exprNode e) 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; @@ -1958,13 +1958,13 @@ constraintList exprNode_traversFalseEnsuresConstraints (exprNode e) 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; @@ -1976,14 +1976,14 @@ constraintList exprNode_traversFalseEnsuresConstraints (exprNode e) 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; @@ -1996,7 +1996,7 @@ constraintList exprNode_traversFalseEnsuresConstraints (exprNode e) /* 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; @@ -2027,52 +2027,52 @@ constraintList exprNode_traversFalseEnsuresConstraints (exprNode e) { 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: @@ -2080,29 +2080,29 @@ constraintList exprNode_traversFalseEnsuresConstraints (exprNode e) 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: @@ -2111,12 +2111,12 @@ constraintList exprNode_traversFalseEnsuresConstraints (exprNode e) 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: @@ -2151,11 +2151,11 @@ void checkArgumentList (/*@out@*/ exprNode temp, exprNodeList arglist, 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, diff --git a/src/constraintList.c b/src/constraintList.c index 985e2c1..c834ec6 100644 --- a/src/constraintList.c +++ b/src/constraintList.c @@ -92,11 +92,14 @@ constraintList_add (/*@returned@*/ constraintList s, /*@only@*/ constraint el) /*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); @@ -126,15 +129,15 @@ static void constraintList_freeShallow (/*@only@*/ constraintList c) /*@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; @@ -632,6 +635,38 @@ void constraintList_dump (/*@observer@*/ constraintList c, FILE *f) 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) { diff --git a/src/constraintResolve.c b/src/constraintResolve.c index 098d9fe..4896a3a 100644 --- a/src/constraintResolve.c +++ b/src/constraintResolve.c @@ -38,21 +38,16 @@ # 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); @@ -225,9 +220,6 @@ void exprNode_mergeResolve (exprNode parent, exprNode child1, exprNode child2) ) ) ); } - - - /*@only@*/ constraintList constraintList_subsumeEnsures (constraintList list1, constraintList list2) { @@ -267,8 +259,6 @@ void exprNode_mergeResolve (exprNode parent, exprNode child1, exprNode child2) return ret; } - - /* tries to resolve constraints in list pre2 using post1 */ static /*@only@*/ constraintList reflectChangesNoOr (/*@observer@*/ /*@temp@*/ constraintList pre2, /*@observer@*/ /*@temp@*/ constraintList post1) @@ -514,14 +504,11 @@ static /*@only@*/ constraint doResolveOr (/*@observer@*/ /*@temp@*/ constraint c 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); @@ -649,17 +636,17 @@ static bool constraint_conflict (constraint c1, constraint c2) 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); */ @@ -699,9 +686,10 @@ static void constraint_fixConflict (/*@temp@*/ constraint good, /*@temp@*/ /*@ob { 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); } @@ -748,42 +736,53 @@ constraintList constraintList_fixConflicts (constraintList list1, constraintList 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; } @@ -793,7 +792,7 @@ static bool arithType_canResolve (arithType ar1, arithType ar2) { case GTE: case GT: - if ((ar2 == GT) || (ar2 == GTE) || (ar2 == EQ) ) + if ((ar2 == GT) || (ar2 == GTE) || (ar2 == EQ)) { return TRUE; } @@ -806,7 +805,7 @@ static bool arithType_canResolve (arithType ar1, arithType ar2) case LT: case LTE: - if ((ar2 == LT) || (ar2 == LTE) || (ar2 == EQ) ) + if ((ar2 == LT) || (ar2 == LTE) || (ar2 == EQ)) return TRUE; break; default: @@ -816,7 +815,7 @@ static bool arithType_canResolve (arithType ar1, arithType ar2) } /*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; @@ -837,9 +836,9 @@ static bool sizeofBufComp(constraintExpr buf1, constraintExpr expr2) 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) @@ -992,10 +991,11 @@ bool constraint_isAlwaysTrue (/*@observer@*/ /*@temp@*/ constraint c) } } - if (constraintExpr_similar (l,r) ) + if (constraintExpr_similar (l,r)) { switch (c->ar) { + case CASTEQ: case EQ: case GTE: case LTE: @@ -1018,8 +1018,8 @@ bool constraint_isAlwaysTrue (/*@observer@*/ /*@temp@*/ constraint c) 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); @@ -1057,125 +1057,127 @@ bool constraint_isAlwaysTrue (/*@observer@*/ /*@temp@*/ constraint c) 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; } @@ -1185,7 +1187,7 @@ bool constraint_search (constraint c, constraintExpr old) /*@*/ 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); @@ -1205,8 +1207,8 @@ static constraint constraint_adjust (/*@returned@*/ constraint substitute, /*@ob 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) ) diff --git a/src/constraintTerm.c b/src/constraintTerm.c index 57172a5..60fe051 100644 --- a/src/constraintTerm.c +++ b/src/constraintTerm.c @@ -386,6 +386,18 @@ bool constraintTerm_canGetValue (constraintTerm term) } } +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)); diff --git a/src/context.c b/src/context.c index 0819834..60d5125 100644 --- a/src/context.c +++ b/src/context.c @@ -1059,10 +1059,12 @@ context_setModeAux (cstring s, bool warn) 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, @@ -1195,6 +1197,7 @@ context_setModeAux (cstring s, bool warn) FLG_NULLSTATE, FLG_NULLDEREF, FLG_NULLASSIGN, FLG_NULLPASS, FLG_NULLRET, + FLG_ALLOCMISMATCH, FLG_COMPDEF, FLG_COMPMEMPASS, FLG_UNIONDEF, FLG_RETSTACK, @@ -1311,9 +1314,14 @@ context_setModeAux (cstring s, bool warn) /* 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, diff --git a/src/ctbase.i b/src/ctbase.i index a8ee579..de8346e 100644 --- a/src/ctbase.i +++ b/src/ctbase.i @@ -2627,3 +2627,54 @@ bool ctbase_isBigger (ctbase ct1, ctbase ct2) 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; + +} diff --git a/src/ctype.c b/src/ctype.c index 8ed249f..d3af606 100644 --- a/src/ctype.c +++ b/src/ctype.c @@ -2838,7 +2838,7 @@ size_t ctype_getArraySize (ctype c) 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; } @@ -2847,3 +2847,8 @@ ctype ctype_biggerType (ctype c1, ctype c2) return c1; } } + +int ctype_getSize (ctype c) +{ + return ctbase_getSize (ctype_getCtbaseSafe (ctype_realType (c))); +} diff --git a/src/exprChecks.c b/src/exprChecks.c index ae0ed4f..db425a7 100644 --- a/src/exprChecks.c +++ b/src/exprChecks.c @@ -966,8 +966,7 @@ void exprNode_checkFunction (/*@unused@*/ uentry ue, /*@only@*/ exprNode body) context_getFlag(FLG_CHECKPOST) )) { exprNode_free (body); - context_exitInnerPlain(); - + context_exitInnerPlain(); return; } } @@ -975,19 +974,20 @@ void exprNode_checkFunction (/*@unused@*/ uentry ue, /*@only@*/ exprNode body) 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)) @@ -1000,7 +1000,7 @@ void exprNode_checkFunction (/*@unused@*/ uentry ue, /*@only@*/ exprNode body) } 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; @@ -1008,15 +1008,15 @@ void exprNode_checkFunction (/*@unused@*/ uentry ue, /*@only@*/ exprNode body) 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 { @@ -1047,7 +1047,7 @@ void exprNode_checkFunction (/*@unused@*/ uentry ue, /*@only@*/ exprNode body) 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); @@ -1090,17 +1090,18 @@ void exprNode_checkFunction (/*@unused@*/ uentry ue, /*@only@*/ exprNode body) 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) { diff --git a/src/exprNode.c b/src/exprNode.c index b8a3c05..15eb9c3 100644 --- a/src/exprNode.c +++ b/src/exprNode.c @@ -5009,9 +5009,12 @@ exprNode_cast (/*@only@*/ lltok tok, /*@only@*/ exprNode e, /*@only@*/ qtype q) 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); diff --git a/src/flags.def b/src/flags.def index cd42428..248f91f 100644 --- a/src/flags.def +++ b/src/flags.def @@ -1919,7 +1919,7 @@ static flaglist flags = "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", @@ -1927,7 +1927,7 @@ static flaglist flags = 0, 0 }, { - FK_BOUNDS, FK_MEMORY, plainFlag, + FK_BOUNDS, FK_MEMORY, modeFlag, "likelyboundswrite", FLG_LIKELYBOUNDSWRITE, "likely buffer overflow from an out of bounds write", @@ -1936,7 +1936,7 @@ static flaglist flags = }, { - FK_BOUNDS, FK_MEMORY, plainFlag, + FK_BOUNDS, FK_MEMORY, modeFlag, "boundsread", FLG_BOUNDSREAD, "possible out of bounds read", @@ -1944,7 +1944,7 @@ static flaglist flags = 0, 0 }, { - FK_BOUNDS, FK_MEMORY, plainFlag, + FK_BOUNDS, FK_MEMORY, modeFlag, "boundswrite", FLG_BOUNDSWRITE, "possible buffer overflow from an out of bounds write", @@ -1980,7 +1980,7 @@ static flaglist flags = { FK_BOUNDS, FK_MEMORY, plainFlag, - "implictconstraint", + "impboundsconstraints", FLG_IMPLICTCONSTRAINT, "generate implicit constraints for functions", NULL, @@ -2021,6 +2021,14 @@ static flaglist flags = 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 */