X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/b072092f32623dab70e6ffe1613740542ea66748..16c024b587f5ddc115928d5cca7095508aa208d9:/src/constraintTerm.c diff --git a/src/constraintTerm.c b/src/constraintTerm.c index 6f88df0..e49f75d 100644 --- a/src/constraintTerm.c +++ b/src/constraintTerm.c @@ -1,11 +1,35 @@ /* -** constraintExpr.c +** 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 +** 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 splint: info@splint.org +** To report a bug: splint-bug@splint.org +** For more information: http://www.splint.org */ -//#define DEBUGPRINT 1 +/* +** constraintTerm.c +*/ + +/* #define DEBUGPRINT 1 */ # include /* for isdigit */ -# include "lclintMacros.nf" +# include "splintMacros.nf" # include "basic.h" # include "cgrammar.h" # include "cgrammar_tokens.h" @@ -14,18 +38,18 @@ # include "exprNodeSList.h" /*@-czechfcns@*/ +/*@-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! */ -//#include "constraintExpr.h" - -/*@access exprNode @*/ +/*@access exprNode@*/ /* !!! NO! Don't do this recklessly! */ bool constraintTerm_isDefined (constraintTerm t) { return t != NULL; } -/*@unused@*/ static bool constraintTerm_same (constraintTerm p_term1, constraintTerm p_term2) ; - void constraintTerm_free (/*@only@*/ constraintTerm term) { llassert (constraintTerm_isDefined (term)); @@ -49,7 +73,7 @@ void constraintTerm_free (/*@only@*/ constraintTerm term) /* type was set incorrectly */ llcontbug (message("constraintTerm_free type was set incorrectly")); } - // term->value.intlit = 0; + term->kind = ERRORBADCONSTRAINTTERMTYPE; free (term); } @@ -73,6 +97,62 @@ bool constraintTerm_isIntLiteral (constraintTerm term) return FALSE; } + +bool constraintTerm_isInitBlock (/*@observer@*/ /*@temp@*/ constraintTerm c) /*@*/ +{ + llassert (c != NULL); + if (c->kind == EXPRNODE) + { + + if (exprNode_isInitBlock(c->value.expr) ) + { + return TRUE; + } + } + return FALSE; +} + + +bool constraintTerm_isExprNode (/*@observer@*/ /*@temp@*/ constraintTerm c) /*@*/ +{ + llassert (c != NULL); + if (c->kind == EXPRNODE) + { + return TRUE; + } + return FALSE; +} + + +int constraintTerm_getInitBlockLength (/*@observer@*/ /*@temp@*/ constraintTerm c) /*@*/ +{ + + exprNodeList list; + int ret; + llassert (c != NULL); + llassert (constraintTerm_isInitBlock (c) ); + llassert (c->kind == EXPRNODE); + + llassert(exprNode_isDefined(c->value.expr) ); + + if (exprNode_isUndefined(c->value.expr) ) + { + return 1; + } + + if (c->value.expr->edata == exprData_undefined) + { + return 1; + } + list = exprData_getArgs(c->value.expr->edata); + + ret = exprNodeList_size(list); + + return ret; +} + + + bool constraintTerm_isStringLiteral (constraintTerm c) /*@*/ { llassert (c != NULL); @@ -86,6 +166,8 @@ bool constraintTerm_isStringLiteral (constraintTerm c) /*@*/ return FALSE; } + + cstring constraintTerm_getStringLiteral (constraintTerm c) { llassert (c != NULL); @@ -132,7 +214,7 @@ constraintTermType constraintTerm_getKind (constraintTerm t) return (t->value.sref); } -/*@only@*/ constraintTerm constraintTerm_makeExprNode (/*@depenedent@*/ exprNode e) +/*@only@*/ constraintTerm constraintTerm_makeExprNode (/*@dependent@*/ exprNode e) { constraintTerm ret = new_constraintTermExpr(); ret->loc = fileloc_copy(exprNode_getfileloc(e)); @@ -201,11 +283,11 @@ static cstring constraintTerm_getName (constraintTerm term) switch (term->kind) { case EXPRNODE: - /*@i334*/ //wtf + /*@i334*/ /*wtf*/ s = message ("%s", exprNode_unparse (term->value.expr) ); break; case INTLITERAL: - s = message (" %d ", term->value.intlit); + s = message (" %d ", (int) term->value.intlit); break; case SREF: @@ -229,18 +311,13 @@ constraintTerm_doSRefFixBaseParam (/*@returned@*/constraintTerm term, exprNodeLi switch (term->kind) { case EXPRNODE: - /*@i334*/ //wtf - // s = message ("%s @ %s ", exprNode_unparse (term->value.expr), - // fileloc_unparse (term->loc) ); + /*@i334*/ /*wtf*/ break; case INTLITERAL: - // s = message (" %d ", term->value.intlit); - break; + break; case SREF: term->value.sref = sRef_fixBaseParam (term->value.sref, arglist); - // s = message ("%s ", sRef_unparse (term->value.sref) ); - break; default: BADEXIT; @@ -259,16 +336,16 @@ cstring constraintTerm_print (constraintTerm term) /*@*/ switch (term->kind) { case EXPRNODE: - /*@i334*/ //wtf - s = message ("%s @ %q ", exprNode_unparse (term->value.expr), + /*@i334*/ /*wtf*/ + s = message ("%s @ %q", exprNode_unparse (term->value.expr), fileloc_unparse (term->loc) ); break; case INTLITERAL: - s = message (" %d ", term->value.intlit); + s = message ("%d", (int)term->value.intlit); break; case SREF: - s = message ("%q ", sRef_unparseDebug (term->value.sref) ); + s = message ("%q", sRef_unparseDebug (term->value.sref) ); break; default: @@ -279,7 +356,7 @@ cstring constraintTerm_print (constraintTerm term) /*@*/ } -constraintTerm constraintTerm_makeIntLiteral (int i) +constraintTerm constraintTerm_makeIntLiteral (long i) { constraintTerm ret = new_constraintTermExpr(); ret->value.intlit = i; @@ -291,47 +368,79 @@ constraintTerm constraintTerm_makeIntLiteral (int i) bool constraintTerm_canGetValue (constraintTerm term) { if (term->kind == INTLITERAL) - return TRUE; + { + return TRUE; + } + else if (term->kind == SREF) + { + if (sRef_hasValue (term->value.sref)) + { + multiVal mval = sRef_getValue (term->value.sref); + + return multiVal_isInt (mval); /* for now, only try to deal with int values */ + } + else + { + return FALSE; + } + } + else if (term->kind == EXPRNODE) + { + return FALSE; + } else - return FALSE; + { + return FALSE; + } } -int constraintTerm_getValue (constraintTerm term) +long constraintTerm_getValue (constraintTerm term) { - llassert (term->kind == INTLITERAL); - return term->value.intlit; -} + llassert (constraintTerm_canGetValue (term)); -/* same and similar are similar but not the same*/ -static bool constraintTerm_same (constraintTerm term1, constraintTerm term2) -{ - llassert (term1 !=NULL && term2 !=NULL); + if (term->kind == INTLITERAL) + { + return term->value.intlit; + } + else if (term->kind == SREF) + { + if (sRef_hasValue (term->value.sref)) + { + multiVal mval = sRef_getValue (term->value.sref); - if ( (term1->kind != term2->kind) || (term1->kind != EXPRNODE) ) + return multiVal_forceInt (mval); /* for now, only try to deal with int values */ + } + else + { + BADBRANCH; + } + } + else if (term->kind == EXPRNODE) { - return FALSE; + BADBRANCH; } - - DPRINTF ( (message - ("Comparing srefs for %s and %s ", constraintTerm_print(term1), constraintTerm_print(term2) - ) - ) - ); - - if (sRef_same (term1->value.expr->sref, term2->value.expr->sref) ) - { - DPRINTF ((message (" %s and %s are same", constraintTerm_print(term1), constraintTerm_print(term2) ) )); - return TRUE; - } - else - { - DPRINTF ((message (" %s and %s are not same", constraintTerm_print(term1), constraintTerm_print(term2) ) )); - return FALSE; - } - + else + { + BADBRANCH; + } + + BADEXIT; +} + +/*drl added this 10.30.001 + */ + +/*@exposed@*/ exprNode constraintTerm_getExprNode (constraintTerm t) +{ + llassert (t != NULL); + + llassert (t->kind == EXPRNODE); + + return t->value.expr; + } -static /*@exposed@*/ sRef constraintTerm_getsRef (constraintTerm t) + /*@exposed@*/ sRef constraintTerm_getsRef (constraintTerm t) { llassert (t != NULL); if (t->kind == EXPRNODE) @@ -353,7 +462,7 @@ bool constraintTerm_probSame (constraintTerm term1, constraintTerm term2) llassert (term1 !=NULL && term2 !=NULL); - DPRINTF ( (message + DPRINTF ((message ("Comparing srefs for %s and %s ", constraintTerm_print(term1), constraintTerm_print(term2) ) ) @@ -380,48 +489,50 @@ bool constraintTerm_similar (constraintTerm term1, constraintTerm term2) llassert (term1 !=NULL && term2 !=NULL); - if ( (term1->kind == INTLITERAL) && (term2->kind == INTLITERAL) ) + if (constraintTerm_canGetValue (term1) && constraintTerm_canGetValue (term2)) + /* evans 2001-07-24: was (term1->kind == INTLITERAL) && (term2->kind == INTLITERAL) ) */ { - int t1, t2; - llassert (constraintTerm_canGetValue(term1) ); - t1 = constraintTerm_getValue (term1); + long t1, t2; - llassert (constraintTerm_canGetValue(term2) ); + t1 = constraintTerm_getValue (term1); t2 = constraintTerm_getValue (term2); - if (t1 == t2) - return TRUE; - - return FALSE; + + return (t1 == t2); + } + + if (constraintTerm_canGetValue (term1) || constraintTerm_canGetValue (term2)) + { + /* evans 2001-07-24: is this right? */ /*@i534@*/ + return FALSE; } - + s1 = constraintTerm_getsRef (term1); s2 = constraintTerm_getsRef (term2); - if ( ! (sRef_isValid(s1) && sRef_isValid(s2) ) ) + if (!(sRef_isValid(s1) && sRef_isValid(s2))) { return FALSE; } - DPRINTF( (message + DPRINTF((message ("Comparing srefs for %s and %s ", constraintTerm_print(term1), constraintTerm_print(term2) ) ) ); - - if (sRef_similarRelaxed(s1, s2) || sRef_sameName (s1, s2) ) - { - DPRINTF ((message (" %s and %s are same", constraintTerm_print(term1), constraintTerm_print(term2) ) )); - return TRUE; - } - else - { - DPRINTF ((message (" %s and %s are not same", constraintTerm_print(term1), constraintTerm_print(term2) ) )); - return FALSE; - } - + + if (sRef_similarRelaxed(s1, s2) || sRef_sameName (s1, s2) ) + { + DPRINTF ((message (" %s and %s are same", constraintTerm_print(term1), constraintTerm_print(term2) ) )); + return TRUE; + } + else + { + DPRINTF ((message (" %s and %s are not same", constraintTerm_print(term1), constraintTerm_print(term2) ) )); + return FALSE; + } } -void constraintTerm_dump ( /*@observer@*/ constraintTerm t, FILE *f) +void constraintTerm_dump (/*@observer@*/ constraintTerm t, FILE *f) { fileloc loc; constraintTermValue value; @@ -441,8 +552,7 @@ void constraintTerm_dump ( /*@observer@*/ constraintTerm t, FILE *f) case EXPRNODE: u = exprNode_getUentry(t->value.expr); - fprintf(f, "%s\n", cstring_toCharsSafe( uentry_rawName (u) ) - ); + fprintf (f, "%s\n", cstring_toCharsSafe (uentry_rawName (u))); break; case SREF: @@ -455,7 +565,7 @@ void constraintTerm_dump ( /*@observer@*/ constraintTerm t, FILE *f) { fprintf(f, "Result\n"); } - else if (sRef_isParam (s ) ) + else if (sRef_isParam (s)) { int param; ctype ct; @@ -470,17 +580,21 @@ void constraintTerm_dump ( /*@observer@*/ constraintTerm t, FILE *f) fprintf(f, "Param %s %d\n", cstring_toCharsSafe(ctString), (int) param ); cstring_free(ctString); } + else if (sRef_isField (s) ) + { + fprintf(f, "sRef_dump %s\n", cstring_toCharsSafe(sRef_dump(s)) ); + } else { u = sRef_getUentry(s); - fprintf(f, "%s\n", cstring_toCharsSafe(uentry_rawName (u) ) ); + fprintf (f, "%s\n", cstring_toCharsSafe (uentry_rawName (u))); } } break; case INTLITERAL: - fprintf (f, "%d\n", t->value.intlit); + fprintf (f, "%ld\n", t->value.intlit); break; default: @@ -490,23 +604,27 @@ void constraintTerm_dump ( /*@observer@*/ constraintTerm t, FILE *f) } -/*@only@*/ constraintTerm constraintTerm_undump ( FILE *f) +/*@only@*/ constraintTerm constraintTerm_undump (FILE *f) { constraintTermType kind; constraintTerm ret; uentry ue; - char * str; - char * os; + char *str; + char *os; - str = mstring_create (MAX_DUMP_LINE_LENGTH); - os = str; - str = fgets(os, MAX_DUMP_LINE_LENGTH, f); + os = mstring_create (MAX_DUMP_LINE_LENGTH); + + str = fgets (os, MAX_DUMP_LINE_LENGTH, f); + + llassert (str != NULL); kind = (constraintTermType) reader_getInt(&str); str = fgets(os, MAX_DUMP_LINE_LENGTH, f); + llassert (str != NULL); + switch (kind) { @@ -533,11 +651,15 @@ void constraintTerm_dump ( /*@observer@*/ constraintTerm t, FILE *f) ostr2 = str2; t = ctype_undump(&str2) ; - s = sRef_makeParam (param, t ); + s = sRef_makeParam (param, t, stateInfo_makeLoc (g_currentloc, SA_CREATED)); free (ostr2); } - else //This must be an identified that we can search for - // in usymTab + else if (strcmp (term, "sRef_dump" ) == 0 ) + { + reader_checkChar(&str, ' '); + s = sRef_undump (&str); + } + else /* This must be an identified that we can search for in usymTab */ { cstring termStr = cstring_makeLiteralTemp(term); @@ -558,8 +680,7 @@ void constraintTerm_dump ( /*@observer@*/ constraintTerm t, FILE *f) cstring termStr; term = reader_getWord(&str); - //This must be an identifier that we can search for - // in usymTab + /* This must be an identifier that we can search for in usymTab */ termStr = cstring_makeLiteralTemp(term); ue = usymtab_lookup (termStr); @@ -590,4 +711,28 @@ void constraintTerm_dump ( /*@observer@*/ constraintTerm t, FILE *f) +/* drl added sometime before 10/17/001*/ +ctype constraintTerm_getCType (constraintTerm term) +{ + ctype ct; + + switch (term->kind) + { + case EXPRNODE: + ct = exprNode_getType (term->value.expr); + break; + + case INTLITERAL: + /*@i888*/ /* hack */ + ct = ctype_signedintegral; + break; + + case SREF: + ct = sRef_getType (term->value.sref) ; + break; + default: + BADEXIT; + } + return ct; +}