X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/15b3d2b27a3dce7a3b65e88fb0d1732e235117f4..35eea586ba9af7af69f0646f5f6a5958b8215dd8:/src/constraintTerm.c diff --git a/src/constraintTerm.c b/src/constraintTerm.c index 215430f..868c9d5 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,10 +38,12 @@ # 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) { @@ -47,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); } @@ -257,7 +283,7 @@ 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: @@ -285,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; @@ -315,7 +336,7 @@ cstring constraintTerm_print (constraintTerm term) /*@*/ switch (term->kind) { case EXPRNODE: - /*@i334*/ //wtf + /*@i334*/ /*wtf*/ s = message ("%s @ %q", exprNode_unparse (term->value.expr), fileloc_unparse (term->loc) ); break; @@ -406,7 +427,20 @@ long constraintTerm_getValue (constraintTerm term) BADEXIT; } -static /*@exposed@*/ sRef constraintTerm_getsRef (constraintTerm t) +/*drl added this 10.30.001 + */ + +/*@exposed@*/ exprNode constraintTerm_getExprNode (constraintTerm t) +{ + llassert (t != NULL); + + llassert (t->kind == EXPRNODE); + + return t->value.expr; + +} + + /*@exposed@*/ sRef constraintTerm_getsRef (constraintTerm t) { llassert (t != NULL); if (t->kind == EXPRNODE) @@ -428,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) ) ) @@ -480,7 +514,7 @@ bool constraintTerm_similar (constraintTerm term1, constraintTerm term2) return FALSE; } - DPRINTF( (message + DPRINTF((message ("Comparing srefs for %s and %s ", constraintTerm_print(term1), constraintTerm_print(term2) ) ) @@ -547,6 +581,10 @@ 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); @@ -567,7 +605,7 @@ void constraintTerm_dump ( /*@observer@*/ constraintTerm t, FILE *f) } -/*@only@*/ constraintTerm constraintTerm_undump ( FILE *f) +/*@only@*/ constraintTerm constraintTerm_undump (FILE *f) { constraintTermType kind; constraintTerm ret; @@ -577,13 +615,17 @@ void constraintTerm_dump ( /*@observer@*/ constraintTerm t, FILE *f) char *str; char *os; - str = mstring_create (MAX_DUMP_LINE_LENGTH); - os = str; + 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) { @@ -613,8 +655,12 @@ void constraintTerm_dump ( /*@observer@*/ constraintTerm t, FILE *f) s = sRef_makeParam (param, t, stateInfo_makeLoc (g_currentloc)); 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); @@ -635,8 +681,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); @@ -667,4 +712,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; +}