X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/843806586e6443959ee7e4c9365ef8cf8538b319..206c5b0ffa51d0e77856156a60df89695dfe61b8:/src/constraint.c?ds=sidebyside diff --git a/src/constraint.c b/src/constraint.c index fc6e7be..51f1d67 100644 --- a/src/constraint.c +++ b/src/constraint.c @@ -1,8 +1,32 @@ +/* +** LCLint - annotation-assisted static program checker +** Copyright (C) 1994-2001 University of Virginia, +** Massachusetts Institute of Technology +** +** This program is free software; you can redistribute it and/or modify it +** under the terms of the GNU General Public License as published by the +** Free Software Foundation; either version 2 of the License, or (at your +** option) any later version. +** +** This program is distributed in the hope that it will be useful, but +** WITHOUT ANY WARRANTY; without even the implied warranty of +** MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU +** General Public License for more details. +** +** The GNU General Public License is available from http://www.gnu.org/ or +** 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 +*/ + /* ** constraint.c */ -//#define DEBUGPRINT 1 +/* #define DEBUGPRINT 1 */ # include /* for isdigit */ # include "lclintMacros.nf" @@ -25,51 +49,13 @@ static /*@notnull@*/ /*@special@*/ constraint constraint_makeNew (void) /*@post:isnull result->or, result->orig, result->generatingExpr, result->fcnPre @*/ /*@defines result->or, result->generatingExpr, result->orig, result->fcnPre @*/; -/* constraint makeConstraintParse (sRef x, lltok relOp, exprNode cconstant) */ - -/* { */ -/* char *t; */ -/* int c; */ -/* constraint ret; */ -/* ret = constraint_makeNew(); */ -/* llassert (sRef_isValid(x) ); */ -/* if (!sRef_isValid(x)) */ -/* return ret; */ - - -/* ret->lexpr = constraintExpr_makeTermsRef (x); */ -/* #warning fix abstraction */ - -/* if (relOp.tok == GE_OP) */ -/* ret->ar = GTE; */ -/* else if (relOp.tok == LE_OP) */ -/* ret->ar = LTE; */ -/* else if (relOp.tok == EQ_OP) */ -/* ret->ar = EQ; */ -/* else */ -/* llfatalbug(message ("Unsupported relational operator") ); */ - - -/* t = cstring_toCharsSafe (exprNode_unparse(cconstant)); */ -/* c = atoi( t ); */ -/* ret->expr = constraintExpr_makeIntLiteral (c); */ - -/* ret->post = TRUE; */ -/* // ret->orig = ret; */ -/* DPRINTF(("GENERATED CONSTRAINT:")); */ -/* DPRINTF( (message ("%s", constraint_print(ret) ) ) ); */ -/* return ret; */ -/* } */ - - static void advanceField (char **s) { reader_checkChar (s, '@'); } - - +# if 0 static constraint makeConstraintParse2 (constraintExpr l, lltok relOp, exprNode cconstant) { char *t; @@ -96,23 +82,31 @@ static constraint makeConstraintParse2 (constraintExpr l, lltok relOp, exprNode ret->expr = constraintExpr_makeIntLiteral (c); ret->post = TRUE; - // ret->orig = ret; DPRINTF(("GENERATED CONSTRAINT:")); DPRINTF( (message ("%s", constraint_print(ret) ) ) ); return ret; } +# endif bool constraint_same (constraint c1, constraint c2) { - - if (c1->ar != c2->ar) - return FALSE; + llassert (c1 != NULL); + llassert (c2 != NULL); + if (c1->ar != c2->ar) + { + return FALSE; + } + if (!constraintExpr_similar (c1->lexpr, c2->lexpr) ) - return FALSE; + { + return FALSE; + } if (!constraintExpr_similar (c1->expr, c2->expr) ) - return FALSE; + { + return FALSE; + } return TRUE; } @@ -141,8 +135,8 @@ constraint makeConstraintParse3 (constraintExpr l, lltok relOp, constraintExpr r ret->orig = constraint_copy(ret); ret = constraint_simplify (ret); - - // ret->orig = ret; + /* ret->orig = ret; */ + DPRINTF(("GENERATED CONSTRAINT:")); DPRINTF( (message ("%s", constraint_print(ret) ) ) ); return ret; @@ -153,8 +147,7 @@ constraint constraint_copy (/*@temp@*/ /*@observer@*/ constraint c) constraint ret; llassert (constraint_isDefined(c) ); - // DPRINTF((message("Copying constraint %q", constraint_print) )); - + ret = constraint_makeNew(); ret->lexpr = constraintExpr_copy (c->lexpr); ret->ar = c->ar; @@ -281,7 +274,7 @@ constraint constraint_setFcnPre (/*@returned@*/ constraint c ) else { c->fcnPre = TRUE; - // DPRINTF(( message("Warning Setting fcnPre directly") )); + DPRINTF(( message("Warning Setting fcnPre directly") )); } return c; } @@ -324,7 +317,7 @@ bool constraint_hasMaxSet(constraint c) constraint constraint_makeReadSafeExprNode ( exprNode po, exprNode ind) { constraint ret = constraint_makeNew(); - // constraintTerm term; + po = po; ind = ind; ret->lexpr = constraintExpr_makeMaxReadExpr(po); @@ -422,12 +415,9 @@ constraint constraint_makeEnsureMaxReadAtLeast (exprNode t1, exprNode t2, filelo constraint ret; ret = constraint_makeReadSafeExprNode(t1, t2); - - ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint); - + ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint); ret->post = TRUE; - // fileloc_incColumn (ret->lexpr->term->loc); return ret; } @@ -437,7 +427,6 @@ static constraint constraint_makeEnsuresOpConstraintExpr (/*@only@*/ constraintE constraint ret; llassert(constraintExpr_isDefined(c1) && constraintExpr_isDefined(c2) ); - // llassert(sequencePoint); ret = constraint_makeNew(); @@ -459,11 +448,9 @@ static constraint constraint_makeEnsuresOp (/*@dependent@*/ exprNode e1, /*@depe { llcontbug((message("null exprNode, Exprnodes are %s and %s", exprNode_unparse(e1), exprNode_unparse(e2) ) - )); + )); } - // llassert (sequencePoint); - e = e1; c1 = constraintExpr_makeValueExpr (e); @@ -586,26 +573,19 @@ constraint constraint_makeSubtractAssign (exprNode e, exprNode f, fileloc sequen constraint constraint_makeMaxSetSideEffectPostDecrement (exprNode e, fileloc sequencePoint) { constraint ret = constraint_makeNew(); - //constraintTerm term; - // e = exprNode_fakeCopy(e); ret->lexpr = constraintExpr_makeValueExpr (e); ret->ar = EQ; ret->post = TRUE; ret->expr = constraintExpr_makeValueExpr (e); ret->expr = constraintExpr_makeDecConstraintExpr (ret->expr); - ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint); -// fileloc_incColumn ( ret->lexpr->term->loc); -// fileloc_incColumn ( ret->lexpr->term->loc); return ret; } constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc sequencePoint) { constraint ret = constraint_makeNew(); - //constraintTerm term; - // e = exprNode_fakeCopy(e); ret->lexpr = constraintExpr_makeValueExpr (e); ret->ar = EQ; ret->post = TRUE; @@ -613,8 +593,6 @@ constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc seq ret->expr = constraintExpr_makeIncConstraintExpr (ret->expr); ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint); -// fileloc_incColumn ( ret->lexpr->term->loc); -// fileloc_incColumn ( ret->lexpr->term->loc); return ret; } @@ -642,47 +620,31 @@ void constraint_free (/*@only@*/ constraint c) } - -// constraint constraint_makeMaxReadSideEffectPostIncrement (exprNode e, fileloc sequencePoint) -// { -// constraint ret = constraint_makeNew(); -// //constraintTerm term; - -// e = exprNode_fakeCopy(e); -// ret->lexpr = constraintExpr_makeMaxReadExpr(e); -// ret->ar = EQ; -// ret->post = TRUE; -// ret->expr = constraintExpr_makeIncConstraintExpr (e); -// ret->lexpr = constraintExpr_setFileLoc (ret->lexpr, sequencePoint); -// return ret; -// } - - cstring arithType_print (arithType ar) /*@*/ { cstring st = cstring_undefined; switch (ar) { case LT: - st = cstring_makeLiteral (" < "); + st = cstring_makeLiteral ("<"); break; case LTE: - st = cstring_makeLiteral (" <= "); + st = cstring_makeLiteral ("<="); break; case GT: - st = cstring_makeLiteral (" > "); + st = cstring_makeLiteral (">"); break; case GTE: - st = cstring_makeLiteral (" >= "); + st = cstring_makeLiteral (">="); break; case EQ: - st = cstring_makeLiteral (" == "); + st = cstring_makeLiteral ("=="); break; case NONNEGATIVE: - st = cstring_makeLiteral (" NONNEGATIVE "); + st = cstring_makeLiteral ("NONNEGATIVE"); break; case POSITIVE: - st = cstring_makeLiteral (" POSITIVE "); + st = cstring_makeLiteral ("POSITIVE"); break; default: llassert(FALSE); @@ -716,6 +678,22 @@ void constraint_printErrorPostCondition (constraint c, fileloc loc) } } + /*drl added 8-11-001*/ +cstring constraint_printLocation (/*@observer@*/ /*@temp@*/ constraint c) /*@*/ +{ + cstring string, ret; + fileloc errorLoc; + + string = constraint_print(c); + + errorLoc = constraint_getFileloc(c); + + ret = message ("constraint: %q @ %q", string, fileloc_unparse(errorLoc) ); + + fileloc_free(errorLoc); + return ret; + +} @@ -723,7 +701,15 @@ void constraint_printError (constraint c, fileloc loc) { cstring string; fileloc errorLoc, temp; - + + + /*drl 11/26/2001 avoid printing tautological constraints */ + if (constraint_isAlwaysTrue(c) ) + { + return; + } + + string = constraint_printDetailed (c); errorLoc = loc; @@ -737,7 +723,7 @@ void constraint_printError (constraint c, fileloc loc) else { llassert(FALSE); - DPRINTF(( message("constraint %s had undefined fileloc %s", constraint_print(c), fileloc_unparse(temp) ) )); + DPRINTF (("constraint %s had undefined fileloc %s", constraint_print(c), fileloc_unparse(temp))); fileloc_free(temp); errorLoc = fileloc_copy(errorLoc); } @@ -807,8 +793,9 @@ static /*@only@*/ cstring constraint_printDetailedPostCondition (/*@observer@*/ if (context_getFlag (FLG_CONSTRAINTLOCATION) ) { cstring temp; - // llassert (c->generatingExpr); - temp = message ("\nOriginal Generating expression %q: %s\n", fileloc_unparse( exprNode_getfileloc (c->generatingExpr) ), + + temp = message ("\nOriginal Generating expression %q: %s\n", + fileloc_unparse( exprNode_getfileloc (c->generatingExpr) ), genExpr ); st = cstring_concatFree (st, temp); @@ -838,25 +825,24 @@ cstring constraint_printDetailed (constraint c) if (constraint_hasMaxSet(c) ) { - temp = cstring_makeLiteral("Possible out-of-bounds store. "); + temp = cstring_makeLiteral("Possible out-of-bounds store:\n"); } else { - temp = cstring_makeLiteral("Possible out-of-bounds read. "); + temp = cstring_makeLiteral("Possible out-of-bounds read:\n"); } - - st = cstring_concatFree(temp,st); genExpr = exprNode_unparse (c->generatingExpr); - + if (context_getFlag (FLG_CONSTRAINTLOCATION) ) { - temp = message ("\nConstraint generated from expression: %s at %q\n", - genExpr, - fileloc_unparse( exprNode_getfileloc (c->generatingExpr) ) - ); - st = cstring_concatFree (st, temp); + cstring temp2; + temp2 = message ("%s\n", genExpr ); + temp = cstring_concatFree (temp, temp2); } + + st = cstring_concatFree(temp,st); + return st; } @@ -867,18 +853,45 @@ cstring constraint_printDetailed (constraint c) llassert (c !=NULL); if (c->post) { - type = cstring_makeLiteral ("ensures: "); + if (context_getFlag (FLG_PARENCONSTRAINT) ) + { + type = cstring_makeLiteral ("ensures: "); + } + else + { + type = cstring_makeLiteral ("ensures"); + } } else { - type = cstring_makeLiteral ("requires: "); + if (context_getFlag (FLG_PARENCONSTRAINT) ) + { + type = cstring_makeLiteral ("requires: "); + } + else + { + type = cstring_makeLiteral ("requires"); + } + } - st = message ("%q: %q %q %q", - type, - constraintExpr_print (c->lexpr), - arithType_print(c->ar), - constraintExpr_print(c->expr) + if (context_getFlag (FLG_PARENCONSTRAINT) ) + { + st = message ("%q: %q %q %q", + type, + constraintExpr_print (c->lexpr), + arithType_print(c->ar), + constraintExpr_print(c->expr) + ); + } + else + { + st = message ("%q %q %q %q", + type, + constraintExpr_print (c->lexpr), + arithType_print(c->ar), + constraintExpr_print(c->expr) ); + } return st; } @@ -938,19 +951,6 @@ constraint constraint_doFixResult (constraint postcondition, /*@dependent@*/ exp return precondition; } -// bool constraint_hasTerm (constraint c, constraintTerm term) -// { -// DPRINTF((message ("Constraint %s", constraint_print (c) ) ) ); - -// if (constraintExpr_includesTerm (c->lexpr, term) ) -// return TRUE; - -// if (constraintExpr_includesTerm (c->expr, term) ) -// return TRUE; - -// return FALSE; -// } - constraint constraint_preserveOrig (/*@returned@*/ constraint c) /*@modifies c @*/ { @@ -1032,10 +1032,8 @@ constraint constraint_undump (FILE *f) char *os; - s = mstring_create (MAX_DUMP_LINE_LENGTH); + os = mstring_create (MAX_DUMP_LINE_LENGTH); - os = s; - s = fgets(os, MAX_DUMP_LINE_LENGTH, f); /*@i33*/ /*this should probably be wrappered...*/ @@ -1096,7 +1094,7 @@ void constraint_dump (/*@observer@*/ constraint c, FILE *f) } -int constraint_compare (/*@observer@*/ /*@temp@*/ constraint * c1, /*@observer@*/ /*@temp@*/ constraint * c2) /*@*/ +int constraint_compare (/*@observer@*/ /*@temp@*/ const constraint * c1, /*@observer@*/ /*@temp@*/ const constraint * c2) /*@*/ { fileloc loc1, loc2; @@ -1139,3 +1137,39 @@ bool constraint_isPost (/*@observer@*/ /*@temp@*/ constraint c) return (c->post); } + + +static int constraint_getDepth(/*@observer@*/ /*@temp@*/ constraint c) +{ + int l , r; + + l = constraintExpr_getDepth(c->lexpr); + r = constraintExpr_getDepth(c->expr); + + if (l > r) + { + DPRINTF(( message("constraint depth returning %d for %s", l, constraint_print(c) ) )); + return l; + } + else + { + DPRINTF(( message("constraint depth returning %d for %s", r, constraint_print(c) ) )); + return r; + } +} + + +bool constraint_tooDeep (/*@observer@*/ /*@temp@*/ constraint c) +{ + int temp; + + temp = constraint_getDepth(c); + + if (temp >= 20 ) + { + return TRUE; + } + + return FALSE; + +}