X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/abd7f89523564e5e238e5852585b98f72c3b48f4..ed62d3fbeda6bb085991cdd683ceacfc57f7afbe:/src/constraintTerm.c diff --git a/src/constraintTerm.c b/src/constraintTerm.c index 8d1aa13..57172a5 100644 --- a/src/constraintTerm.c +++ b/src/constraintTerm.c @@ -1,6 +1,6 @@ /* ** Splint - annotation-assisted static program checker -** Copyright (C) 1994-2002 University of Virginia, +** Copyright (C) 1994-2003 University of Virginia, ** Massachusetts Institute of Technology ** ** This program is free software; you can redistribute it and/or modify it @@ -37,10 +37,6 @@ # include "exprChecks.h" # include "exprNodeSList.h" -/*@-czechfcns@*/ - -/*@access exprNode @*/ - bool constraintTerm_isDefined (constraintTerm t) { return t != NULL; @@ -54,23 +50,23 @@ void constraintTerm_free (/*@only@*/ constraintTerm term) switch (term->kind) { - case EXPRNODE: + case CTT_EXPR: /* we don't free an exprNode*/ break; - case SREF: + case CTT_SREF: /* sref */ sRef_free (term->value.sref); break; - case INTLITERAL: + case CTT_INTLITERAL: /* don't free an int */ break; - case ERRORBADCONSTRAINTTERMTYPE: + case CTT_ERRORBADCONSTRAINTTERMTYPE: default: /* type was set incorrectly */ llcontbug (message("constraintTerm_free type was set incorrectly")); } - term->kind = ERRORBADCONSTRAINTTERMTYPE; + term->kind = CTT_ERRORBADCONSTRAINTTERMTYPE; free (term); } @@ -87,7 +83,7 @@ bool constraintTerm_isIntLiteral (constraintTerm term) { llassert(term != NULL); - if (term->kind == INTLITERAL) + if (term->kind == CTT_INTLITERAL) return TRUE; return FALSE; @@ -97,10 +93,10 @@ bool constraintTerm_isIntLiteral (constraintTerm term) bool constraintTerm_isInitBlock (/*@observer@*/ /*@temp@*/ constraintTerm c) /*@*/ { llassert (c != NULL); - if (c->kind == EXPRNODE) + + if (c->kind == CTT_EXPR) { - - if (exprNode_isInitBlock(c->value.expr) ) + if (exprNode_isInitBlock (c->value.expr)) { return TRUE; } @@ -112,22 +108,22 @@ bool constraintTerm_isInitBlock (/*@observer@*/ /*@temp@*/ constraintTerm c) /*@ bool constraintTerm_isExprNode (/*@observer@*/ /*@temp@*/ constraintTerm c) /*@*/ { llassert (c != NULL); - if (c->kind == EXPRNODE) + + if (c->kind == CTT_EXPR) { return TRUE; } return FALSE; } - +/*@access exprNode@*/ int constraintTerm_getInitBlockLength (/*@observer@*/ /*@temp@*/ constraintTerm c) /*@*/ { - - exprNodeList list; + exprNodeList list; int ret; llassert (c != NULL); llassert (constraintTerm_isInitBlock (c) ); - llassert (c->kind == EXPRNODE); + llassert (c->kind == CTT_EXPR); llassert(exprNode_isDefined(c->value.expr) ); @@ -146,13 +142,13 @@ int constraintTerm_getInitBlockLength (/*@observer@*/ /*@temp@*/ constraintTerm return ret; } - +/*@noaccess exprNode@*/ bool constraintTerm_isStringLiteral (constraintTerm c) /*@*/ { llassert (c != NULL); - if (c->kind == EXPRNODE) + if (c->kind == CTT_EXPR) { if (exprNode_knownStringValue(c->value.expr) ) { @@ -168,14 +164,14 @@ cstring constraintTerm_getStringLiteral (constraintTerm c) { llassert (c != NULL); llassert (constraintTerm_isStringLiteral (c) ); - llassert (c->kind == EXPRNODE); + llassert (c->kind == CTT_EXPR); return (cstring_copy ( multiVal_forceString (exprNode_getValue (c->value.expr) ) ) ); } constraintTerm constraintTerm_simplify (/*@returned@*/ constraintTerm term) /*@modifies term@*/ { - if (term->kind == EXPRNODE) + if (term->kind == CTT_EXPR) { if ( exprNode_knownIntValue (term->value.expr ) ) { @@ -183,7 +179,7 @@ constraintTerm constraintTerm_simplify (/*@returned@*/ constraintTerm term) /*@m temp = exprNode_getLongValue (term->value.expr); term->value.intlit = (int)temp; - term->kind = INTLITERAL; + term->kind = CTT_INTLITERAL; } } return term; @@ -205,27 +201,27 @@ constraintTermType constraintTerm_getKind (constraintTerm t) /*@exposed@*/ sRef constraintTerm_getSRef (constraintTerm t) { llassert (constraintTerm_isDefined(t) ); - llassert (t->kind == SREF); + llassert (t->kind == CTT_SREF); return (t->value.sref); } -/*@only@*/ constraintTerm constraintTerm_makeExprNode (/*@dependent@*/ exprNode e) +/*@only@*/ constraintTerm constraintTerm_makeExprNode (/*@dependent@*/ exprNode e) { - constraintTerm ret = new_constraintTermExpr(); - ret->loc = fileloc_copy(exprNode_getfileloc(e)); + constraintTerm ret = new_constraintTermExpr (); + ret->loc = fileloc_copy (exprNode_loc (e)); ret->value.expr = e; - ret->kind = EXPRNODE; - ret = constraintTerm_simplify(ret); + ret->kind = CTT_EXPR; + ret = constraintTerm_simplify (ret); return ret; } -/*@only@*/ constraintTerm constraintTerm_makesRef (/*@temp@*/ /*@observer@*/ sRef s) +/*@only@*/ constraintTerm constraintTerm_makesRef (/*@temp@*/ /*@observer@*/ sRef s) { constraintTerm ret = new_constraintTermExpr(); ret->loc = fileloc_undefined; ret->value.sref = sRef_saveCopy(s); - ret->kind = SREF; + ret->kind = CTT_SREF; ret = constraintTerm_simplify(ret); return ret; } @@ -240,14 +236,14 @@ constraintTerm constraintTerm_copy (constraintTerm term) switch (term->kind) { - case EXPRNODE: + case CTT_EXPR: ret->value.expr = term->value.expr; break; - case INTLITERAL: + case CTT_INTLITERAL: ret->value.intlit = term->value.intlit; break; - case SREF: + case CTT_SREF: ret->value.sref = sRef_saveCopy(term->value.sref); break; default: @@ -278,15 +274,15 @@ static cstring constraintTerm_getName (constraintTerm term) switch (term->kind) { - case EXPRNODE: - /*@i334*/ /*wtf*/ + case CTT_EXPR: + s = message ("%s", exprNode_unparse (term->value.expr) ); break; - case INTLITERAL: + case CTT_INTLITERAL: s = message (" %d ", (int) term->value.intlit); break; - case SREF: + case CTT_SREF: s = message ("%q", sRef_unparse (term->value.sref) ); break; @@ -306,13 +302,13 @@ constraintTerm_doSRefFixBaseParam (/*@returned@*/constraintTerm term, exprNodeLi switch (term->kind) { - case EXPRNODE: - /*@i334*/ /*wtf*/ + case CTT_EXPR: + break; - case INTLITERAL: + case CTT_INTLITERAL: break; - case SREF: + case CTT_SREF: term->value.sref = sRef_fixBaseParam (term->value.sref, arglist); break; default: @@ -322,7 +318,7 @@ constraintTerm_doSRefFixBaseParam (/*@returned@*/constraintTerm term, exprNodeLi } -cstring constraintTerm_print (constraintTerm term) /*@*/ +cstring constraintTerm_unparse (constraintTerm term) /*@*/ { cstring s; s = cstring_undefined; @@ -331,16 +327,16 @@ cstring constraintTerm_print (constraintTerm term) /*@*/ switch (term->kind) { - case EXPRNODE: - /*@i334*/ /*wtf*/ + case CTT_EXPR: + s = message ("%s @ %q", exprNode_unparse (term->value.expr), fileloc_unparse (term->loc) ); break; - case INTLITERAL: + case CTT_INTLITERAL: s = message ("%d", (int)term->value.intlit); break; - case SREF: + case CTT_SREF: s = message ("%q", sRef_unparseDebug (term->value.sref) ); break; @@ -356,18 +352,18 @@ constraintTerm constraintTerm_makeIntLiteral (long i) { constraintTerm ret = new_constraintTermExpr(); ret->value.intlit = i; - ret->kind = INTLITERAL; + ret->kind = CTT_INTLITERAL; ret->loc = fileloc_undefined; return ret; } bool constraintTerm_canGetValue (constraintTerm term) { - if (term->kind == INTLITERAL) + if (term->kind == CTT_INTLITERAL) { return TRUE; } - else if (term->kind == SREF) + else if (term->kind == CTT_SREF) { if (sRef_hasValue (term->value.sref)) { @@ -380,7 +376,7 @@ bool constraintTerm_canGetValue (constraintTerm term) return FALSE; } } - else if (term->kind == EXPRNODE) + else if (term->kind == CTT_EXPR) { return FALSE; } @@ -394,11 +390,11 @@ long constraintTerm_getValue (constraintTerm term) { llassert (constraintTerm_canGetValue (term)); - if (term->kind == INTLITERAL) + if (term->kind == CTT_INTLITERAL) { return term->value.intlit; } - else if (term->kind == SREF) + else if (term->kind == CTT_SREF) { if (sRef_hasValue (term->value.sref)) { @@ -411,7 +407,7 @@ long constraintTerm_getValue (constraintTerm term) BADBRANCH; } } - else if (term->kind == EXPRNODE) + else if (term->kind == CTT_EXPR) { BADBRANCH; } @@ -430,7 +426,7 @@ long constraintTerm_getValue (constraintTerm term) { llassert (t != NULL); - llassert (t->kind == EXPRNODE); + llassert (t->kind == CTT_EXPR); return t->value.expr; @@ -439,12 +435,12 @@ long constraintTerm_getValue (constraintTerm term) /*@exposed@*/ sRef constraintTerm_getsRef (constraintTerm t) { llassert (t != NULL); - if (t->kind == EXPRNODE) + if (t->kind == CTT_EXPR) { return exprNode_getSref(t->value.expr); } - if (t->kind == SREF) + if (t->kind == CTT_SREF) { return t->value.sref; } @@ -486,7 +482,9 @@ bool constraintTerm_similar (constraintTerm term1, constraintTerm term2) llassert (term1 !=NULL && term2 !=NULL); if (constraintTerm_canGetValue (term1) && constraintTerm_canGetValue (term2)) - /* evans 2001-07-24: was (term1->kind == INTLITERAL) && (term2->kind == INTLITERAL) ) */ + + /*3/30/2003 comment updated to reflect name change form INTLITERAL to CTT_INTLITERAL*/ + /* evans 2001-07-24: was (term1->kind == CTT_INTLITERAL) && (term2->kind == CTT_INTLITERAL) ) */ { long t1, t2; @@ -495,10 +493,16 @@ bool constraintTerm_similar (constraintTerm term1, constraintTerm term2) return (t1 == t2); } - + + /*drl this if statement handles the case where constraintTerm_canGetValue only returns + true for term1 or term2 but no both + if constraintTerm_canGetValue returned tru for both we would have returned in the previous if statement + I suppose this could be done with xor but I've never used xor and don't feel like starting now + besides this way is more effecient. + */ if (constraintTerm_canGetValue (term1) || constraintTerm_canGetValue (term2)) { - /* evans 2001-07-24: is this right? */ /*@i534@*/ + return FALSE; } @@ -528,7 +532,7 @@ bool constraintTerm_similar (constraintTerm term1, constraintTerm term2) } } -void constraintTerm_dump ( /*@observer@*/ constraintTerm t, FILE *f) +void constraintTerm_dump (/*@observer@*/ constraintTerm t, FILE *f) { fileloc loc; constraintTermValue value; @@ -546,13 +550,12 @@ void constraintTerm_dump ( /*@observer@*/ constraintTerm t, FILE *f) switch (kind) { - case EXPRNODE: + case CTT_EXPR: 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: + case CTT_SREF: { sRef s; @@ -562,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; @@ -577,16 +580,20 @@ 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: + case CTT_INTLITERAL: fprintf (f, "%ld\n", t->value.intlit); break; @@ -621,12 +628,16 @@ void constraintTerm_dump ( /*@observer@*/ constraintTerm t, FILE *f) switch (kind) { - case SREF: + case CTT_SREF: { sRef s; char * term; term = reader_getWord(&str); - + + if (term == NULL) + { + llfatalbug (message ("Library file appears to be corrupted.") ); + } if (strcmp (term, "Result") == 0 ) { s = sRef_makeResult (ctype_unknown); @@ -642,11 +653,21 @@ void constraintTerm_dump ( /*@observer@*/ constraintTerm t, FILE *f) str2 = reader_getWord(&str); param = reader_getInt(&str); + if (str2 == NULL) + { + llfatalbug (message ("Library file appears to be corrupted.") ); + } + ostr2 = str2; t = ctype_undump(&str2) ; - s = sRef_makeParam (param, t, stateInfo_makeLoc (g_currentloc)); + s = sRef_makeParam (param, t, stateInfo_makeLoc (g_currentloc, SA_CREATED)); free (ostr2); } + 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); @@ -661,13 +682,19 @@ void constraintTerm_dump ( /*@observer@*/ constraintTerm t, FILE *f) } break; - case EXPRNODE: + case CTT_EXPR: { sRef s; char * term; cstring termStr; term = reader_getWord(&str); + + if (term == NULL) + { + llfatalbug (message ("Library file appears to be corrupted.") ); + } + /* This must be an identifier that we can search for in usymTab */ termStr = cstring_makeLiteralTemp(term); @@ -680,7 +707,7 @@ void constraintTerm_dump ( /*@observer@*/ constraintTerm t, FILE *f) break; - case INTLITERAL: + case CTT_INTLITERAL: { int i; @@ -706,16 +733,15 @@ ctype constraintTerm_getCType (constraintTerm term) switch (term->kind) { - case EXPRNODE: + case CTT_EXPR: ct = exprNode_getType (term->value.expr); break; - case INTLITERAL: - /*@i888*/ /* hack */ + case CTT_INTLITERAL: ct = ctype_signedintegral; break; - case SREF: + case CTT_SREF: ct = sRef_getType (term->value.sref) ; break; default: @@ -724,3 +750,37 @@ ctype constraintTerm_getCType (constraintTerm term) return ct; } +bool constraintTerm_isConstantOnly (constraintTerm term) +{ + switch (term->kind) + { + case CTT_EXPR: + if (exprNode_isNumLiteral (term->value.expr) || + exprNode_isStringLiteral (term->value.expr) || + exprNode_isCharLiteral (term->value.expr) ) + { + return TRUE; + } + else + { + return FALSE; + } + + case CTT_INTLITERAL: + return TRUE; + + case CTT_SREF: + if ( sRef_isConst (term->value.sref) ) + { + return TRUE; + } + else + { + return FALSE; + } + default: + BADEXIT; + } + + BADEXIT; +}