X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/e5f31c003fe6a778d1224c8a778f750a1a9ebb3d..508533c52d02429894d89b95224577d8e3cf3c48:/src/constraintResolve.c diff --git a/src/constraintResolve.c b/src/constraintResolve.c index 7d7b8be..6f795b3 100644 --- a/src/constraintResolve.c +++ b/src/constraintResolve.c @@ -1,6 +1,6 @@ /* -** LCLint - annotation-assisted static program checker -** Copyright (C) 1994-2001 University of Virginia, +** Splint - annotation-assisted static program checker +** Copyright (C) 1994-2002 University of Virginia, ** Massachusetts Institute of Technology ** ** This program is free software; you can redistribute it and/or modify it @@ -17,9 +17,9 @@ ** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, ** MA 02111-1307, USA. ** -** For information on lclint: lclint-request@cs.virginia.edu -** To report a bug: lclint-bug@cs.virginia.edu -** For more information: http://lclint.cs.virginia.edu +** For information on splint: info@splint.org +** To report a bug: splint-bug@splint.org +** For more information: http://www.splint.org */ /* @@ -30,7 +30,7 @@ /* #define DEBUGPRINT 1 */ # include /* for isdigit */ -# include "lclintMacros.nf" +# include "splintMacros.nf" # include "basic.h" # include "cgrammar.h" # include "cgrammar_tokens.h" @@ -39,7 +39,13 @@ # include "exprNodeSList.h" -/*@access constraint, exprNode @*/ +/*@access constraint, exprNode @*/ /*!!! NO! Don't do this so recklessly - design your code more carefully so you don't need to! */ + +/*@-nullderef@*/ /* !!! DRL needs to fix this code! */ +/*@-nullstate@*/ /* !!! DRL needs to fix this code! */ +/*@-nullpass@*/ /* !!! DRL needs to fix this code! */ +/*@-temptrans@*/ /* !!! DRL needs to fix this code! */ + static constraint inequalitySubstitute (/*@returned@*/ constraint p_c, constraintList p_p); @@ -125,6 +131,13 @@ static /*@only@*/ constraintList reflectChangesEnsuresFree1 (/*@only@*/ constrai DPRINTF((message ("constraintList_mergeRequires: merging %s and %s ", constraintList_print (list1), constraintList_print(list2) ) ) ); + if (context_getFlag (FLG_REDUNDANTCONSTRAINTS) ) + { + ret = constraintList_copy(list1); + ret = constraintList_addList(ret, list2); + return ret; + } + /* get constraints in list1 not satified by list2 */ temp = constraintList_reflectChanges(list1, list2); DPRINTF((message ("constraintList_mergeRequires: temp = %s", constraintList_print(temp) ) ) ); @@ -146,9 +159,9 @@ void exprNode_mergeResolve (exprNode parent, exprNode child1, exprNode child2) { constraintList temp, temp2; - DPRINTF( (message ("magically merging constraint into parent:%s for", exprNode_unparse (parent) )) ); + DPRINTF((message ("magically merging constraint into parent:%s for", exprNode_unparse (parent) )) ); - DPRINTF( (message (" children: %s and %s", exprNode_unparse (child1), exprNode_unparse(child2) ) ) ); + DPRINTF((message (" children: %s and %s", exprNode_unparse (child1), exprNode_unparse(child2) ) ) ); if (exprNode_isError (child1) || exprNode_isError(child2) ) { @@ -176,7 +189,7 @@ void exprNode_mergeResolve (exprNode parent, exprNode child1, exprNode child2) llassert(!exprNode_isError (child1) && ! exprNode_isError(child2) ); - DPRINTF( (message ("Child constraints are %s %s and %s %s", + DPRINTF((message ("Child constraints are %s %s and %s %s", constraintList_print (child1->requiresConstraints), constraintList_print (child1->ensuresConstraints), constraintList_print (child2->requiresConstraints), @@ -199,7 +212,7 @@ void exprNode_mergeResolve (exprNode parent, exprNode child1, exprNode child2) parent->requiresConstraints = temp2; - DPRINTF( (message ("Parent requires constraints are %s ", + DPRINTF((message ("Parent requires constraints are %s ", constraintList_print (parent->requiresConstraints) ) ) ); @@ -209,7 +222,7 @@ void exprNode_mergeResolve (exprNode parent, exprNode child1, exprNode child2) child2->ensuresConstraints); - DPRINTF( (message ("Parent constraints are %s and %s ", + DPRINTF((message ("Parent constraints are %s and %s ", constraintList_print (parent->requiresConstraints), constraintList_print (parent->ensuresConstraints) ) ) ); @@ -235,7 +248,7 @@ void exprNode_mergeResolve (exprNode parent, exprNode child1, exprNode child2) } else { - DPRINTF ( (message ("Subsuming %s", constraint_print (el) ) ) ); + DPRINTF ((message ("Subsuming %s", constraint_print (el) ) ) ); } } end_constraintList_elements; @@ -371,12 +384,22 @@ static /*@only@*/ constraint doResolve (/*@only@*/ constraint c, constraintList constraint temp; llassert(constraint_isUndefined (c->or ) ); + + DPRINTF((message("doResolve:: call on constraint c = : %q and constraintList %q", + constraint_printOr(c), constraintList_print(post1) + ) + )); if (!resolveOr (c, post1) ) { temp = constraint_substitute (c, post1); + DPRINTF((message("doResolve:: after substitute temp is %q", + constraint_printOr(temp) + ) + )); + if (!resolveOr (temp, post1) ) { /* try inequality substitution */ @@ -400,11 +423,57 @@ static /*@only@*/ constraint doResolve (/*@only@*/ constraint c, constraintList if (!resolveOr (temp2, post1) ) { if (!constraint_same (temp, temp2) ) - temp = constraint_addOr (temp, temp2); - + { + /* drl added 8/28/2002*/ + /*make sure that the information from + a post condition like i = i + 1 is transfered + */ + constraint tempSub; + tempSub = constraint_substitute (temp2, post1); + + DPRINTF(( + message("doResolve: adding %s ", + constraint_printOr(tempSub) + ) + )); + + DPRINTF(( + message("doResolve: not adding %s ", + constraint_printOr(temp2) + ) + )); + + temp = constraint_addOr (temp, tempSub); + constraint_free(tempSub); + + } if (!constraint_same (temp, temp3) && !constraint_same (temp3, temp2) ) - temp = constraint_addOr (temp, temp3); - + { + /* drl added 8/28/2002*/ + /*make sure that the information from + a post condition like i = i + 1 is transfered + */ + constraint tempSub; + + tempSub = constraint_substitute (temp3, post1); + + DPRINTF(( + message("doResolve: adding %s ", + constraint_printOr(tempSub) + ) + )); + + + DPRINTF(( + message("doResolve: not adding %s ", + constraint_printOr(temp3) + ) + )); + + temp = constraint_addOr (temp, tempSub); + + constraint_free(tempSub); + } *resolved = FALSE; constraint_free(temp2); @@ -432,7 +501,7 @@ static /*@only@*/ constraint doResolve (/*@only@*/ constraint c, constraintList } constraint_free(c); - *resolved = TRUE; + /*drl bee: pbr*/ *resolved = TRUE; return NULL; } @@ -447,7 +516,7 @@ static /*@only@*/ constraint doResolveOr (/*@observer@*/ /*@temp@*/ constraint c - *resolved = FALSE; + /*drl bee: pbr*/ *resolved = FALSE; ret = constraint_copy(c); @@ -481,7 +550,7 @@ static /*@only@*/ constraint doResolveOr (/*@observer@*/ /*@temp@*/ constraint c curr = doResolve (curr, post1, resolved); - if (*resolved) + /*drl bee: pbr*/ if (*resolved) { /* curr is null so we don't try to free it*/ llassert(curr == NULL); @@ -547,7 +616,7 @@ static /*@only@*/ constraintList reflectChangesEnsures (/*@observer@*/ constrain } else { - DPRINTF ( (message ("Resolved away %s ", constraint_print(el) ) ) ); + DPRINTF ((message ("Resolved away %s ", constraint_print(el) ) ) ); } } end_constraintList_elements; @@ -575,7 +644,7 @@ static bool constraint_conflict (constraint c1, constraint c2) if (c1->ar == EQ) if (c1->ar == c2->ar) { - DPRINTF ( (message ("%s conflicts with %s ", constraint_print (c1), constraint_print(c2) ) ) ); + DPRINTF ((message ("%s conflicts with %s ", constraint_print (c1), constraint_print(c2) ) ) ); return TRUE; } } @@ -598,7 +667,7 @@ static bool constraint_conflict (constraint c1, constraint c2) if (constraintTerm_isExprNode(term) ) { - DPRINTF ( (message ("%s conflicts with %s ", constraint_print (c1), constraint_print(c2) ) ) ); + DPRINTF ((message ("%s conflicts with %s ", constraint_print (c1), constraint_print(c2) ) ) ); return TRUE; } } @@ -606,11 +675,11 @@ static bool constraint_conflict (constraint c1, constraint c2) if (constraint_tooDeep(c1) || constraint_tooDeep(c2) ) { - DPRINTF ( (message ("%s conflicts with %s (constraint is too deep", constraint_print (c1), constraint_print(c2) ) ) ); + DPRINTF ((message ("%s conflicts with %s (constraint is too deep", constraint_print (c1), constraint_print(c2) ) ) ); return TRUE; } - DPRINTF ( (message ("%s doesn't conflict with %s ", constraint_print (c1), constraint_print(c2) ) ) ); + DPRINTF ((message ("%s doesn't conflict with %s ", constraint_print (c1), constraint_print(c2) ) ) ); return FALSE; @@ -692,13 +761,13 @@ bool constraintList_resolve (/*@temp@*/ /*@observer@*/ constraint c, /*@temp@*/ { if ( satifies (c, el) ) { - DPRINTF ( (message ("\n%s Satifies %s\n ", constraint_print(el), constraint_print(c) ) ) ); + DPRINTF ((message ("\n%s Satifies %s\n ", constraint_print(el), constraint_print(c) ) ) ); return TRUE; } - DPRINTF ( (message ("\n%s does not satify %s\n ", constraint_print(el), constraint_print(c) ) ) ); + DPRINTF ((message ("\n%s does not satify %s\n ", constraint_print(el), constraint_print(c) ) ) ); } end_constraintList_elements; - DPRINTF ( (message ("no constraints satify %s", constraint_print(c) ) )); + DPRINTF ((message ("no constraints satify %s", constraint_print(c) ) )); return FALSE; } @@ -708,7 +777,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; } @@ -721,7 +790,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: @@ -738,7 +807,7 @@ static bool sizeofBufComp(constraintExpr buf1, constraintExpr expr2) sRef s1, s2; /*@access constraintExpr@*/ - if ( (expr2->kind != term) && (buf1->kind != term) ) + if ((expr2->kind != term) && (buf1->kind != term) ) return FALSE; @@ -760,7 +829,8 @@ static bool sizeofBufComp(constraintExpr buf1, constraintExpr expr2) /*@i223@*/ /*this may be the wronge thing to test for */ if (sRef_similarRelaxed(s1, s2) || sRef_sameName (s1, s2) ) { - if (ctype_isFixedArray (sRef_getType (s2) ) ) + /*@i22*/ /* get rid of this test of now */ + /* if (ctype_isFixedArray (sRef_getType (s2) ) ) */ return TRUE; } return FALSE; @@ -781,7 +851,7 @@ static bool sizeOfMaxSet( /*@observer@*/ /*@temp@*/ constraint c) l = c->lexpr; r = c->expr; - if (!( (c->ar == EQ) || (c->ar == GTE) || (c->ar == LTE) ) ) + if (!((c->ar == EQ) || (c->ar == GTE) || (c->ar == LTE) ) ) return FALSE; /*check if the constraintExpr is MaxSet(buf) */ @@ -996,7 +1066,7 @@ static bool rangeCheck (arithType ar1, /*@observer@*/ constraintExpr expr1, arit return TRUE; } } - DPRINTF( ("Can't Get value")); + DPRINTF(("Can't Get value")); constraintExpr_free(e1); constraintExpr_free(e2); @@ -1050,7 +1120,7 @@ static bool rangeCheck (arithType ar1, /*@observer@*/ constraintExpr expr1, arit constraintExpr_free(e1); constraintExpr_free(e2); - DPRINTF( ("Can't Get value")); + DPRINTF(("Can't Get value")); return FALSE; } @@ -1089,7 +1159,7 @@ static constraint constraint_adjust (/*@returned@*/ constraint substitute, /*@ob { fileloc loc1, loc2, loc3; - DPRINTF ( (message("Start adjust on %s and %s", constraint_print(substitute), + DPRINTF ((message("Start adjust on %s and %s", constraint_print(substitute), constraint_print(old)) )); @@ -1102,7 +1172,7 @@ static constraint constraint_adjust (/*@returned@*/ constraint substitute, /*@ob if (fileloc_closer (loc1, loc3, loc2)) { constraintExpr temp; - DPRINTF ( (message("Doing adjust on %s", constraint_print(substitute) ) + DPRINTF ((message("Doing adjust on %s", constraint_print(substitute) ) )); temp = substitute->lexpr; substitute->lexpr = substitute->expr; @@ -1132,7 +1202,7 @@ constraint inequalitySubstitute (/*@returned@*/ constraint c, constraintList p constraintList_elements (p, el) { - if ( (el->ar == LT ) ) + if ((el->ar == LT ) ) /* if (!constraint_conflict (c, el) ) */ /*@i523 explain this! */ { constraintExpr temp2; @@ -1184,7 +1254,7 @@ static constraint inequalitySubstituteStrong (/*@returned@*/ constraint c, con { DPRINTF (( message ("inequalitySubstituteStrong examining substituting %s on %s", constraint_print(el), constraint_print(c) ) )); - if ( (el->ar == LT ) || (el->ar == LTE ) ) + if ((el->ar == LT ) || (el->ar == LTE ) ) /* if (!constraint_conflict (c, el) ) */ /*@i523@*/ { constraintExpr temp2; @@ -1200,7 +1270,7 @@ static constraint inequalitySubstituteStrong (/*@returned@*/ constraint c, con )); temp2 = constraintExpr_copy (el->expr); constraintExpr_free(c->expr); - if ( (el->ar == LTE ) ) + if ((el->ar == LTE ) ) { c->expr = temp2; } @@ -1236,7 +1306,7 @@ static constraint inequalitySubstituteUnsound (/*@returned@*/ constraint c, co constraintList_elements (p, el) { DPRINTF (( message ("inequalitySubstituteUnsound examining substituting %s on %s", constraint_print(el), constraint_print(c) ) )); - if ( ( el->ar == LTE) || (el->ar == LT) ) + if (( el->ar == LTE) || (el->ar == LT) ) /* if (!constraint_conflict (c, el) ) */ /*@i532@*/ { constraintExpr temp2; @@ -1278,20 +1348,22 @@ static constraint inequalitySubstituteUnsound (/*@returned@*/ constraint c, co temp = constraint_adjust(temp, ret); - DPRINTF((message ("Substituting %s in the constraint %s", - constraint_print (temp), constraint_print (ret) + DPRINTF((message ("constraint_substitute :: Substituting in %s using %s", + constraint_print (ret), constraint_print (temp) ) ) ); ret = constraint_searchandreplace (ret, temp->lexpr, temp->expr); - DPRINTF(( message ("The new constraint is %s", constraint_print (ret) ) )); + DPRINTF(( message (" constraint_substitute :: The new constraint is %s", constraint_print (ret) ) )); constraint_free(temp); } } end_constraintList_elements; - DPRINTF(( message ("The finial new constraint is %s", constraint_print (ret) ) )); ret = constraint_simplify(ret); + + DPRINTF(( message (" constraint_substitute :: The final new constraint is %s", constraint_print (ret) ) )); + return ret; } @@ -1331,9 +1403,9 @@ return ret; static constraint constraint_solve (/*@returned@*/ constraint c) { - DPRINTF( (message ("Solving %s\n", constraint_print(c) ) ) ); + DPRINTF((message ("Solving %s\n", constraint_print(c) ) ) ); c->expr = constraintExpr_solveBinaryExpr (c->lexpr, c->expr); - DPRINTF( (message ("Solved and got %s\n", constraint_print(c) ) ) ); + DPRINTF((message ("Solved and got %s\n", constraint_print(c) ) ) ); return c; }