X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/08eb3d0ec56d0574e69334b7a8f09f3bef93b9f4..b87215ab641c38a5509a608751384ebb9f4f8bf9:/src/exprNode.c diff --git a/src/exprNode.c b/src/exprNode.c index 8d31677..8940676 100644 --- a/src/exprNode.c +++ b/src/exprNode.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,16 +17,16 @@ ** 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 */ /* ** exprNode.c */ # include /* for isdigit */ -# include "lclintMacros.nf" +# include "splintMacros.nf" # include "basic.h" # include "cgrammar.h" # include "cgrammar_tokens.h" @@ -35,10 +35,11 @@ # include "transferChecks.h" # include "exprNodeSList.h" +static bool exprNode_sameStorage (exprNode p_e1, exprNode p_e2) /*@*/ ; static bool exprNode_isEmptyStatement (exprNode p_e); static /*@exposed@*/ exprNode exprNode_firstStatement (/*@returned@*/ exprNode p_e); static bool exprNode_isFalseConstant (exprNode p_e) /*@*/ ; -static bool exprNode_isBlock (exprNode p_e); +static bool exprNode_isStatement (exprNode p_e); static void checkGlobUse (uentry p_glob, bool p_isCall, /*@notnull@*/ exprNode p_e); static void exprNode_addUse (exprNode p_e, /*@exposed@*/ sRef p_s); static bool exprNode_matchArgType (ctype p_ct, exprNode p_e); @@ -81,8 +82,7 @@ static /*@observer@*/ cstring exprNode_rootVarName (exprNode p_e); static /*@exposed@*/ exprNode exprNode_lastStatement (/*@returned@*/ exprNode p_e); -static /*@null@*/ sRef defref = sRef_undefined; -static /*@only@*/ exprNode mustExitNode = exprNode_undefined; +static /*@only@*/ exprNode s_mustExitNode = exprNode_undefined; static int checkArgsReal (uentry p_fcn, /*@dependent@*/ exprNode p_f, uentryList p_cl, @@ -105,6 +105,11 @@ static ctype ctypeType; static ctype filelocType; static bool initMod = FALSE; +/*@function void exprNode_swap (sef exprNode, sef exprNode)@*/ +/*@-macroassign@*/ +# define exprNode_swap(e1,e2) do { exprNode m_tmp = (e1); (e1) = (e2); (e2) = m_tmp; } while (FALSE) +/*@=macroassign@*/ + static void exprNode_defineConstraints(/*@sef@*/ /*@special@*/ /*@notnull@*/ exprNode e) /*@defines e->requiresConstraints, e->ensuresConstraints, e->trueEnsuresConstraints, e->falseEnsuresConstraints @*/ @@ -132,8 +137,6 @@ void exprNode_initMod (void) ctypeType = ctype_unknown; filelocType = ctype_unknown; - defref = sRef_undefined; - if (usymtab_existsType (cstring_makeLiteralTemp ("cstring"))) { cstringType = usymtab_lookupAbstractType (cstring_makeLiteralTemp ("cstring")); @@ -211,7 +214,7 @@ void exprNode_initMod (void) void exprNode_destroyMod (void) /*@globals killed regArg, killed outArg, killed outStringArg, - killed mustExitNode, initMod @*/ + killed s_mustExitNode, initMod @*/ { if (initMod) { @@ -219,7 +222,7 @@ exprNode_destroyMod (void) uentry_free (outArg); uentry_free (outStringArg); - exprNode_free (mustExitNode); + exprNode_free (s_mustExitNode); initMod = FALSE; /*@-branchstate@*/ } @@ -228,7 +231,7 @@ exprNode_destroyMod (void) static void exprNode_resetSref (/*@notnull@*/ exprNode e) { - e->sref = defref; + e->sref = sRef_undefined; } exprNode exprNode_fakeCopy (exprNode e) @@ -433,7 +436,7 @@ static /*@notnull@*/ /*@special@*/ exprNode e->typ = c; e->kind = XPR_EMPTY; e->val = multiVal_undefined; - e->sref = defref; + e->sref = sRef_undefined; e->etext = cstring_undefined; e->loc = fileloc_undefined; e->guards = guardSet_undefined; @@ -453,13 +456,13 @@ static /*@notnull@*/ /*@special@*/ exprNode /*@observer@*/ exprNode exprNode_makeMustExit (void) { - if (exprNode_isUndefined (mustExitNode)) + if (exprNode_isUndefined (s_mustExitNode)) { - mustExitNode = exprNode_createPlain (ctype_unknown); - mustExitNode->exitCode = XK_MUSTEXIT; + s_mustExitNode = exprNode_createPlain (ctype_unknown); + s_mustExitNode->exitCode = XK_MUSTEXIT; } - return mustExitNode; + return s_mustExitNode; } @@ -545,7 +548,7 @@ static /*@notnull@*/ /*@special@*/ exprNode } ret->kind = XPR_EMPTY; - ret->sref = defref; + ret->sref = sRef_undefined; ret->etext = cstring_undefined; ret->exitCode = XK_NEVERESCAPE; ret->canBreak = FALSE; @@ -597,7 +600,7 @@ static /*@notnull@*/ /*@special@*/ exprNode ret->val = multiVal_undefined; ret->kind = XPR_EMPTY; - ret->sref = defref; + ret->sref = sRef_undefined; ret->etext = cstring_undefined; ret->exitCode = XK_NEVERESCAPE; ret->canBreak = FALSE; @@ -634,7 +637,7 @@ static /*@notnull@*/ /*@special@*/ exprNode ret->msets = sRefSet_undefined; ret->kind = XPR_EMPTY; - ret->sref = defref; + ret->sref = sRef_undefined; ret->etext = cstring_undefined; ret->exitCode = XK_NEVERESCAPE; ret->canBreak = FALSE; @@ -670,7 +673,13 @@ exprNode_isUnknownConstant (/*@notnull@*/ exprNode e) while (e->kind == XPR_PARENS) { e = exprData_getUopNode (e->edata); - llassert (exprNode_isDefined (e)); + + if (!exprNode_isDefined (e)) + { + return FALSE; + } + + /* evans 2002-02-05: was llassert (exprNode_isDefined (e)); but this can fail */ } if (e->kind == XPR_CONST) @@ -803,17 +812,17 @@ exprNode_combineLiterals (exprNode e, exprNode rest) exprNode_rawStringLiteral (/*@only@*/ cstring t, /*@only@*/ fileloc loc) { exprNode e = exprNode_createLoc (ctype_string, loc); - int len = cstring_length (t); + size_t len = cstring_length (t); if (context_getFlag (FLG_STRINGLITERALLEN)) { - if (len > context_getValue (FLG_STRINGLITERALLEN)) + if (len > size_fromInt (context_getValue (FLG_STRINGLITERALLEN))) { voptgenerror (FLG_STRINGLITERALLEN, message ("String literal length (%d) exceeds maximum " "length (%d): \"%s\"", - len, + size_toInt (len), context_getValue (FLG_STRINGLITERALLEN), t), e->loc); @@ -823,7 +832,7 @@ exprNode_rawStringLiteral (/*@only@*/ cstring t, /*@only@*/ fileloc loc) e->kind = XPR_STRINGLITERAL; e->val = multiVal_makeString (cstring_copy (t)); e->edata = exprData_makeLiteral (t); - e->sref = sRef_makeType (ctype_string); + e->sref = sRef_makeConst (ctype_string); if (context_getFlag (FLG_READONLYSTRINGS)) { @@ -838,15 +847,23 @@ exprNode_rawStringLiteral (/*@only@*/ cstring t, /*@only@*/ fileloc loc) return (e); /* s released */ } +/*@only@*/ exprNode +exprNode_wideStringLiteral (/*@only@*/ cstring t, /*@only@*/ fileloc loc) +{ + exprNode res = exprNode_stringLiteral (t, loc); + res->typ = ctype_makeWideString (); + return res; +} + /*@only@*/ exprNode exprNode_stringLiteral (/*@only@*/ cstring t, /*@only@*/ fileloc loc) { - int len = cstring_length (t) - 2; + size_t len = size_fromInt (cstring_length (t) - 2); char *ts = cstring_toCharsSafe (t); char *s = cstring_toCharsSafe (cstring_create (len + 1)); llassert (*ts == '\"' && *(ts + len + 1) == '\"'); - strncpy (s, ts+1, size_fromInt (len)); + strncpy (s, ts+1, len); *(s + len) = '\0'; cstring_free (t); return exprNode_rawStringLiteral (cstring_fromCharsO (s), loc); @@ -865,7 +882,7 @@ exprNode exprNode_fromUIO (cstring c) } e->loc = loc; /* save loc was mangled */ - e->sref = defref; + e->sref = sRef_undefined; if (usymtab_exists (c)) { @@ -921,12 +938,30 @@ exprNode exprNode_fromUIO (cstring c) return (e); } +exprNode exprNode_makeConstantString (cstring c, /*@only@*/ fileloc loc) +{ + exprNode e = exprNode_createPlain (ctype_unknown); + e->kind = XPR_VAR; + e->loc = loc; + e->sref = sRef_makeConst (ctype_string); + e->edata = exprData_makeId (uentry_makeUnrecognized (c, fileloc_copy (loc))); + e->typ = ctype_string; + + /* No alias errors for unrecognized identifiers */ + sRef_setAliasKind (e->sref, AK_STATIC, loc); + sRef_setExKind (e->sref, XO_OBSERVER, loc); + + return (e); +} + exprNode exprNode_createId (/*@observer@*/ uentry c) { if (uentry_isValid (c)) { exprNode e = exprNode_new (); - + + DPRINTF (("create id: %s", uentry_unparse (c))); + e->typ = uentry_getType (c); if (uentry_isFunction (c) @@ -946,7 +981,7 @@ exprNode exprNode_createId (/*@observer@*/ uentry c) /* ** yoikes! leaving this out was a heinous bug...that would have been - ** caught if i had lclint working first. gag! + ** caught if i had splint working first. gag! */ e->etext = cstring_undefined; @@ -976,14 +1011,13 @@ exprNode exprNode_createId (/*@observer@*/ uentry c) e->msets = sRefSet_new (); e->uses = sRefSet_new (); - /*> missing fields, detected by lclint <*/ + /*> missing fields, detected by splint <*/ e->exitCode = XK_NEVERESCAPE; e->isJumpPoint = FALSE; e->canBreak = FALSE; e->mustBreak = FALSE; - exprNode_defineConstraints(e); - + exprNode_defineConstraints (e); return e; } else @@ -1012,10 +1046,82 @@ exprNode_fromIdentifier (/*@observer@*/ uentry c) } ret = exprNode_fromIdentifierAux (c); - return ret; } +static void exprNode_checkStringLiteralLength (ctype t1, exprNode e2) +{ + multiVal mval = exprNode_getValue (e2); + cstring slit; + size_t len; + + if (ctype_isFixedArray (t1)) + { + size_t nelements = ctype_getArraySize (t1); + + llassert (multiVal_isString (mval)); + slit = multiVal_forceString (mval); + + len = cstring_lengthExpandEscapes (slit); + + llassert (exprNode_isDefined (e2)); + + if (len == nelements) + { + mstring temp; + + temp = cstring_expandEscapes (slit); + + if (temp[len-1] == '\0') + { + voptgenerror + (FLG_STRINGLITNOROOMFINALNULL, + message ("String literal with %d character%& " + "is assigned to %s (no room for final null terminator): %s", + len + 1, + ctype_unparse (t1), + exprNode_unparse (e2)), + e2->loc); + } + else + { + voptgenerror + (FLG_STRINGLITNOROOM, + message ("String literal with %d character%& " + "is assigned to %s (no room for null terminator): %s", + len + 1, + ctype_unparse (t1), + exprNode_unparse (e2)), + e2->loc); + } + } + else if (len > nelements) + { + voptgenerror + (FLG_STRINGLITTOOLONG, + message ("String literal with %d character%& (counting null terminator) " + "is assigned to %s (insufficient storage available): %s", + len + 1, + ctype_unparse (t1), + exprNode_unparse (e2)), + e2->loc); + } + else if (len < nelements - 1) + { + voptgenerror + (FLG_STRINGLITSMALLER, + message ("String literal with %d character%& is assigned to %s (possible waste of storage): %s", + len + 1, + ctype_unparse (t1), + exprNode_unparse (e2)), + e2->loc); + } + else + { + ; /* okay */ + } + } +} static /*@only@*/ /*@notnull@*/ exprNode exprNode_fromIdentifierAux (/*@observer@*/ uentry c) @@ -1060,6 +1166,16 @@ exprNode_isNonNegative (exprNode e) { return (multiVal_forceInt (m) >= 0); } + + /* + ** This is not always true if programmer defines enum + ** values, but then the constant should be known. + */ + + if (ctype_isEnum (ctype_realType (e->typ))) + { + return TRUE; + } } return FALSE; @@ -1082,6 +1198,9 @@ exprNode_arrayFetch (/*@only@*/ exprNode e1, /*@only@*/ exprNode e2) ** error in ind, assume valid and continue */ + DPRINTF (("Array fetch: %s / %s", + exprNode_unparse (e1), exprNode_unparse (e2))); + if (exprNode_isError (e1)) { exprNode_free (e2); @@ -1096,10 +1215,12 @@ exprNode_arrayFetch (/*@only@*/ exprNode e1, /*@only@*/ exprNode e2) /* ** this sets up funny aliasing, that leads to spurious - ** lclint errors. Hence, the i2 comments. + ** splint errors. Hence, the i2 comments. */ - if (!ctype_isRealArray (crarr) + /* evans 2001-09-09 added ctype_isKnown so there is no swap when e1 type is unknown */ + if (ctype_isKnown (crarr) + && !ctype_isRealArray (crarr) && ctype_isRealNumeric (crarr) && !exprNode_isError (e2) && ctype_isRealAP (exprNode_getType (e2))) /* fetch like 3[a] */ @@ -1116,6 +1237,8 @@ exprNode_arrayFetch (/*@only@*/ exprNode e1, /*@only@*/ exprNode e2) ind = e2; } + DPRINTF (("arr: %s", exprNode_unparse (arr))); + if (sRef_possiblyNull (arr->sref)) { if (!usymtab_isGuarded (arr->sref)) @@ -1127,6 +1250,7 @@ exprNode_arrayFetch (/*@only@*/ exprNode e1, /*@only@*/ exprNode e2) exprNode_unparse (arr)), arr->loc)) { + DPRINTF (("ref: %s", sRef_unparseFull (arr->sref))); sRef_showNullInfo (arr->sref); /* suppress future messages */ @@ -1489,7 +1613,14 @@ checkPrintfArgs (/*@notnull@*/ /*@dependent@*/ exprNode f, uentry fcn, /*@switchbreak@*/ break; case 'c': /* int converted to char (check its a char?) */ - expecttype = ctype_makeConj (ctype_char, ctype_uchar); + expecttype = ctype_makeConj (ctype_int, + ctype_makeConj (ctype_char, + ctype_uchar)); + /*@i231@*/ + /* evans 2001-10-05 - changed to reflect correct ISO spec: + int converted to char */ + + /* expecttype = ctype_makeConj (ctype_char, ctype_uchar); */ /*@switchbreak@*/ break; case 's': /* string */ @@ -1516,8 +1647,11 @@ checkPrintfArgs (/*@notnull@*/ /*@dependent@*/ exprNode f, uentry fcn, case 'p': /* pointer */ expecttype = ctype_makePointer (ctype_void); - uentry_setDefState (regArg, SS_RELDEF); /* need not be defined */ - sRef_setPosNull (uentry_getSref (regArg), fileloc_undefined); /* could be null */ + /* need not be defined */ + uentry_setDefState (regArg, SS_RELDEF); + sRef_setPosNull (uentry_getSref (regArg), + fileloc_undefined); + /* could be null */ /*@switchbreak@*/ break; case 'n': /* pointer to int, modified by call! */ @@ -1910,7 +2044,7 @@ checkScanfArgs (/*@notnull@*/ /*@dependent@*/ exprNode f, uentry fcn, } else { - /* a->sref = defref; */ + /* a->sref = sRef_undefined; */ } } } @@ -2050,6 +2184,14 @@ checkMessageArgs (/*@notnull@*/ /*@dependent@*/ exprNode f, case 'f': expecttype = ctype_float; break; case 'b': expecttype = ctype_bool; break; case 't': expecttype = ctypeType; break; + case 'p': + expecttype = ctype_makePointer (ctype_void); + /* need not be defined */ + uentry_setDefState (regArg, SS_RELDEF); + sRef_setPosNull (uentry_getSref (regArg), + fileloc_undefined); + /* could be null */ + /*@switchbreak@*/ break; case 'l': expecttype = filelocType; break; case '&': /* a wee bit of a hack methinks */ expecttype = ctype_int; @@ -2283,8 +2425,10 @@ static void checkExpressionDefined (exprNode e1, exprNode e2, lltok op) hasError = optgenerror (FLG_EVALORDER, message ("Expression has undefined behavior " - "(value of left operand is modified " - "by right operand): %s %s %s", + "(value of left operand %s is modified " + "by right operand %s): %s %s %s", + exprNode_unparse (e1), + exprNode_unparse (e2), exprNode_unparse (e1), lltok_unparse (op), exprNode_unparse (e2)), e2->loc); @@ -3030,7 +3174,7 @@ checkGlobMods (/*@notnull@*/ /*@dependent@*/ exprNode f, if (freshMods) { /* - ** Spurious errors reported, because lclint can't tell + ** Spurious errors reported, because splint can't tell ** mods must be fresh if freshMods is true. */ @@ -3084,7 +3228,7 @@ void checkGlobUse (uentry glob, bool isCall, /*@notnull@*/ exprNode e) } static void -reflectEnsuresClause (uentry le, exprNode f, exprNodeList args) +reflectEnsuresClause (exprNode ret, uentry le, exprNode f, exprNodeList args) { DPRINTF (("Reflect ensures clause: %s(%s) / %s / %s", exprNode_unparse (f), exprNodeList_unparse (args), @@ -3138,16 +3282,17 @@ reflectEnsuresClause (uentry le, exprNode f, exprNodeList args) if (sRef_isResult (sRef_getRootBase (sel))) { - ; /*@i423 what do we do about results */ + s = exprNode_getSref (ret); } else { s = sRef_fixBaseParam (sel, args); - DPRINTF (("Reflecting state clause on: %s / %s", - sRef_unparse (sel), sRef_unparse (s))); - - sRef_setMetaStateValueComplete (s, key, mvalue, exprNode_loc (f)); } + + DPRINTF (("Reflecting state clause on: %s / %s", + sRef_unparse (sel), sRef_unparse (s))); + + sRef_setMetaStateValueComplete (s, key, mvalue, exprNode_loc (f)); } end_sRefSet_elements; sRefSet_free (osrs); @@ -3157,7 +3302,9 @@ reflectEnsuresClause (uentry le, exprNode f, exprNodeList args) sRefSet srs = stateClause_getRefs (cl); sRefModVal modf = stateClause_getEnsuresFunction (cl); int eparam = stateClause_getStateParameter (cl); - + + llassert (modf != NULL); + DPRINTF (("Reflect after clause: %s / %s", stateClause_unparse (cl), sRefSet_unparse (srs))); @@ -3171,25 +3318,259 @@ reflectEnsuresClause (uentry le, exprNode f, exprNodeList args) if (sRef_isResult (sRef_getRootBase (sel))) { - ; /*@i423 what do we do about results */ + DPRINTF (("Fix base: %s / %s", + sRef_unparse (sel), sRef_unparse (exprNode_getSref (ret)))); + s = sRef_fixBase (sel, exprNode_getSref (ret)); + DPRINTF (("==> %s", sRef_unparseFull (s))); } else { s = sRef_fixBaseParam (sel, args); + } + + DPRINTF (("elements: %s", sRef_unparse (s))); + DPRINTF (("elements: %s", sRef_unparseFull (s))); + + DPRINTF (("Reflecting state clause on: %s / %s", + sRef_unparseFull (sel), sRef_unparseFull (s))); + + /* evans 2001-08-24 - added aliasSetCompleteParam */ + sRef_aliasSetCompleteParam (modf, s, eparam, exprNode_loc (f)); + + DPRINTF (("After reflecting state clause on: %s / %s", + sRef_unparseFull (sel), sRef_unparseFull (s))); + } end_sRefSet_elements; + } + } + } end_stateClauseList_elements ; + } + + DPRINTF (("Here: %s / %s", + uentry_unparseFull (le), + bool_unparse (uentry_hasMetaStateEnsures (le)))); + + if (uentry_hasMetaStateEnsures (le)) + { + fileloc loc = exprNode_loc (f); + + metaStateConstraintList mscl = uentry_getMetaStateEnsures (le); + + metaStateConstraintList_elements (mscl, msc) + { + metaStateSpecifier msspec = metaStateConstraint_getSpecifier (msc); + metaStateInfo msinfo = metaStateSpecifier_getMetaStateInfo (msspec); + metaStateExpression msexpr = metaStateConstraint_getExpression (msc); + cstring key = metaStateInfo_getName (msinfo); + sRef mlsr = metaStateSpecifier_getSref (msspec); + sRef s; + sRef lastref = sRef_undefined; + stateValue sval = stateValue_undefined; + + DPRINTF (("Meta state constraint for %s: %s", uentry_unparse (le), + metaStateConstraint_unparse (msc))); + DPRINTF (("Matches left: %s", sRef_unparseDebug (mlsr))); + + if (sRef_isResult (sRef_getRootBase (mlsr))) + { + s = exprNode_getSref (ret); + } + else + { + s = sRef_fixBaseParam (mlsr, args); + } + + DPRINTF (("Setting state: %s", sRef_unparseFull (s))); + + while (metaStateExpression_isDefined (msexpr)) + { + metaStateSpecifier ms = metaStateExpression_getSpecifier (msexpr); + metaStateInfo msi = metaStateSpecifier_getMetaStateInfo (ms); + sRef msr, fs; + + DPRINTF (("Check expression: %s", metaStateExpression_unparse (msexpr))); + + if (metaStateExpression_isMerge (msexpr)) + { + msexpr = metaStateExpression_getRest (msexpr); + } + else + { + msexpr = metaStateExpression_undefined; + } + + if (metaStateInfo_isDefined (msi)) + { + /* Must match lhs state */ + llassert (metaStateInfo_equal (msinfo, msi)); + } + + if (metaStateSpecifier_isElipsis (ms)) + { + /* + ** For elipsis, we need to merge all the relevant elipsis parameters + ** + */ + + uentryList params = uentry_getParams (le); + int paramno = uentryList_size (params) - 1; + + if (!uentry_isElipsisMarker (uentryList_getN (params, paramno))) + { + voptgenerror + (FLG_TYPE, + message ("Ensures clauses uses ... for function without ... in parameter list: %q", + uentry_getName (le)), + uentry_whereLast (le)); + /*@innerbreak@*/ break; + } + + while (paramno < exprNodeList_size (args)) + { + exprNode arg = exprNodeList_getN (args, paramno); + fs = exprNode_getSref (arg); + DPRINTF (("Merge arg: %s", exprNode_unparse (arg))); + + /* cut and pasted... gack*/ + if (stateValue_isDefined (sval)) + { + /* Use combination table to merge old state value with new one: */ + stateValue tval = sRef_getMetaStateValue (fs, key); - DPRINTF (("elements: %s", sRef_unparse (s))); - DPRINTF (("elements: %s", sRef_unparseFull (s))); + if (stateValue_isDefined (tval)) + { + stateCombinationTable sctable = metaStateInfo_getMergeTable (msinfo); + cstring msg = cstring_undefined; + int nval = stateCombinationTable_lookup (sctable, + stateValue_getValue (sval), + stateValue_getValue (tval), + &msg); + DPRINTF (("Combining: %s + %s -> %d", + stateValue_unparseValue (sval, msinfo), + stateValue_unparseValue (tval, msinfo), + nval)); + + if (nval == stateValue_error) + { + if (optgenerror + (FLG_STATEMERGE, + message + ("Attributes merged in ensures clause in states that " + "cannot be combined (%q is %q, %q is %q)%q", + sRef_unparse (lastref), + stateValue_unparseValue (sval, msinfo), + sRef_unparse (fs), + stateValue_unparseValue (tval, msinfo), + cstring_isDefined (msg) ? + message (": %s", msg) : cstring_undefined), + exprNode_loc (f))) + { + sRef_showMetaStateInfo (fs, key); + } + } + + stateValue_updateValueLoc (sval, nval, fileloc_undefined); + loc = exprNode_loc (arg); + } + else + { + DPRINTF (("No value for: %s:%s", sRef_unparse (fs), key)); + } + } + else + { + sval = sRef_getMetaStateValue (fs, key); + } + + lastref = fs; + + if (stateValue_isError (sval)) + { + /*@innerbreak@*/ break; /* Don't merge any more values if here was an error */ + } + + + paramno++; + } + } + else + { + msr = metaStateSpecifier_getSref (ms); + + + llassert (sRef_isParam (sRef_getRootBase (msr))); + fs = sRef_fixBaseParam (msr, args); + + if (stateValue_isDefined (sval)) + { + /* Use combination table to merge old state value with new one: */ + stateValue tval = sRef_getMetaStateValue (fs, key); + + if (stateValue_isDefined (tval)) + { + stateCombinationTable sctable = metaStateInfo_getMergeTable (msinfo); + cstring msg = cstring_undefined; + int nval = stateCombinationTable_lookup (sctable, + stateValue_getValue (sval), + stateValue_getValue (tval), + &msg); + DPRINTF (("Combining: %s + %s -> %d", + stateValue_unparseValue (sval, msinfo), + stateValue_unparseValue (tval, msinfo), + nval)); - DPRINTF (("Reflecting state clause on: %s / %s", - sRef_unparse (sel), sRef_unparse (s))); + if (nval == stateValue_error) + { + if (optgenerror + (FLG_STATEMERGE, + message + ("Attributes merged in ensures clause in states that " + "cannot be combined (%q is %q, %q is %q)%q", + sRef_unparse (lastref), + stateValue_unparseValue (sval, msinfo), + sRef_unparse (fs), + stateValue_unparseValue (tval, msinfo), + cstring_isDefined (msg) + ? message (": %s", msg) : cstring_undefined), + exprNode_loc (f))) + { + sRef_showMetaStateInfo (fs, key); + } + } - modf (s, eparam, exprNode_loc (f)); + stateValue_updateValueLoc (sval, nval, fileloc_undefined); } - } end_sRefSet_elements; + else + { + DPRINTF (("No value for: %s:%s", sRef_unparse (fs), key)); + } + } + else + { + sval = sRef_getMetaStateValue (fs, key); + } + + lastref = fs; + + if (stateValue_isError (sval)) + { + /*@innerbreak@*/ break; /* Don't merge any more values if here was an error */ + } } } - } end_stateClauseList_elements ; - + + DPRINTF (("Setting: %s:%s <- %s", sRef_unparse (s), key, stateValue_unparse (sval))); + + if (stateValue_isDefined (sval)) + { + sRef_setMetaStateValueComplete (s, key, stateValue_getValue (sval), loc); + } + else + { + DPRINTF (("Undefined state: %s", cstring_toCharsSafe (sRef_unparse (s)))); + } + } end_metaStateConstraintList_elements ; + + metaStateConstraintList_free (mscl); } } } @@ -3251,7 +3632,7 @@ checkRequiresClause (uentry le, exprNode f, exprNodeList args) if (sRef_isResult (sRef_getRootBase (sel))) { - ; /*@i423 what do we do about results */ + BADBRANCH; } else { @@ -3297,6 +3678,8 @@ checkRequiresClause (uentry le, exprNode f, exprNodeList args) stateClause_unparse (cl), sRefSet_unparse (srs))); + llassert (modf != NULL); + sRefSet_elements (srs, sel) { sRef s; @@ -3384,10 +3767,6 @@ functionCallSafe (/*@only@*/ /*@notnull@*/ exprNode f, checkRequiresClause (le, f, args); setCodePoint (); - DPRINTF (("Reflect: %s", uentry_unparseFull (le))); - reflectEnsuresClause (le, f, args); - setCodePoint (); - if (uentry_isValid (le) && (uentry_isFunction (le) || (uentry_isVariable (le) @@ -3397,11 +3776,12 @@ functionCallSafe (/*@only@*/ /*@notnull@*/ exprNode f, /* f->typ is already set to the return type */ + DPRINTF (("Function: %s", uentry_unparseFull (le))); ret->sref = uentry_returnedRef (le, args); DPRINTF (("Returned: %s / %s", uentry_unparseFull (le), sRef_unparseFull (ret->sref))); - + if (uentry_isFunction (le) && exprNodeList_size (args) >= 1) { qual nullPred = uentry_nullPred (le); @@ -3506,10 +3886,15 @@ functionCallSafe (/*@only@*/ /*@notnull@*/ exprNode f, } else { - ret->sref = defref; + ret->sref = sRef_undefined; exprNode_checkSetAny (ret, uentry_rawName (le)); } + DPRINTF (("Before reflect: %s", sRef_unparseFull (ret->sref))); + DPRINTF (("Reflect: %s", uentry_unparseFull (le))); + reflectEnsuresClause (ret, le, f, args); + setCodePoint (); + return (ret); } @@ -3517,8 +3902,7 @@ functionCallSafe (/*@only@*/ /*@notnull@*/ exprNode f, ** this is yucky! should keep the uentry as part of exprNode! */ -/*@observer@*/ uentry -exprNode_getUentry (exprNode e) +uentry exprNode_getUentry (exprNode e) { if (exprNode_isError (e)) { @@ -3533,6 +3917,19 @@ exprNode_getUentry (exprNode e) } } +/* +** Returns true iff e1 and e2 are both exactly the same storage +** (conservative). +*/ + +static bool exprNode_sameStorage (exprNode e1, exprNode e2) +{ + sRef s1 = exprNode_getSref (e1); + sRef s2 = exprNode_getSref (e2); + + return (sRef_realSame (s1, s2)); +} + exprNode exprNode_makeInitBlock (lltok brace, /*@only@*/ exprNodeList inits) { @@ -3550,7 +3947,9 @@ exprNode_functionCall (/*@only@*/ exprNode f, /*@only@*/ exprNodeList args) { ctype t; - setCodePoint (); +# ifdef DEBUGSPLINT + usymtab_checkAllValid (); +# endif if (exprNode_isUndefined (f)) { @@ -3729,7 +4128,7 @@ exprNode_fieldAccess (/*@only@*/ exprNode s, /*@only@*/ lltok dot, /*@only@*/ cstring f) { exprNode res = exprNode_fieldAccessAux (s, lltok_getLoc (dot), f); - lltok_release (dot); + lltok_free (dot); return res; } @@ -3933,7 +4332,7 @@ exprNode_arrowAccess (/*@only@*/ exprNode s, /*@only@*/ cstring f) { exprNode res = exprNode_arrowAccessAux (s, lltok_getLoc (arrow), f); - lltok_release (arrow); + lltok_free (arrow); return res; } @@ -4006,56 +4405,57 @@ exprNode_postOp (/*@only@*/ exprNode e, /*@only@*/ lltok op) /* added 7/11/2000 D.L */ /*@i223*/ - /*DRL 6/8/01 I decided to disable all LCLint Warning here since the code + /*DRL 6/8/01 I decided to disable all Splint warnings here since the code probably needs a rewrite any way */ + /*@i65234@*/ /*@ignore@*/ - // updateEnvironmentForPostOp (e); - - /* start modifications */ - /* added by Seejo on 4/16/2000 */ - - /* Arithmetic operations on pointers wil modify the size/len/null terminated - status */ - if ((sRef_isPossiblyNullTerminated (e->sref)) || (sRef_isNullTerminated(e->sref))) { - - ret->sref = sRef_copy (e->sref); - - /* Operator : ++ */ - if (lltok_getTok (op) == INC_OP) { - if (sRef_getSize(e->sref) > 0) { - - sRef_setSize (ret->sref, sRef_getSize(e->sref) - 1); - - if (sRef_getLen(e->sref) == 1) { /* i.e. the first character is \0 */ - /* Assumption: there is only 1 \0 in the buffer */ - /* This will not be correct if there are 2 \0's in the buffer */ - sRef_setNotNullTerminatedState(ret->sref); - sRef_resetLen(ret->sref); - } else { - sRef_setNullTerminatedState(ret->sref); - sRef_setLen (ret->sref, sRef_getLen(e->sref) - 1); - } - if (sRef_isNullTerminated (ret->sref)) - printf ("ret->sref is Null Terminated\n"); - else if (sRef_isPossiblyNullTerminated (ret->sref)) - printf ("ret->sref is Possibly Null Terminated\n"); - else if (sRef_isNotNullTerminated (ret->sref)) - printf ("ret->sref is Not Null Terminated\n"); - } - } - - /* Operator : -- */ - if (lltok_getTok (op) == DEC_OP) { - if (sRef_getSize(e->sref) >= 0) { - sRef_setSize (ret->sref, sRef_getSize(e->sref) + 1); - sRef_setLen (ret->sref, sRef_getLen(e->sref) + 1); - } - } - } - /*@end@*/ - /* end modifications */ + /* updateEnvironmentForPostOp (e); */ + + /* start modifications */ + /* added by Seejo on 4/16/2000 */ + + /* Arithmetic operations on pointers wil modify the size/len/null terminated + status */ + if ((sRef_isPossiblyNullTerminated (e->sref)) || (sRef_isNullTerminated(e->sref))) { + + ret->sref = sRef_copy (e->sref); + + /* Operator : ++ */ + if (lltok_getTok (op) == INC_OP) { + if (sRef_getSize(e->sref) > 0) { + + sRef_setSize (ret->sref, sRef_getSize(e->sref) - 1); + + if (sRef_getLen(e->sref) == 1) { /* i.e. the first character is \0 */ + /* Assumption: there is only 1 \0 in the buffer */ + /* This will not be correct if there are 2 \0's in the buffer */ + sRef_setNotNullTerminatedState(ret->sref); + sRef_resetLen(ret->sref); + } else { + sRef_setNullTerminatedState(ret->sref); + sRef_setLen (ret->sref, sRef_getLen(e->sref) - 1); + } + if (sRef_isNullTerminated (ret->sref)) + printf ("ret->sref is Null Terminated\n"); + else if (sRef_isPossiblyNullTerminated (ret->sref)) + printf ("ret->sref is Possibly Null Terminated\n"); + else if (sRef_isNotNullTerminated (ret->sref)) + printf ("ret->sref is Not Null Terminated\n"); + } + } + + /* Operator : -- */ + if (lltok_getTok (op) == DEC_OP) { + if (sRef_getSize(e->sref) >= 0) { + sRef_setSize (ret->sref, sRef_getSize(e->sref) + 1); + sRef_setLen (ret->sref, sRef_getLen(e->sref) + 1); + } + } + } + /*@end@*/ + /* end modifications */ return ret; } @@ -4317,8 +4717,11 @@ exprNode_preOp (/*@only@*/ exprNode e, /*@only@*/ lltok op) if (sRef_isKnown (e->sref)) { + DPRINTF (("Checking possibly null: %s", sRef_unparseFull (e->sref))); + if (sRef_possiblyNull (e->sref)) { + DPRINTF (("Checking possibly null: %s", sRef_unparse (e->sref))); if (!usymtab_isGuarded (e->sref) && !context_inProtectVars ()) { if (optgenerror @@ -4372,7 +4775,7 @@ ctype sizeof_resultType (void) } else { - sizet = ctype_ulint; + sizet = ctype_ulint; } } return sizet; @@ -4568,7 +4971,7 @@ exprNode_cast (/*@only@*/ lltok tok, /*@only@*/ exprNode e, /*@only@*/ qtype q) if (exprNode_isError (e)) { qtype_free (q); - lltok_release (tok); + lltok_free (tok); return exprNode_undefined; } @@ -4584,28 +4987,15 @@ exprNode_cast (/*@only@*/ lltok tok, /*@only@*/ exprNode e, /*@only@*/ qtype q) ret->kind = XPR_CAST; ret->edata = exprData_makeCast (tok, e, q); - if (ctype_isRealSU (ctype_getBaseType (sRef_getType (e->sref)))) + ret->sref = sRef_copy (e->sref); + + if (!sRef_isConst (e->sref)) { - /* - ** This is a bit of a hack to avoid a problem - ** when the code does, - ** (some other struct) x - ** ... - ** x->field - */ - - ret->sref = sRef_copy (e->sref); usymtab_addForceMustAlias (ret->sref, e->sref); - sRef_setTypeFull (ret->sref, c); - DPRINTF (("Cast: %s -> %s", sRef_unparseFull (e->sref), - sRef_unparseFull (ret->sref))); - } - else - { - ret->sref = e->sref; - sRef_setTypeFull (ret->sref, c); - DPRINTF (("Cast 2: -> %s", sRef_unparseFull (ret->sref))); } + + sRef_setTypeFull (ret->sref, c); + DPRINTF (("Cast 2: -> %s", sRef_unparseFull (ret->sref))); /* ** we allow @@ -4880,6 +5270,7 @@ exprNode_makeOp (/*@keep@*/ exprNode e1, /*@keep@*/ exprNode e2, } ret->val = multiVal_undefined; + ret->kind = XPR_OP; ret->edata = exprData_makeOp (e1, e2, op); @@ -4908,6 +5299,7 @@ exprNode_makeOp (/*@keep@*/ exprNode e1, /*@keep@*/ exprNode e2, tret = ctype_unknown; te1 = exprNode_getType (e1); + DPRINTF (("te1 = %s / %s", exprNode_unparse (e1), ctype_unparse (te1))); te2 = exprNode_getType (e2); @@ -4972,7 +5364,18 @@ exprNode_makeOp (/*@keep@*/ exprNode e1, /*@keep@*/ exprNode e2, case TDIV: /* */ case MUL_ASSIGN: /* numeric, numeric -> numeric */ case DIV_ASSIGN: /* */ - + + if (opid == TMULT || opid == MUL_ASSIGN) + { + ret->val = multiVal_multiply (exprNode_getValue (e1), + exprNode_getValue (e2)); + } + else + { + ret->val = multiVal_divide (exprNode_getValue (e1), + exprNode_getValue (e2)); + } + tret = checkNumerics (tr1, tr2, te1, te2, e1, e2, op); break; @@ -4980,7 +5383,18 @@ exprNode_makeOp (/*@keep@*/ exprNode e1, /*@keep@*/ exprNode e2, case TMINUS: /* pointer, int -> pointer */ case SUB_ASSIGN: /* int, pointer -> pointer */ case ADD_ASSIGN: /* numeric, numeric -> numeric */ - + + if (opid == TPLUS || opid == ADD_ASSIGN) + { + ret->val = multiVal_add (exprNode_getValue (e1), + exprNode_getValue (e2)); + } + else + { + ret->val = multiVal_subtract (exprNode_getValue (e1), + exprNode_getValue (e2)); + } + tr1 = ctype_fixArrayPtr (tr1); if ((ctype_isRealPointer (tr1) && !exprNode_isNullValue (e1)) @@ -4997,6 +5411,20 @@ exprNode_makeOp (/*@keep@*/ exprNode e1, /*@keep@*/ exprNode e2, e1->loc); } + /* + ** Swap terms so e1 is always the pointer + */ + + if (ctype_isRealPointer (tr1)) + { + ; + } + else + { + exprNode_swap (e1, e2); + } + + if (sRef_possiblyNull (e1->sref) && !usymtab_isGuarded (e1->sref)) { @@ -5011,56 +5439,52 @@ exprNode_makeOp (/*@keep@*/ exprNode e1, /*@keep@*/ exprNode e2, ret->sref = sRef_copy (e1->sref); - /* start modifications */ - /* added by Seejo on 4/16/2000 */ - - /* Arithmetic operations on pointers wil modify the size/len/null terminated - status */ - if ((sRef_isPossiblyNullTerminated (e1->sref)) || (sRef_isNullTerminated(e1->sref))) { - //if (sRef_isKnown (e->sref)) { - //ret->sref = sRef_makeAddress (e->sref); - //} - - int val; - /*drl 1-4-2001 - added ugly fixed to stop - program from crashing on point + int +int - one day I'll fix this or ask Seejo wtf the codes supposed to do. */ - - if (!multiVal_isInt (e2->val) ) - break; - /*end drl*/ + /* start modifications */ + /* added by Seejo on 4/16/2000 */ + + /* Arithmetic operations on pointers wil modify the size/len/null terminated + status */ + if ((sRef_isPossiblyNullTerminated (e1->sref)) || (sRef_isNullTerminated(e1->sref))) { + int val; + /*drl 1-4-2002 + added ugly fixed to stop + program from crashing on point + int +int + one day I'll fix this or ask Seejo wtf the codes supposed to do. */ + + if (!multiVal_isInt (e2->val) ) + break; + /*end drl*/ + + val = (int) multiVal_forceInt (e2->val); + + /* Operator : + or += */ + if ((lltok_getTok (op) == TPLUS) || (lltok_getTok(op) == ADD_ASSIGN)) { + if (sRef_getSize(e1->sref) >= val) {/* Incrementing the pointer by + val should not result in a + size < 0 (size = 0 is ok !) */ + + sRef_setSize (ret->sref, sRef_getSize(e1->sref) - val); + + if (sRef_getLen(e1->sref) == val) { /* i.e. the character at posn val is \0 */ + sRef_setNotNullTerminatedState(ret->sref); + sRef_resetLen (ret->sref); + } else { + sRef_setNullTerminatedState(ret->sref); + sRef_setLen (ret->sref, sRef_getLen(e1->sref) - val); + } + } + } + + /* Operator : - or -= */ + if ((lltok_getTok (op) == TMINUS) || (lltok_getTok (op) == SUB_ASSIGN)) { + if (sRef_getSize(e1->sref) >= 0) { + sRef_setSize (ret->sref, sRef_getSize(e1->sref) + val); + sRef_setLen (ret->sref, sRef_getLen(e1->sref) + val); + } + } + } - val = (int) multiVal_forceInt (e2->val); - - /* Operator : + or += */ - if ((lltok_getTok (op) == TPLUS) || (lltok_getTok(op) == ADD_ASSIGN)) { - if (sRef_getSize(e1->sref) >= val) {/* Incrementing the pointer by - val should not result in a - size < 0 (size = 0 is ok !) */ - - sRef_setSize (ret->sref, sRef_getSize(e1->sref) - val); - - if (sRef_getLen(e1->sref) == val) { /* i.e. the character at posn val is \0 */ - sRef_setNotNullTerminatedState(ret->sref); - sRef_resetLen (ret->sref); - } else { - sRef_setNullTerminatedState(ret->sref); - sRef_setLen (ret->sref, sRef_getLen(e1->sref) - val); - } - } - } - - /* Operator : - or -= */ - if ((lltok_getTok (op) == TMINUS) || (lltok_getTok (op) == SUB_ASSIGN)) { - if (sRef_getSize(e1->sref) >= 0) { - sRef_setSize (ret->sref, sRef_getSize(e1->sref) + val); - sRef_setLen (ret->sref, sRef_getLen(e1->sref) + val); - } - } - } - - /* end modifications */ + /* end modifications */ sRef_setNullError (ret->sref); @@ -5104,61 +5528,56 @@ exprNode_makeOp (/*@keep@*/ exprNode e1, /*@keep@*/ exprNode e2, ret->sref = sRef_copy (e2->sref); - /* start modifications */ - /* added by Seejo on 4/16/2000 */ - - /* Arithmetic operations on pointers wil modify the size/len/null terminated - status */ - - if ((sRef_isPossiblyNullTerminated (e2->sref)) || (sRef_isNullTerminated(e2->sref))) { - //if (sRef_isKnown (e->sref)) { - //ret->sref = sRef_makeAddress (e->sref); - //} - - int val = (int) multiVal_forceInt (e1->val); - - /* Operator : + or += */ - if ((lltok_getTok (op) == TPLUS) || (lltok_getTok(op) == ADD_ASSIGN)) { - if (sRef_getSize(e2->sref) >= val) {/* Incrementing the pointer by - val should not result in a - size < 0 (size = 0 is ok !) */ - - sRef_setSize (ret->sref, sRef_getSize(e2->sref) - val); - - if (sRef_getLen(e2->sref) == val) { /* i.e. the character at posn val is \0 */ - sRef_setNotNullTerminatedState(ret->sref); - sRef_resetLen (ret->sref); - } else { - sRef_setNullTerminatedState(ret->sref); - sRef_setLen (ret->sref, sRef_getLen(e2->sref) - val); - } - } - } - - /* Operator : - or -= */ - if ((lltok_getTok (op) == TMINUS) || (lltok_getTok (op) == SUB_ASSIGN)) { - if (sRef_getSize(e2->sref) >= 0) { - sRef_setSize (ret->sref, sRef_getSize(e2->sref) + val); - sRef_setLen (ret->sref, sRef_getLen(e2->sref) + val); - } - } - } - - /* end modifications */ - + /* start modifications */ + /* added by Seejo on 4/16/2000 */ + + /* Arithmetic operations on pointers wil modify the size/len/null terminated + status */ + + if ((sRef_isPossiblyNullTerminated (e2->sref)) || (sRef_isNullTerminated(e2->sref))) { + int val = (int) multiVal_forceInt (e1->val); + + /* Operator : + or += */ + if ((lltok_getTok (op) == TPLUS) || (lltok_getTok(op) == ADD_ASSIGN)) { + if (sRef_getSize(e2->sref) >= val) {/* Incrementing the pointer by + val should not result in a + size < 0 (size = 0 is ok !) */ + + sRef_setSize (ret->sref, sRef_getSize(e2->sref) - val); + + if (sRef_getLen(e2->sref) == val) { /* i.e. the character at posn val is \0 */ + sRef_setNotNullTerminatedState(ret->sref); + sRef_resetLen (ret->sref); + } else { + sRef_setNullTerminatedState(ret->sref); + sRef_setLen (ret->sref, sRef_getLen(e2->sref) - val); + } + } + } + + /* Operator : - or -= */ + if ((lltok_getTok (op) == TMINUS) || (lltok_getTok (op) == SUB_ASSIGN)) { + if (sRef_getSize(e2->sref) >= 0) { + sRef_setSize (ret->sref, sRef_getSize(e2->sref) + val); + sRef_setLen (ret->sref, sRef_getLen(e2->sref) + val); + } + } + } + /* end modifications */ + sRef_setNullError (ret->sref); - + /* ** Fixed for 2.2c: the alias state of ptr + int is dependent, ** since is points to storage that should not be deallocated ** through this pointer. */ - + if (sRef_isOnly (ret->sref) || sRef_isFresh (ret->sref)) { sRef_setAliasKind (ret->sref, AK_DEPENDENT, exprNode_loc (ret)); } - + tret = e2->typ; ret->sref = e2->sref; } @@ -5169,7 +5588,7 @@ exprNode_makeOp (/*@keep@*/ exprNode e1, /*@keep@*/ exprNode e2, break; - case LEFT_ASSIGN: /* Shifts: should be unsigned values */ + case LEFT_ASSIGN: case RIGHT_ASSIGN: case LEFT_OP: case RIGHT_OP: @@ -5181,47 +5600,80 @@ exprNode_makeOp (/*@keep@*/ exprNode e1, /*@keep@*/ exprNode e2, case OR_ASSIGN: { bool reported = FALSE; - flagcode code = FLG_BITWISEOPS; - if (opid == LEFT_OP || opid == LEFT_ASSIGN - || opid == RIGHT_OP || opid == RIGHT_ASSIGN) { - code = FLG_SHIFTSIGNED; - } + /* + ** Shift Operator + */ - if (!ctype_isUnsigned (tr1)) + if (opid == LEFT_OP || opid == LEFT_ASSIGN + || opid == RIGHT_OP || opid == RIGHT_ASSIGN) { - if (exprNode_isNonNegative (e1)) { - ; - } else { - reported = optgenerror - (code, - message ("Left operand of %s is not unsigned value (%t): %s", - lltok_unparse (op), te1, - exprNode_unparse (ret)), - e1->loc); - - if (reported) { - te1 = ctype_uint; + /* + ** evans 2002-01-01: fixed this to follow ISO 6.5.7. + */ + + if (!ctype_isUnsigned (tr2) + && !exprNode_isNonNegative (e2)) + { + reported = optgenerror + (FLG_SHIFTNEGATIVE, + message ("Right operand of %s may be negative (%t): %s", + lltok_unparse (op), te2, + exprNode_unparse (ret)), + e2->loc); } - } + + if (!ctype_isUnsigned (tr1) + && !exprNode_isNonNegative (e1)) + { + reported = optgenerror + (FLG_SHIFTIMPLEMENTATION, + message ("Left operand of %s may be negative (%t): %s", + lltok_unparse (op), te1, + exprNode_unparse (ret)), + e1->loc); + } + + /* + ** Should check size of right operand also... + */ + } - else + else { - /* right need not be signed for shifts */ - if (code != FLG_SHIFTSIGNED - && !ctype_isUnsigned (tr2)) + if (!ctype_isUnsigned (tr1)) { - if (!exprNode_isNonNegative (e2)) { + if (exprNode_isNonNegative (e1)) { + ; + } else { reported = optgenerror - (code, - message ("Right operand of %s is not unsigned value (%t): %s", - lltok_unparse (op), te2, + (FLG_BITWISEOPS, + message ("Left operand of %s is not unsigned value (%t): %s", + lltok_unparse (op), te1, exprNode_unparse (ret)), - e2->loc); + e1->loc); + + if (reported) { + te1 = ctype_uint; + } } } + else + { + if (!ctype_isUnsigned (tr2)) + { + if (!exprNode_isNonNegative (e2)) { + reported = optgenerror + (FLG_BITWISEOPS, + message ("Right operand of %s is not unsigned value (%t): %s", + lltok_unparse (op), te2, + exprNode_unparse (ret)), + e2->loc); + } + } + } } - + if (!reported) { if (!checkIntegral (e1, e2, ret, op)) { @@ -5250,6 +5702,10 @@ exprNode_makeOp (/*@keep@*/ exprNode e1, /*@keep@*/ exprNode e2, case NE_OP: case TLT: /* comparisons */ case TGT: /* numeric, numeric -> bool */ + + DPRINTF (("Here we go: %s / %s", + ctype_unparse (tr1), ctype_unparse (tr2))); + if ((ctype_isReal (tr1) && !ctype_isInt (tr1)) || (ctype_isReal (tr2) && !ctype_isInt (tr2))) { @@ -5318,6 +5774,9 @@ exprNode_makeOp (/*@keep@*/ exprNode e1, /*@keep@*/ exprNode e2, ** Types should match. */ + DPRINTF (("Match types: %s / %s", exprNode_unparse (e1), + exprNode_unparse (e2))); + if (!exprNode_matchTypes (e1, e2)) { hasError = gentypeerror @@ -5353,6 +5812,21 @@ exprNode_makeOp (/*@keep@*/ exprNode e1, /*@keep@*/ exprNode e2, tret = ctype_bool; } + /* certain comparisons on unsigned's and zero look suspicious */ + + if (opid == TLT || opid == LE_OP || opid == GE_OP) + { + if ((ctype_isUnsigned (tr1) && exprNode_isZero (e2)) + || (ctype_isUnsigned (tr2) && exprNode_isZero (e1))) + { + voptgenerror + (FLG_UNSIGNEDCOMPARE, + message ("Comparison of unsigned value involving zero: %s", + exprNode_unparse (ret)), + e1->loc); + } + } + /* EQ_OP should NOT be used with booleans (unless one is FALSE) */ if ((opid == EQ_OP || opid == NE_OP) && @@ -5449,7 +5923,7 @@ exprNode_makeOp (/*@keep@*/ exprNode e1, /*@keep@*/ exprNode e2, llfatalbug (cstring_makeLiteral ("There has been a problem in the parser. This is believed to result " - "from a problem with bison v. 1.25. Please try rebuidling LCLint " + "from a problem with bison v. 1.25. Please try rebuidling Splint " "using the pre-compiled grammar files by commenting out the " "BISON= line in the top-level Makefile.")); } @@ -5521,11 +5995,11 @@ void exprNode_checkAssignMod (exprNode e1, exprNode ret) } exprNode -exprNode_assign (/*@only@*/ exprNode e1, - /*@only@*/ exprNode e2, /*@only@*/ lltok op) +exprNode_assign (/*@only@*/ exprNode e1, /*@only@*/ exprNode e2, /*@only@*/ lltok op) { bool isalloc = FALSE; bool isjustalloc = FALSE; + bool noalias = FALSE; exprNode ret; DPRINTF (("%s [%s] <- %s [%s]", @@ -5537,7 +6011,22 @@ exprNode_assign (/*@only@*/ exprNode e1, if (lltok_getTok (op) != TASSIGN) { ret = exprNode_makeOp (e1, e2, op); - } + + DPRINTF (("Here goes: %s %s", + ctype_unparse (e1->typ), + ctype_unparse (e2->typ))); + + if (exprNode_isDefined (e1) + && exprNode_isDefined (e2)) + { + if (ctype_isNumeric (e2->typ) + || ctype_isNumeric (e1->typ)) + { + /* Its a pointer arithmetic expression like ptr += i */ + noalias = TRUE; + } + } + } else { ret = exprNode_createPartialCopy (e1); @@ -5621,6 +6110,8 @@ exprNode_assign (/*@only@*/ exprNode e1, sRef_unparse (e1->sref)), g_currentloc); } + + exprNode_checkAssignMod (e1, ret); /* evans 2001-07-22 */ } } else @@ -5635,7 +6126,17 @@ exprNode_assign (/*@only@*/ exprNode e1, ctype te1 = exprNode_getType (e1); ctype te2 = exprNode_getType (e2); - if (!ctype_forceMatch (te1, te2)) + if (ctype_isVoid (te2)) + { + (void) gentypeerror + (te2, e2, te1, e1, + message ("Assignment of void value to %t: %s %s %s", + te1, exprNode_unparse (e1), + lltok_unparse (op), + exprNode_unparse (e2)), + e1->loc); + } + else if (!ctype_forceMatch (te1, te2)) { if (exprNode_matchLiteral (te1, e2)) { @@ -5652,12 +6153,25 @@ exprNode_assign (/*@only@*/ exprNode e1, e1->loc); } } + else + { + /* Type checks okay */ + } } exprNode_mergeUSs (ret, e2); exprNode_checkUse (ret, e2->sref, e2->loc); - doAssign (e1, e2, FALSE); + DPRINTF (("Do assign! %s %s", exprNode_unparse (e1), exprNode_unparse (e2))); + if (noalias) + { + ; + } + else + { + doAssign (e1, e2, FALSE); + } + ret->sref = e1->sref; } else @@ -5665,7 +6179,7 @@ exprNode_assign (/*@only@*/ exprNode e1, if (exprNode_isDefined (e2)) { exprNode_mergeUSs (ret, e2); - exprNode_checkUse (ret, e2->sref, e2->loc); + exprNode_checkUse (ret, e2->sref, e2->loc); } } @@ -5691,11 +6205,11 @@ exprNode_assign (/*@only@*/ exprNode e1, /* ** be careful! this defines e1->sref. */ - - if (!sRef_isMacroParamRef (e1->sref)) - { - exprNode_checkSet (ret, e1->sref); - } + + /* evans 2001-07-22: removed if (!sRef_isMacroParamRef (e1->sref)) */ + + DPRINTF (("Setting: %s -> %s", exprNode_unparse (ret), sRef_unparse (e1->sref))); + exprNode_checkSet (ret, e1->sref); if (isjustalloc) { @@ -5846,7 +6360,7 @@ exprNode_cond (/*@keep@*/ exprNode pred, /*@keep@*/ exprNode ifclause, } else /* all errors! */ { - ret = exprNode_createLoc (ctype_unknown, g_currentloc); + ret = exprNode_createLoc (ctype_unknown, fileloc_copy (g_currentloc)); } } @@ -6052,6 +6566,7 @@ exprNode_mustBreak (exprNode e) { return e->mustBreak; } + return FALSE; } @@ -6174,7 +6689,7 @@ exprNode exprNode_concat (/*@only@*/ exprNode e1, /*@only@*/ exprNode e2) { voptgenerror (FLG_CASEBREAK, cstring_makeLiteral - ("Fall through case (no preceeding break)"), + ("Fall through case (no preceding break)"), e2->loc); } } @@ -6190,6 +6705,7 @@ exprNode exprNode_concat (/*@only@*/ exprNode e1, /*@only@*/ exprNode e2) usymtab_setMustBreak (); } + DPRINTF (("==> %s", exprNode_unparse (ret))); return ret; } @@ -6206,7 +6722,7 @@ exprNode exprNode_statement (/*@only@*/ exprNode e, /*@only@*/ lltok t) { if (!exprNode_isError (e)) { - exprNode_checkStatement(e); + exprChecks_checkStatementEffect(e); } return (exprNode_statementError (e, t)); @@ -6261,6 +6777,36 @@ void exprNode_produceGuards (exprNode pred) } } +exprNode exprNode_compoundStatementExpression (/*@only@*/ lltok tlparen, /*@only@*/ exprNode e) +{ + exprNode laststmt; + + DPRINTF (("Compound: %s", exprNode_unparse (e))); + + if (!context_flagOn (FLG_GNUEXTENSIONS, exprNode_loc (e))) + { + (void) llgenhinterror + (FLG_SYNTAX, + message ("Compound statement expressions is not supported by ISO C99"), + message ("Use +gnuextensions to allow compound statement expressions (and other GNU language extensions) " + "without this warning"), + exprNode_loc (e)); + } + + /* + ** The type of a compoundStatementExpression is the type of the last statement + */ + + llassert (exprNode_isBlock (e)); + laststmt = exprNode_lastStatement (e); + + DPRINTF (("Last statement: %s / %s", exprNode_unparse (laststmt), ctype_unparse (exprNode_getType (laststmt)))); + DPRINTF (("e: %s", exprNode_unparse (e))); + e->typ = exprNode_getType (laststmt); + return exprNode_addParens (tlparen, e); +} + + exprNode exprNode_makeBlock (/*@only@*/ exprNode e) { exprNode ret = exprNode_createPartialCopy (e); @@ -6272,8 +6818,10 @@ exprNode exprNode_makeBlock (/*@only@*/ exprNode e) ret->mustBreak = e->mustBreak; } + DPRINTF (("Block e: %s", exprNode_unparse (e))); ret->edata = exprData_makeSingle (e); ret->kind = XPR_BLOCK; + DPRINTF (("Block: %s", exprNode_unparse (ret))); return ret; } @@ -6282,6 +6830,12 @@ bool exprNode_isBlock (exprNode e) return (exprNode_isDefined (e) && ((e)->kind == XPR_BLOCK)); } + +bool exprNode_isStatement (exprNode e) +{ + return (exprNode_isDefined (e) + && ((e)->kind == XPR_STMT)); +} bool exprNode_isAssign (exprNode e) { @@ -6300,6 +6854,27 @@ bool exprNode_isEmptyStatement (exprNode e) && (lltok_isSemi (exprData_getTok (e->edata)))); } +bool exprNode_isMultiStatement (exprNode e) +{ + return (exprNode_isDefined (e) + && ((e->kind == XPR_FOR) + || (e->kind == XPR_FORPRED) + || (e->kind == XPR_IF) + || (e->kind == XPR_IFELSE) + || (e->kind == XPR_WHILE) + || (e->kind == XPR_WHILEPRED) + || (e->kind == XPR_DOWHILE) + || (e->kind == XPR_BLOCK) + || (e->kind == XPR_STMT) + || (e->kind == XPR_STMTLIST) + || (e->kind == XPR_SWITCH))); +} + +void exprNode_checkIfPred (exprNode pred) +{ + exprNode_checkPred (cstring_makeLiteralTemp ("if"), pred); +} + exprNode exprNode_if (/*@only@*/ exprNode pred, /*@only@*/ exprNode tclause) { exprNode ret; @@ -6333,7 +6908,7 @@ exprNode exprNode_if (/*@only@*/ exprNode pred, /*@only@*/ exprNode tclause) { if (exprNode_isError (tclause)) { - ret = exprNode_createLoc (ctype_unknown, g_currentloc); + ret = exprNode_createLoc (ctype_unknown, fileloc_copy (g_currentloc)); } else { @@ -6349,8 +6924,8 @@ exprNode exprNode_if (/*@only@*/ exprNode pred, /*@only@*/ exprNode tclause) message ("Predicate always exits: %s", exprNode_unparse (pred)), exprNode_loc (pred)); } - - exprNode_checkPred (cstring_makeLiteralTemp ("if"), pred); + + /*! exprNode_checkPred (cstring_makeLiteralTemp ("if"), pred); */ /*@i523@*/ exprNode_checkUse (pred, pred->sref, pred->loc); if (!exprNode_isError (tclause)) @@ -6455,7 +7030,7 @@ exprNode exprNode_ifelse (/*@only@*/ exprNode pred, { if (exprNode_isError (eclause)) { - ret = exprNode_createLoc (ctype_unknown, g_currentloc); + ret = exprNode_createLoc (ctype_unknown, fileloc_copy (g_currentloc)); } else { @@ -6479,7 +7054,7 @@ exprNode exprNode_ifelse (/*@only@*/ exprNode pred, exprNode_loc (pred)); } - exprNode_checkPred (cstring_makeLiteralTemp ("if"), pred); + /*@i3423 exprNode_checkPred (cstring_makeLiteralTemp ("if"), pred);*/ exprNode_checkUse (ret, pred->sref, pred->loc); exprNode_mergeCondUSs (ret, tclause, eclause); @@ -6534,6 +7109,9 @@ checkSwitchExpr (exprNode test, /*@dependent@*/ exprNode e, /*@out@*/ bool *allp exprNodeSList_elements (el, current) { + + DPRINTF ((message("checkSwitchExpr current = %s ", exprNode_unparse(current) ) )); + if (exprNode_isDefined (current)) { switch (current->kind) @@ -6543,7 +7121,7 @@ checkSwitchExpr (exprNode test, /*@dependent@*/ exprNode e, /*@out@*/ bool *allp if (hasDefault) { voptgenerror - (FLG_CONTROL, + (FLG_DUPLICATECASES, message ("Duplicate default cases in switch"), exprNode_loc (current)); } @@ -6571,7 +7149,7 @@ checkSwitchExpr (exprNode test, /*@dependent@*/ exprNode e, /*@out@*/ bool *allp (/*@-usedef@*/usedEnums/*@=usedef@*/, cname)) { voptgenerror - (FLG_CONTROL, + (FLG_DUPLICATECASES, message ("Duplicate case in switch: %s", cname), current->loc); @@ -6638,6 +7216,7 @@ checkSwitchExpr (exprNode test, /*@dependent@*/ exprNode e, /*@out@*/ bool *allp g_currentloc); enumNameSList_free (unused); + *allpaths = FALSE; /* evans 2002-01-01 */ } else { @@ -6859,7 +7438,7 @@ exprNode exprNode_while (/*@keep@*/ exprNode t, /*@keep@*/ exprNode b) { if (exprNode_isError (b)) { - ret = exprNode_createLoc (ctype_unknown, g_currentloc); + ret = exprNode_createLoc (ctype_unknown, fileloc_copy (g_currentloc)); } else { @@ -6904,7 +7483,7 @@ exprNode exprNode_while (/*@keep@*/ exprNode t, /*@keep@*/ exprNode b) if (exprNode_isDefined (t) && exprNode_mustEscape (t)) { voptgenerror - (FLG_CONTROL, + (FLG_ALWAYSEXITS, message ("Predicate always exits: %s", exprNode_unparse (t)), exprNode_loc (t)); } @@ -6950,12 +7529,15 @@ exprNode exprNode_while (/*@keep@*/ exprNode t, /*@keep@*/ exprNode b) exprNode exprNode_doWhile (/*@only@*/ exprNode b, /*@only@*/ exprNode t) { exprNode ret; - + + DPRINTF (("Do while: %s / %s", + exprNode_unparse (b), exprNode_unparse (t))); + if (exprNode_isError (t)) { if (exprNode_isError (b)) { - ret = exprNode_createLoc (ctype_unknown, g_currentloc); + ret = exprNode_createLoc (ctype_unknown, fileloc_copy (g_currentloc)); } else { @@ -6965,11 +7547,15 @@ exprNode exprNode_doWhile (/*@only@*/ exprNode b, /*@only@*/ exprNode t) exprNode_checkUse (ret, b->sref, b->loc); ret->exitCode = b->exitCode; ret->canBreak = b->canBreak; - ret->mustBreak = b->mustBreak; + ret->mustBreak = FALSE; } } else { + DPRINTF (("Do while: %s / %s", + exitkind_unparse (t->exitCode), + exitkind_unparse (b->exitCode))); + ret = exprNode_createPartialCopy (t); exprNode_checkPred (cstring_makeLiteralTemp ("while"), t); @@ -6990,9 +7576,16 @@ exprNode exprNode_doWhile (/*@only@*/ exprNode b, /*@only@*/ exprNode t) exprNode_mergeUSs (ret, t); exprNode_checkUse (ret, t->sref, t->loc); - ret->exitCode = b->exitCode; + /* evans 2001-10-05: while loop can break */ + ret->exitCode = exitkind_makeConditional (b->exitCode); + + DPRINTF (("Do while: %s", + exitkind_unparse (ret->exitCode))); + ret->canBreak = b->canBreak; - ret->mustBreak = b->mustBreak; + + /* Always FALSE for doWhile loops - break's when test is false */ + ret->mustBreak = FALSE; /* b->mustBreak; */ } } @@ -7000,7 +7593,78 @@ exprNode exprNode_doWhile (/*@only@*/ exprNode b, /*@only@*/ exprNode t) ret->kind = XPR_DOWHILE; ret->edata = exprData_makePair (t, b); - return ret; + return ret; +} + +bool exprNode_loopMustExec (exprNode forPred) +{ + /* + ** Returns true if it is obvious that the loop always executes at least once + ** + ** For now, we only identify the most obvious cases. Should be true anytime + ** we can prove init => !test. + */ + + if (exprNode_isDefined (forPred)) + { + exprNode init, test, inc; + exprData edata; + + llassert (forPred->kind == XPR_FORPRED); + + edata = forPred->edata; + init = exprData_getTripleInit (edata); + test = exprData_getTripleTest (edata); + inc = exprData_getTripleInc (edata); + + if (exprNode_isAssign (init)) + { + exprNode loopVar = exprData_getOpA (init->edata); + exprNode loopInit = exprData_getOpB (init->edata); + + if (exprNode_isDefined (test) && test->kind == XPR_OP) + { + exprNode testVar = exprData_getOpA (test->edata); + exprNode testVal = exprData_getOpB (test->edata); + lltok comp = exprData_getOpTok (test->edata); + int opid = lltok_getTok (comp); + + DPRINTF (("Same storage: %s / %s", exprNode_unparse (loopVar), + exprNode_unparse (testVar))); + + if (exprNode_sameStorage (loopVar, testVar)) + { + multiVal valinit = exprNode_getValue (loopInit); + multiVal valtest = exprNode_getValue (testVal); + + DPRINTF (("Values: %s / %s", multiVal_unparse (valinit), + multiVal_unparse (valtest))); + + if (multiVal_isInt (valinit) && multiVal_isInt (valtest)) + { + long v1 = multiVal_forceInt (valinit); + long v2 = multiVal_forceInt (valtest); + + DPRINTF (("Here: %ld %ld", v1, v2)); + + if ((opid == EQ_OP && v1 < v2) + || (opid == NE_OP && v1 != v2) + || (opid == TLT && v1 <= v2) + || (opid == TGT && v1 >= v2) + || (opid == LE_OP && v1 < v2) + || (opid == GE_OP && v1 > v2)) + { + DPRINTF (("mustexec if inc")); + return TRUE; + } + } + } + } + } + } + + DPRINTF (("loop must exec: FALSE")); + return FALSE; } exprNode exprNode_for (/*@keep@*/ exprNode inc, /*@keep@*/ exprNode body) @@ -7056,14 +7720,13 @@ exprNode exprNode_for (/*@keep@*/ exprNode inc, /*@keep@*/ exprNode body) ret->exitCode = exitkind_makeConditional (body->exitCode); - exprNode_mergeUSs (inc, body); + exprNode_mergeUSs (inc, body); if (exprNode_isDefined (inc)) { exprNode tmp; context_setMessageAnnote (cstring_makeLiteral ("in post loop increment")); - tmp = exprNode_effect (exprData_getTripleInc (inc->edata)); exprNode_freeShallow (tmp); @@ -7435,7 +8098,7 @@ exprNode exprNode_comma (/*@only@*/ exprNode e1, /*@only@*/ exprNode e2) { if (exprNode_isError (e2)) { - ret = exprNode_createLoc (ctype_unknown, g_currentloc); + ret = exprNode_createLoc (ctype_unknown, fileloc_copy (g_currentloc)); } else { @@ -7514,6 +8177,10 @@ static bool exprNode_checkOneInit (/*@notnull@*/ exprNode el, exprNode val) ctype t2 = exprNode_getType (val); bool hasError = FALSE; + DPRINTF (("Check one init: %s / %s", + exprNode_unparse (el), + exprNode_unparse (val))); + if (ctype_isUnknown (t1)) { voptgenerror (FLG_IMPTYPE, @@ -7528,12 +8195,44 @@ static bool exprNode_checkOneInit (/*@notnull@*/ exprNode el, exprNode val) if (exprNode_isDefined (val) && val->kind == XPR_INITBLOCK) { exprNodeList vals = exprData_getArgs (val->edata); + + DPRINTF (("Check one init: %s", exprNodeList_unparse (vals))); + DPRINTF (("Type: %s", ctype_unparse (t1))); if (ctype_isRealAP (t1)) { int i = 0; int nerrors = 0; + if (ctype_isFixedArray (t1)) + { + size_t nelements = ctype_getArraySize (t1); + + DPRINTF (("Checked array: %s / %d", + ctype_unparse (t1), nelements)); + + if (exprNode_isStringLiteral (val)) + { + exprNode_checkStringLiteralLength (t1, val); + } + else + { + if (exprNodeList_size (vals) != size_toInt (nelements)) + { + hasError = optgenerror + (exprNodeList_size (vals) > size_toInt (nelements) + ? FLG_INITSIZE : FLG_INITALLELEMENTS, + message ("Initializer block for " + "%s has %d element%&, but declared as %s: %q", + exprNode_unparse (el), + exprNodeList_size (vals), + ctype_unparse (t1), + exprNodeList_unparse (vals)), + val->loc); + } + } + } + exprNodeList_elements (vals, oneval) { cstring istring = message ("%d", i); @@ -7644,6 +8343,50 @@ static bool exprNode_checkOneInit (/*@notnull@*/ exprNode el, exprNode val) } end_exprNodeList_elements; } } + /* evans 2001-12-30: added to fix bug reported by Jim Zelenka */ + else if (ctype_isUnion (ctype_realType (t1))) + { + uentryList fields = ctype_getFields (t1); + int i = 0; + + /* + ** Union initializers set the first member always. + */ + + DPRINTF (("Union initializer: %s / %s", + exprNode_unparse (el), ctype_unparse (ctype_realType (t1)))); + + if (exprNodeList_size (vals) != 1) + { + hasError = optgenerror + (FLG_TYPE, + message ("Initializer block for union " + "%s has %d elements, union initializers should have one element: %q", + exprNode_unparse (el), + exprNodeList_size (vals), + exprNodeList_unparse (vals)), + val->loc); + } + else + { + exprNode oneval = exprNodeList_head (vals); + uentry thisfield = uentryList_getN (fields, i); + exprNode newel = + exprNode_fieldAccessAux (exprNode_fakeCopy (el), + exprNode_loc (el), + uentry_getName (thisfield)); + + if (exprNode_isDefined (newel)) + { + if (exprNode_checkOneInit (newel, oneval)) + { + hasError = TRUE; + } + + exprNode_freeIniter (newel); + } + } + } else { hasError = optgenerror @@ -7676,11 +8419,13 @@ static bool exprNode_checkOneInit (/*@notnull@*/ exprNode el, exprNode val) return hasError; } -static exprNode +static /*@notnull@*/ exprNode exprNode_makeInitializationAux (/*@temp@*/ idDecl t) { exprNode ret; + DPRINTF (("Initialization: %s", idDecl_unparse (t))); + if (usymtab_exists (idDecl_observeId (t))) { uentry ue = usymtab_lookup (idDecl_observeId (t)); @@ -7719,8 +8464,14 @@ exprNode_makeInitializationAux (/*@temp@*/ idDecl t) } else { - uentry ue = uentry_makeUnrecognized (idDecl_observeId (t), - g_currentloc); + uentry ue; + + DPRINTF (("Unrecognized: %s", idDecl_unparse (t))); + + ue = uentry_makeUnrecognized (idDecl_observeId (t), fileloc_copy (g_currentloc)); + /*!! fileloc_copy (g_currentloc)); */ + /*@i32!!! should get error without this */ + ret = exprNode_fromIdentifierAux (ue); /* @@ -7758,13 +8509,14 @@ exprNode exprNode_makeInitialization (/*@only@*/ idDecl t, exprNode ret = exprNode_makeInitializationAux (t); fileloc loc = exprNode_loc (e); + DPRINTF (("initialization: %s = %s", idDecl_unparse (t), exprNode_unparse (e))); + if (exprNode_isError (e)) { e = exprNode_createUnknown (); - idDecl_free (t); - /* error: assume initializer is defined */ sRef_setDefined (ret->sref, g_currentloc); + ret->edata = exprData_makeInit (t, e); } else { @@ -7780,6 +8532,7 @@ exprNode exprNode_makeInitialization (/*@only@*/ idDecl t, exprData_free (ret->edata, ret->kind); ret->edata = exprData_makeInit (t, e); + DPRINTF (("ret: %s", exprNode_unparse (ret))); exprNode_checkUse (ret, e->sref, e->loc); @@ -7795,7 +8548,7 @@ exprNode exprNode_makeInitialization (/*@only@*/ idDecl t, { sRef_setDefState (lhs->sref, SS_PARTIAL, fileloc_undefined); } - + (void) exprNode_checkOneInit (lhs, e); if (uentry_isStatic (ue)) @@ -7832,14 +8585,42 @@ exprNode exprNode_makeInitialization (/*@only@*/ idDecl t, sRef_setDefState (ret->sref, SS_PARTIAL, fileloc_undefined); } - doAssign (ret, e, TRUE); + if (exprNode_isStringLiteral (e) + && (ctype_isArray (ct)) + && (ctype_isChar (ctype_realType (ctype_baseArrayPtr (ct))))) + { + /* + ** If t is a char [], the literal is copied. + */ + + exprNode_checkStringLiteralLength (ct, e); + sRef_setDefState (ret->sref, SS_DEFINED, e->loc); + ret->val = multiVal_copy (e->val); + + sRef_setNullTerminatedState (ret->sref); + + if (multiVal_isDefined (e->val)) + { + cstring slit = multiVal_forceString (e->val); + sRef_setLen (ret->sref, cstring_length (slit) + 1); + } + + if (ctype_isFixedArray (ct)) + { + sRef_setSize (ret->sref, size_toInt (ctype_getArraySize (ct))); + } + } + else + { + doAssign (ret, e, TRUE); + } if (uentry_isStatic (ue)) { sRef_setDefState (ret->sref, SS_DEFINED, fileloc_undefined); } } - + if (context_inIterDef ()) { /* should check if it is yield */ @@ -7851,6 +8632,15 @@ exprNode exprNode_makeInitialization (/*@only@*/ idDecl t, } exprNode_mergeUSs (ret, e); + DPRINTF (("Ret: %s %p %p", + exprNode_unparse (ret), + ret->requiresConstraints, + ret->ensuresConstraints)); + + DPRINTF (("Ret: %s %s %s", + exprNode_unparse (ret), + constraintList_unparse (ret->requiresConstraints), + constraintList_unparse (ret->ensuresConstraints))); return ret; } @@ -7871,23 +8661,23 @@ exprNode exprNode_iter (/*@observer@*/ uentry name, if (uentry_isInvalid (end)) { - llerror (FLG_ITER, + llerror (FLG_ITERBALANCE, message ("Iter %s not balanced with end_%s", iname, iname)); } else { cstring ename = uentry_getName (end); - if (!cstring_equalPrefix (ename, "end_")) + if (!cstring_equalPrefixLit (ename, "end_")) { - llerror (FLG_ITER, message ("Iter %s not balanced with end_%s: %s", + llerror (FLG_ITERBALANCE, message ("Iter %s not balanced with end_%s: %s", iname, iname, ename)); } else { if (!cstring_equal (iname, cstring_suffix (ename, 4))) { - llerror (FLG_ITER, + llerror (FLG_ITERBALANCE, message ("Iter %s not balanced with end_%s: %s", iname, iname, ename)); } @@ -7934,11 +8724,11 @@ exprNode_iterNewId (/*@only@*/ cstring s) e->kind = XPR_VAR; e->val = multiVal_unknown (); e->guards = guardSet_new (); - e->sref = defref; + e->sref = sRef_undefined; e->isJumpPoint = FALSE; e->exitCode = XK_NEVERESCAPE; - /*> missing fields, detected by lclint <*/ + /*> missing fields, detected by splint <*/ e->canBreak = FALSE; e->mustBreak = FALSE; e->etext = cstring_undefined; @@ -8014,7 +8804,7 @@ exprNode_iterExpr (/*@returned@*/ exprNode e) if (fileloc_isDefined (e->loc)) { voptgenerror - (FLG_ITER, + (FLG_ITERYIELD, message ("Yield parameter is not simple identifier: %s", exprNode_unparse (e)), e->loc); @@ -8022,7 +8812,7 @@ exprNode_iterExpr (/*@returned@*/ exprNode e) else { voptgenerror - (FLG_ITER, + (FLG_ITERYIELD, message ("Yield parameter is not simple identifier: %s", exprNode_unparse (e)), g_currentloc); @@ -8065,7 +8855,7 @@ exprNode_iterId (/*@observer@*/ uentry c) if (!context_inHeader ()) { if (optgenerror - (FLG_ITER, + (FLG_ITERYIELD, message ("Yield parameter shadows local declaration: %q", uentry_getName (c)), fileloc_isDefined (e->loc) ? e->loc : g_currentloc)) @@ -8125,8 +8915,7 @@ exprNode exprNode_iterStart (/*@observer@*/ uentry name, /*@only@*/ exprNodeList { if (exprNode_isDefined (e)) { - /*@access sRef@*/ - if (e->sref == defref) /*@noaccess sRef@*/ + if (sRef_isInvalid (e->sref)) { /*@-mods@*/ e->sref = sRef_makeUnknown (); @@ -8307,9 +9096,47 @@ static /*@only@*/ exprNode exprNode_effect (exprNode e) exprNode_effect (exprData_getPairB (data))); break; case XPR_OP: - ret = exprNode_op (exprNode_effect (exprData_getOpA (data)), - exprNode_effect (exprData_getOpB (data)), - exprData_getOpTok (data)); + /* + ** evans 2002-03-15: for && and ||, need to do the guards also + ** this is what cgrammar.y does - should be + ** able to avoid duplication, but need to + ** time with grammar productions. + */ + + DPRINTF (("Effect: %s", exprNode_unparse (e))); + + if (lltok_getTok (exprData_getOpTok (data)) == AND_OP) + { + exprNode e1 = exprNode_effect (exprData_getOpA (data)); + exprNode e2; + exprNode_produceGuards (e1); + context_enterAndClause (e1); + e2 = exprNode_effect (exprData_getOpB (data)); + + ret = exprNode_op (e1, e2, + exprData_getOpTok (data)); + + context_exitAndClause (ret, e2); + } + else if (lltok_getTok (exprData_getOpTok (data)) == OR_OP) + { + exprNode e1 = exprNode_effect (exprData_getOpA (data)); + exprNode e2; + exprNode_produceGuards (e1); + context_enterOrClause (e1); + e2 = exprNode_effect (exprData_getOpB (data)); + + ret = exprNode_op (e1, e2, + exprData_getOpTok (data)); + + context_exitOrClause (ret, e2); + } + else + { + ret = exprNode_op (exprNode_effect (exprData_getOpA (data)), + exprNode_effect (exprData_getOpB (data)), + exprData_getOpTok (data)); + } break; case XPR_POSTOP: @@ -8525,6 +9352,9 @@ static /*@observer@*/ cstring exprNode_rootVarName (exprNode e) case XPR_VAR: ret = exprData_getId (data); break; + case XPR_INIT: + ret = idDecl_getName (exprData_getInitId (data)); + break; case XPR_LABEL: case XPR_TOK: case XPR_ITERCALL: @@ -8566,7 +9396,6 @@ static /*@observer@*/ cstring exprNode_rootVarName (exprNode e) case XPR_BLOCK: case XPR_STMT: case XPR_STMTLIST: - case XPR_INIT: case XPR_FACCESS: case XPR_ARROW: case XPR_NODE: @@ -8777,17 +9606,31 @@ static /*@only@*/ cstring exprNode_doUnparse (exprNode e) break; case XPR_BLOCK: - ret = message ("{ %s }", exprNode_unparseFirst (exprData_getSingle (data))); + ret = message ("{ %s }", exprNode_unparse (exprData_getSingle (data))); + /* evans 2002-02-20 was unparseFirst! */ break; case XPR_STMT: - ret = cstring_copy (exprNode_unparse (exprData_getUopNode (data))); + ret = message ("%s;", exprNode_unparse (exprData_getUopNode (data))); break; case XPR_STMTLIST: - ret = message ("%s; %s", - exprNode_unparse (exprData_getPairA (data)), - exprNode_unparse (exprData_getPairB (data))); + if (exprNode_isStatement (exprData_getPairA (data))) + { + /* + ** statement expressions already print the ; + */ + + ret = message ("%s %s", + exprNode_unparse (exprData_getPairA (data)), + exprNode_unparse (exprData_getPairB (data))); + } + else + { + ret = message ("%s; %s", + exprNode_unparse (exprData_getPairA (data)), + exprNode_unparse (exprData_getPairB (data))); + } break; case XPR_FTDEFAULT: @@ -8833,7 +9676,14 @@ static /*@only@*/ cstring exprNode_doUnparse (exprNode e) break; case XPR_STRINGLITERAL: - ret = message ("\"%s\"", exprData_getLiteral (data)); + if (ctype_isWideString (e->typ)) + { + ret = message ("L\"%s\"", exprData_getLiteral (data)); + } + else + { + ret = message ("\"%s\"", exprData_getLiteral (data)); + } break; case XPR_NUMLIT: @@ -8962,7 +9812,22 @@ exprNode_matchLiteral (ctype expected, exprNode e) } else if (ctype_isArrayPtr (expected)) { - return (val == 0); + /* + ** evans 2001-10-14: We allow 0 to match any pointer, but only if the type matches or is void *. + */ + + if (val == 0) + { + if (ctype_match (exprNode_getType (e), expected) + || ctype_isVoidPointer (exprNode_getType (e))) + { + return TRUE; + } + } + else + { + return FALSE; + } } else if (ctype_isAnyFloat (expected)) { @@ -9045,6 +9910,10 @@ exprNode_matchTypes (exprNode e1, exprNode e2) return TRUE; } + DPRINTF (("Matching literal! %s %s %s %s", + ctype_unparse (t1), exprNode_unparse (e2), + ctype_unparse (t2), exprNode_unparse (e1))); + return (exprNode_matchLiteral (t1, e2) || exprNode_matchLiteral (t2, e1)); } @@ -9230,7 +10099,7 @@ exprNode_checkUse (exprNode e, /*@exposed@*/ sRef s, fileloc loc) while (sRef_isValid (s) && sRef_isKnown (s)) { - ynm readable = sRef_isReadable (s); + ynm readable = sRef_isValidLvalue (s); DPRINTF (("Readable: %s / %s", sRef_unparseFull (s), ynm_unparse (readable))); @@ -9241,6 +10110,7 @@ exprNode_checkUse (exprNode e, /*@exposed@*/ sRef s, fileloc loc) { lastRef = errorRef; errorRef = s; + DPRINTF (("Setting ERROR: %s", sRef_unparseFull (s))); deadRef = sRef_isPossiblyDead (errorRef); unuseable = sRef_isUnuseable (errorRef); errorMaybe = TRUE; @@ -9256,6 +10126,7 @@ exprNode_checkUse (exprNode e, /*@exposed@*/ sRef s, fileloc loc) if (!sRef_isPartial (s)) { + DPRINTF (("Defining! %s", sRef_unparseFull (s))); sRef_setDefined (s, fileloc_undefined); } } @@ -9336,6 +10207,8 @@ exprNode_checkUse (exprNode e, /*@exposed@*/ sRef s, fileloc loc) sRef_unparseOpt (errorRef), cstring_makeLiteral (errorMaybe ? "may be " : "")), loc); + + DPRINTF (("Error: %s", sRef_unparseFull (errorRef))); } sRef_setDefined (errorRef, loc); @@ -9392,8 +10265,7 @@ exprNode_checkSet (exprNode e, /*@exposed@*/ sRef s) } if (sRef_isMeaningful (s)) - { - + { if (sRef_isDead (s)) { sRef base = sRef_getBaseSafe (s); @@ -9588,7 +10460,7 @@ checkOneArg (uentry ucurrent, /*@notnull@*/ exprNode current, } } - checkPassTransfer (current, ucurrent, isSpec, fcn, argno, totargs); + transferChecks_passParam (current, ucurrent, isSpec, fcn, argno, totargs); exprNode_mergeUSs (fcn, current); } } @@ -9755,7 +10627,9 @@ static ctype if ((ctype_isRealInt (tr1) || ctype_isReal (tr1)) && (ctype_isRealInt (tr2) || ctype_isReal (tr2))) { - ; + DPRINTF (("No error: [%s] %s / [%s] %s", + exprNode_unparse (e1), ctype_unparse (tr1), + exprNode_unparse (e2), ctype_unparse (tr2))); } else { @@ -10067,6 +10941,10 @@ checkOneRepExpose (sRef ysr, sRef base, static void doAssign (/*@notnull@*/ exprNode e1, /*@notnull@*/ exprNode e2, bool isInit) { + DPRINTF (("Do assign: %s <- %s", + exprNode_unparse (e1), exprNode_unparse (e2))); + DPRINTF (("Ctype: %s", ctype_unparse (exprNode_getType (e1)))); + if (ctype_isRealFunction (exprNode_getType (e1)) && !ctype_isRealPointer (exprNode_getType (e1))) { @@ -10176,11 +11054,11 @@ doAssign (/*@notnull@*/ exprNode e1, /*@notnull@*/ exprNode e2, bool isInit) { DPRINTF (("Check init: %s / %s", exprNode_unparse (e1), exprNode_unparse (e2))); - checkInitTransfer (e1, e2); + transferChecks_initialization (e1, e2); } else { - checkAssignTransfer (e1, e2); + transferChecks_assign (e1, e2); } } else @@ -10214,6 +11092,11 @@ doAssign (/*@notnull@*/ exprNode e1, /*@notnull@*/ exprNode e2, bool isInit) } } + if (exprNode_isStringLiteral (e2)) + { + exprNode_checkStringLiteralLength (exprNode_getType (e1), e2); + } + if (isInit && sRef_isFileOrGlobalScope (e1->sref)) { ; @@ -10451,6 +11334,7 @@ long exprNode_getLongValue (exprNode e) { } else { + /*@!! BADBRANCH;*/ value = 0; } @@ -10477,8 +11361,9 @@ long exprNode_getLongValue (exprNode e) { lltok t = exprData_getUopTok (e->edata); return fileloc_copy(lltok_getLoc (t)); } else { - //drl possible problem : warning fix - // llcontbug (message ("Cannot get next sequence point: %s", exprNode_unparse (e))); + /* drl possible problem : warning fix + llcontbug (message ("Cannot get next sequence point: %s", exprNode_unparse (e))); + */ return fileloc_undefined; } } @@ -10491,3 +11376,8 @@ exprNode exprNode_createNew(ctype c) return ret; } + +bool exprNode_isInitBlock (exprNode e) +{ + return (exprNode_isDefined(e) && e->kind == XPR_INITBLOCK); +}