X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/3aaedf88e9f7831799d4ec7a3b71599f188661e4..920a3797c23377bfb7332b0c11bda1d708cabb72:/src/forjunk.c diff --git a/src/forjunk.c b/src/forjunk.c index 0f579ac..861d400 100644 --- a/src/forjunk.c +++ b/src/forjunk.c @@ -14,12 +14,38 @@ # include "aliasChecks.h" # include "exprNodeSList.h" -# include "exprData.i" # include "exprDataQuite.i" +/*@access constraint, exprNode @*/ + +/*@access constraintExpr @*/ + +static bool isInc (/*@observer@*/ constraintExpr c) /*@*/ +{ + + llassert(constraintExpr_isDefined(c) ); + if (c->kind == binaryexpr ) + { + constraintExprBinaryOpKind binOP; + constraintExpr t1, t2; + t1 = constraintExprData_binaryExprGetExpr1 (c->data); + t2 = constraintExprData_binaryExprGetExpr2 (c->data); + + binOP = constraintExprData_binaryExprGetOp (c->data); + if (binOP == PLUS) + if (constraintExpr_isLit (t2) && constraintExpr_getValue (t2) == 1 ) + { + return TRUE; + } + } + + return FALSE; +} + + // look for constraints like cexrp = cexrp + 1 -static bool incVar (constraint c) +static bool incVar (/*@notnull@*/ constraint c) /*@*/ { constraintExpr t1; if (c->ar != EQ) @@ -29,18 +55,28 @@ static bool incVar (constraint c) if (! isInc (c->expr ) ) return FALSE; + llassert (constraintExpr_isDefined(c->expr) ); llassert (c->expr->kind == binaryexpr); + t1 = constraintExprData_binaryExprGetExpr1 (c->expr->data); if (constraintExpr_similar (c->lexpr, t1) ) return TRUE; return FALSE; } +/*@noaccess constraintExpr @*/ -static bool increments (constraint c, - constraintExpr var) +static bool increments (/*@observer@*/ constraint c, + /*@observer@*/ constraintExpr var) { + llassert(constraint_isDefined(c) ); + + if (constraint_isUndefined(c) ) + { + return FALSE; + } + llassert (incVar (c)); if (constraintExpr_similar (c->lexpr, var) ) return TRUE; @@ -48,17 +84,33 @@ static bool increments (constraint c, return FALSE; } -static bool canGetForTimes ( exprNode forPred, exprNode forBody) +static bool canGetForTimes (/*@notnull@*/ exprNode forPred, /*@notnull@*/ exprNode forBody) { exprNode init, test, inc, t1, t2; lltok tok; + llassert(exprNode_isDefined (forPred) ); + llassert(exprNode_isDefined (forBody) ); + init = exprData_getTripleInit (forPred->edata); test = exprData_getTripleTest (forPred->edata); inc = exprData_getTripleInc (forPred->edata); - + llassert(exprNode_isDefined(test) ); + + if (exprNode_isUndefined(test) ) + { + return FALSE; + } + + llassert(exprNode_isDefined(inc) ); + + if (exprNode_isUndefined(inc) ) + { + return FALSE; + } + if (test->kind != XPR_PREOP) return FALSE; @@ -79,6 +131,13 @@ static bool canGetForTimes ( exprNode forPred, exprNode forBody) { t1 = exprData_getUopNode (test->edata); t2 = exprData_getUopNode (inc->edata); + llassert(exprNode_isDefined(t2) && exprNode_isDefined(t2) ); + + if (exprNode_isUndefined(t1) || exprNode_isUndefined(t2) ) + { + return FALSE; + } + if (sRef_sameName (t1->sref, t2->sref) ) { return TRUE; @@ -87,16 +146,23 @@ static bool canGetForTimes ( exprNode forPred, exprNode forBody) return FALSE; } -static constraintList getLessThanConstraints (constraintList c) +static /*@only@*/ constraintList getLessThanConstraints (/*@observer@*/ constraintList c) { constraintList ret; - ret = constraintList_new(); + ret = constraintList_makeNew(); constraintList_elements (c, el) { + llassert(constraint_isDefined(el)); + if ( constraint_isUndefined(el) ) + continue; + if (el->ar == LT || el->ar == LTE) { - ret = constraintList_add (ret, el); + constraint temp; + temp = constraint_copy(el); + + ret = constraintList_add (ret, temp); } } end_constraintList_elements; @@ -104,16 +170,18 @@ static constraintList getLessThanConstraints (constraintList c) return ret; } -static constraintList getIncConstraints (constraintList c) +static /*@only@*/ constraintList getIncConstraints (/*@observer@*/ constraintList c) { constraintList ret; - ret = constraintList_new(); + ret = constraintList_makeNew(); constraintList_elements (c, el) { if (incVar (el) ) { - ret = constraintList_add (ret, el); + constraint temp; + temp = constraint_copy(el); + ret = constraintList_add (ret, temp); } } end_constraintList_elements; @@ -121,12 +189,13 @@ static constraintList getIncConstraints (constraintList c) return ret; } -constraintExpr getForTimes ( exprNode forPred, exprNode forBody) +static /*@only@*/ constraintExpr getForTimes (/*@notnull@*/ exprNode forPred, /*@notnull@*/ exprNode forBody) { exprNode init, test, inc, t1, t2; constraintList ltCon; constraintList incCon; + constraintExpr ret; lltok tok; @@ -134,8 +203,8 @@ constraintExpr getForTimes ( exprNode forPred, exprNode forBody) test = exprData_getTripleTest (forPred->edata); inc = exprData_getTripleInc (forPred->edata); - llassert(test); - llassert(inc); + llassert(exprNode_isDefined(test) ); + llassert(exprNode_isDefined(inc) ); ltCon = getLessThanConstraints (test->trueEnsuresConstraints); incCon = getIncConstraints (inc->ensuresConstraints); @@ -146,12 +215,15 @@ constraintExpr getForTimes ( exprNode forPred, exprNode forBody) constraintList_elements (ltCon, el) { - constraintList_elements(incCon, el2); + constraintList_elements(incCon, el2) { if ( increments(el2, el->lexpr) ) { DPRINTF(( message ("getForTimes: %s increments %s", constraint_print(el2), constraint_print(el) ) )); - return constraintExpr_copy (el->expr); + ret = constraintExpr_copy (el->expr); + constraintList_free(ltCon); + constraintList_free(incCon); + return ret; } else @@ -161,6 +233,9 @@ constraintExpr getForTimes ( exprNode forPred, exprNode forBody) } end_constraintList_elements; + + constraintList_free(ltCon); + constraintList_free(incCon); DPRINTF (( message ("getForTimes: %s %s resorting to ugly hack", exprNode_unparse(forPred), exprNode_unparse(forBody) ) )); if (! canGetForTimes (forPred, forBody) ) @@ -198,29 +273,9 @@ constraintExpr getForTimes ( exprNode forPred, exprNode forBody) BADEXIT; } +/*@access constraintExpr @*/ -static bool isInc (constraintExpr c) -{ - - if (c->kind == binaryexpr ) - { - constraintExprBinaryOpKind binOP; - constraintExpr t1, t2; - t1 = constraintExprData_binaryExprGetExpr1 (c->data); - t2 = constraintExprData_binaryExprGetExpr2 (c->data); - - binOP = constraintExprData_binaryExprGetOp (c->data); - if (binOP == PLUS) - if (constraintExpr_isLit (t2) && constraintExpr_getValue (t2) == 1 ) - { - return TRUE; - } - } - - return FALSE; -} - -constraintExpr constraintExpr_searchAndAdd (constraintExpr c, constraintExpr find, constraintExpr add) +static /*@only@*/ constraintExpr constraintExpr_searchAndAdd (/*@only@*/ constraintExpr c, /*@observer@*/ constraintExpr find, /*@observer@*/ constraintExpr add) { constraintExprKind kind; constraintExpr temp; @@ -230,14 +285,18 @@ constraintExpr constraintExpr_searchAndAdd (constraintExpr c, constraintExpr fin if ( constraintExpr_similar (c, find) ) { - #warning mem leak constraintExpr new; + + cstring cPrint; + + cPrint = constraintExpr_unparse(c); + + + new = constraintExpr_makeAddExpr (c, constraintExpr_copy(add) ); - new = constraintExpr_makeAddConstraintExpr (c, add); - - DPRINTF((message ("Replacing %s with %s", - constraintExpr_unparse(c), constraintExpr_unparse(new) + DPRINTF((message ("Replacing %q with %q", + cPrint, constraintExpr_unparse(new) ))); return new; } @@ -250,17 +309,17 @@ constraintExpr constraintExpr_searchAndAdd (constraintExpr c, constraintExpr fin break; case unaryExpr: temp = constraintExprData_unaryExprGetExpr (c->data); - temp = constraintExpr_searchAndAdd (temp, find, add); + temp = constraintExpr_searchAndAdd (constraintExpr_copy(temp), find, add); c->data = constraintExprData_unaryExprSetExpr (c->data, temp); break; case binaryexpr: temp = constraintExprData_binaryExprGetExpr1 (c->data); - temp = constraintExpr_searchAndAdd (temp, find, add); + temp = constraintExpr_searchAndAdd (constraintExpr_copy(temp), find, add); c->data = constraintExprData_binaryExprSetExpr1 (c->data, temp); temp = constraintExprData_binaryExprGetExpr2 (c->data); - temp = constraintExpr_searchAndAdd (temp, find, add); + temp = constraintExpr_searchAndAdd (constraintExpr_copy(temp), find, add); c->data = constraintExprData_binaryExprSetExpr2 (c->data, temp); break; default: @@ -270,7 +329,9 @@ constraintExpr constraintExpr_searchAndAdd (constraintExpr c, constraintExpr fin } -constraint constraint_searchAndAdd (constraint c, constraintExpr find, constraintExpr add) +/*@noaccess constraintExpr @*/ + +static constraint constraint_searchAndAdd (/*@returned@*/ constraint c, /*@observer@*/ constraintExpr find, /*@observer@*/ constraintExpr add) { llassert (constraint_search (c, find) ); @@ -287,13 +348,13 @@ constraint constraint_searchAndAdd (constraint c, constraintExpr find, constrai } -constraintList constraintList_searchAndAdd (constraintList list, - constraintExpr find, constraintExpr add) +/*@only@*/ static constraintList constraintList_searchAndAdd (/*@returned@*/ constraintList list, + /*@observer@*/ constraintExpr find, /*@observer@*/ constraintExpr add) { constraintList newConstraints; constraintList ret; - newConstraints = constraintList_new(); + newConstraints = constraintList_makeNew(); constraintList_elements (list, el) { @@ -303,23 +364,23 @@ constraintList constraintList_searchAndAdd (constraintList list, new = constraint_copy (el); new = constraint_searchAndAdd (new, find, add); + DPRINTF (( (message ("Adding constraint %s ", constraint_print (new)) ) )); newConstraints = constraintList_add (newConstraints, new); - DPRINTF (( (message ("Adding constraint %s ", constraint_print (new)) ) )); } } end_constraintList_elements; - ret = constraintList_addList (list, newConstraints); + ret = constraintList_addListFree (list, newConstraints); return ret; } -void doAdjust(exprNode e, exprNode forPred, exprNode forBody, constraintExpr iterations) +static void doAdjust(/*@unused@*/ exprNode e, /*@unused@*/ exprNode forPred, /*@observer@*/ exprNode forBody, /*@observer@*/ constraintExpr iterations) { constraintList_elements (forBody->ensuresConstraints, el) { - // look fro var = var + 1 + // look for var = var + 1 if (incVar(el) ) { DPRINTF((message ("Found inc variable constraint : %s", constraint_print (el) ) )); @@ -331,8 +392,8 @@ void doAdjust(exprNode e, exprNode forPred, exprNode forBody, constraintExpr it void forLoopHeuristics( exprNode e, exprNode forPred, exprNode forBody) { - exprNode init, test, inc, t1, t2, t3 ,t4; - constraint con; + exprNode init, test, inc; + constraintExpr iterations; init = exprData_getTripleInit (forPred->edata); @@ -344,11 +405,11 @@ void forLoopHeuristics( exprNode e, exprNode forPred, exprNode forBody) iterations = getForTimes (forPred, forBody ); - if (iterations) + if (iterations != NULL) { doAdjust ( e, forPred, forBody, iterations); + constraintExpr_free(iterations); } - }