X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/103db890f4c938d87ba5e66873c757071dd9d2f3..abd7f89523564e5e238e5852585b98f72c3b48f4:/src/exprNode.c diff --git a/src/exprNode.c b/src/exprNode.c index 349965a..f3040f7 100644 --- a/src/exprNode.c +++ b/src/exprNode.c @@ -1,6 +1,6 @@ /* -** LCLint - annotation-assisted static program checker -** Copyright (C) 1994-2000 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,33 +17,33 @@ ** 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" # include "exprChecks.h" -# include "aliasChecks.h" +# include "transferChecks.h" # include "exprNodeSList.h" -# include "exprData.i" +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, sRef p_s); +static void exprNode_addUse (exprNode p_e, /*@exposed@*/ sRef p_s); static bool exprNode_matchArgType (ctype p_ct, exprNode p_e); - exprNode exprNode_fakeCopy (exprNode p_e) /*@*/ ; +static exprNode exprNode_fakeCopy (exprNode p_e) /*@*/ ; static exprNode exprNode_statementError (/*@only@*/ exprNode p_e, /*@only@*/ lltok p_t); static bool exprNode_matchTypes (exprNode p_e1, exprNode p_e2); static void checkUniqueParams (exprNode p_fcn, @@ -56,12 +56,12 @@ static void abstractOpError (ctype p_tr1, ctype p_tr2, lltok p_op, static ctype checkNumerics (ctype p_tr1, ctype p_tr2, ctype p_te1, ctype p_te2, /*@notnull@*/ exprNode p_e1, /*@notnull@*/ exprNode p_e2, lltok p_op); static void doAssign (/*@notnull@*/ exprNode p_e1, /*@notnull@*/ exprNode p_e2, bool p_isInit); -static void checkSafeUse (exprNode p_e, sRef p_s); +static void checkSafeUse (exprNode p_e, /*@exposed@*/ sRef p_s); static void reflectNullTest (/*@notnull@*/ exprNode p_e, bool p_isnull); static void checkMacroParen (exprNode p_e); static exprNodeSList exprNode_flatten (/*@dependent@*/ exprNode p_e); static void exprNode_checkSetAny (exprNode p_e, /*@dependent@*/ cstring p_name); -static void exprNode_checkUse (exprNode p_e, sRef p_s, fileloc p_loc); +static void exprNode_checkUse (exprNode p_e, /*@exposed@*/ sRef p_s, fileloc p_loc); static void exprNode_mergeUSs (exprNode p_res, exprNode p_other); static void exprNode_mergeCondUSs (exprNode p_res, exprNode p_other1, exprNode p_other2); static /*@only@*/ /*@notnull@*/ exprNode exprNode_fromIdentifierAux (/*@observer@*/ uentry p_c); @@ -106,6 +106,21 @@ 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 @*/ +{ + e->requiresConstraints = constraintList_makeNew (); + e->ensuresConstraints = constraintList_makeNew (); + e->trueEnsuresConstraints = constraintList_makeNew (); + e->falseEnsuresConstraints = constraintList_makeNew (); +} + /* ** must occur after library has been read */ @@ -222,6 +237,13 @@ static void exprNode_resetSref (/*@notnull@*/ exprNode e) e->sref = defref; } +exprNode exprNode_fakeCopy (exprNode e) +{ + /*@-temptrans@*/ /*@-retalias@*/ + return e; + /*@=temptrans@*/ /*@=retalias@*/ +} + static bool isFlagKey (char key) { return (key == '-' || key == '+' || key == ' ' || key == '#'); @@ -263,7 +285,15 @@ exprNode_freeIniter (/*@only@*/ exprNode e) switch (e->kind) { case XPR_FACCESS: + /* + ** Its a fake copy, don't free the field->rec and field->field + ** fields. + */ + + /*@-compdestroy@*/ sfree (e->edata->field); + /*@=compdestroy@*/ + sfree (e->edata); break; case XPR_FETCH: @@ -282,6 +312,17 @@ exprNode_freeIniter (/*@only@*/ exprNode e) sRefSet_free (e->sets); sRefSet_free (e->msets); guardSet_free (e->guards); + + constraintList_free(e->requiresConstraints); + constraintList_free(e->ensuresConstraints); + constraintList_free(e->trueEnsuresConstraints); + constraintList_free(e->falseEnsuresConstraints); + + e->requiresConstraints = NULL; + e->ensuresConstraints = NULL; + e->trueEnsuresConstraints = NULL; + e->falseEnsuresConstraints = NULL; + sfree (e); } } @@ -346,6 +387,16 @@ exprNode_free (exprNode e) guardSet_free (e->guards); exprData_free (e->edata, e->kind); + constraintList_free(e->requiresConstraints); + constraintList_free(e->ensuresConstraints); + constraintList_free(e->trueEnsuresConstraints); + constraintList_free(e->falseEnsuresConstraints); + + e->requiresConstraints = NULL; + e->ensuresConstraints = NULL; + e->trueEnsuresConstraints = NULL; + e->falseEnsuresConstraints = NULL; + nowalloc--; sfree (e); /*@-branchstate@*/ @@ -379,8 +430,8 @@ exprNode_new (void) static /*@notnull@*/ /*@special@*/ exprNode exprNode_createPlain (ctype c) /*@defines result@*/ - /*@post:isnull result->edata, result->loc, result->val, result->guards, - result->uses, result->sets, result->msets, result->etext @*/ + /*@ensures isnull result->edata, result->loc, result->val, result->guards, + result->uses, result->sets, result->msets, result->etext @*/ /*@*/ { exprNode e = exprNode_new (); @@ -400,10 +451,9 @@ static /*@notnull@*/ /*@special@*/ exprNode e->canBreak = FALSE; e->mustBreak = FALSE; e->isJumpPoint = FALSE; - e->environment = environmentTable_undefined; - e->requiresConstraints = constraintList_new(); - e->ensuresConstraints = constraintList_new(); - + + exprNode_defineConstraints(e); + return (e); } @@ -509,6 +559,8 @@ static /*@notnull@*/ /*@special@*/ exprNode ret->isJumpPoint = FALSE; ret->edata = exprData_undefined; + exprNode_defineConstraints(ret); + return (ret); } @@ -559,6 +611,8 @@ static /*@notnull@*/ /*@special@*/ exprNode ret->isJumpPoint = FALSE; ret->edata = exprData_undefined; + exprNode_defineConstraints(ret); + return (ret); } @@ -594,6 +648,8 @@ static /*@notnull@*/ /*@special@*/ exprNode ret->isJumpPoint = FALSE; ret->edata = exprData_undefined; + exprNode_defineConstraints(ret); + return (ret); } } @@ -620,7 +676,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) @@ -704,46 +766,76 @@ multiVal exprNode_getValue (exprNode e) } /*@only@*/ exprNode -exprNode_stringLiteral (/*@only@*/ cstring t, /*@only@*/ fileloc loc) +exprNode_combineLiterals (exprNode e, exprNode rest) +{ + cstring ns; + + /* Both must be string literals. */ + + if (exprNode_isUndefined (rest) || exprNode_isUndefined (e)) + { + exprNode_free (rest); + return e; + } + + if (!exprNode_isStringLiteral (e)) + { + voptgenerror + (FLG_SYNTAX, + message ("Constant concatentation is ungrammatical: %s %s", exprNode_unparse (e), + exprNode_unparse (rest)), + e->loc); + exprNode_free (rest); + return e; + } + + if (!exprNode_isStringLiteral (rest)) + { + voptgenerror + (FLG_SYNTAX, + message ("Constant concatentation is ungrammatical: %s %s", exprNode_unparse (e), exprNode_unparse (rest)), + rest->loc); + + exprNode_free (rest); + return e; + } + + ns = cstring_concat (multiVal_forceString (exprNode_getValue (e)), + multiVal_forceString (exprNode_getValue (rest))); + + multiVal_free (e->val); + exprData_free (e->edata, e->kind); + e->edata = exprData_makeLiteral (cstring_copy (ns)); + e->val = multiVal_makeString (ns); + exprNode_free (rest); + return e; +} + +/*@only@*/ exprNode +exprNode_rawStringLiteral (/*@only@*/ cstring t, /*@only@*/ fileloc loc) { exprNode e = exprNode_createLoc (ctype_string, loc); - int len = cstring_length (t) - 2; - char *ts = cstring_toCharsSafe (t); - char *s = cstring_toCharsSafe (cstring_create (len + 1)); + 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, + "length (%d): \"%s\"", + size_toInt (len), context_getValue (FLG_STRINGLITERALLEN), t), e->loc); } } - strncpy (s, ts+1, size_fromInt (len)); - *(s + len) = '\0'; - - e->kind = XPR_STRINGLITERAL; - e->val = multiVal_makeString (cstring_fromCharsO (s)); + e->val = multiVal_makeString (cstring_copy (t)); e->edata = exprData_makeLiteral (t); - e->sref = sRef_makeType (ctype_string); - /* Start modifications */ - /* This expr is null terminated, so we set the len and size */ - sRef_setNullTerminatedState(e->sref); - /* - TPRINTF("Len is set to : %d\n\n", strlen((char *)multiVal_forceString(e->val))); - TPRINTF("Size is set to : %d\n\n", strlen((char *)multiVal_forceString(e->val))); - TPRINTF("State is set to: %d\n\n", e->sref->bufinfo.bufstate); - */ - sRef_setLen(e->sref, strlen((char *)multiVal_forceString(e->val))); - sRef_setSize(e->sref, strlen((char *)multiVal_forceString(e->val))); + e->sref = sRef_makeConst (ctype_string); if (context_getFlag (FLG_READONLYSTRINGS)) { @@ -758,6 +850,28 @@ exprNode_stringLiteral (/*@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) +{ + 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, len); + *(s + len) = '\0'; + cstring_free (t); + return exprNode_rawStringLiteral (cstring_fromCharsO (s), loc); +} + exprNode exprNode_fromUIO (cstring c) { fileloc loc = context_getSaveLocation (); @@ -815,8 +929,7 @@ exprNode exprNode_fromUIO (cstring c) else { voptgenerror - (FLG_UNRECOG, message ("Unrecognized identifier: %s", c), - e->loc); + (FLG_UNRECOG, message ("Unrecognized identifier: %s", c), e->loc); } } @@ -828,12 +941,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) @@ -853,7 +984,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; @@ -883,17 +1014,19 @@ 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); + return e; } else { - return exprNode_createUnknown (); + return exprNode_createUnknown (); } } @@ -917,11 +1050,84 @@ 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; + int len; + + if (ctype_isFixedArray (t1)) + { + int nelements = long_toInt (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) { @@ -930,7 +1136,7 @@ exprNode_fromIdentifierAux (/*@observer@*/ uentry c) uentry_setUsed (c, e->loc); - if (uentry_isVar (c) && sRef_isGlobal (sr)) + if (uentry_isVar (c) && sRef_isFileOrGlobalScope (sr)) { checkGlobUse (c, FALSE, e); } @@ -965,6 +1171,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; @@ -987,6 +1203,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); @@ -1001,10 +1220,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] */ @@ -1021,6 +1242,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)) @@ -1032,6 +1255,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 */ @@ -1138,7 +1362,7 @@ exprNode_arrayFetch (/*@only@*/ exprNode e1, /*@only@*/ exprNode e2) } else { - ret->sref = sRef_makeArrayFetch (arr->sref); + ret->sref = sRef_makeArrayFetch (arr->sref); } ret->sets = sRefSet_realNewUnion (arr->sets, ind->sets); @@ -1242,16 +1466,20 @@ checkPrintfArgs (/*@notnull@*/ /*@dependent@*/ exprNode f, uentry fcn, while ((code = strchr (code, '%')) != NULL) { char *origcode = code; + cstring codetext = cstring_newEmpty (); char key = *(++code); ctype modtype = ctype_int; bool modified = FALSE; fileloc_addColumn (formatloc, code - ocode); + codetext = cstring_appendChar (codetext, key); + /* ignore flags */ while (isFlagKey (key)) { key = *(++code); + codetext = cstring_appendChar (codetext, key); fileloc_incColumn (formatloc); } @@ -1264,6 +1492,7 @@ checkPrintfArgs (/*@notnull@*/ /*@dependent@*/ exprNode f, uentry fcn, while (isdigit ((int) key) != 0) { key = *(++code); + codetext = cstring_appendChar (codetext, key); fileloc_incColumn (formatloc); } @@ -1271,6 +1500,7 @@ checkPrintfArgs (/*@notnull@*/ /*@dependent@*/ exprNode f, uentry fcn, if (key == '.') { key = *(++code); + codetext = cstring_appendChar (codetext, key); fileloc_incColumn (formatloc); /* @@ -1289,6 +1519,7 @@ checkPrintfArgs (/*@notnull@*/ /*@dependent@*/ exprNode f, uentry fcn, while (isdigit ((int) key) != 0) { key = *(++code); + codetext = cstring_appendChar (codetext, key); fileloc_incColumn (formatloc); } } @@ -1298,17 +1529,20 @@ checkPrintfArgs (/*@notnull@*/ /*@dependent@*/ exprNode f, uentry fcn, { modtype = ctype_sint; /* short */ key = *(++code); + codetext = cstring_appendChar (codetext, key); fileloc_incColumn (formatloc); } else if (key == 'l' || key == 'L') { modtype = ctype_lint; /* long */ key = *(++code); + codetext = cstring_appendChar (codetext, key); fileloc_incColumn (formatloc); if (key == 'l' || key == 'L') { modtype = ctype_llint; /* long long */ key = *(++code); + codetext = cstring_appendChar (codetext, key); fileloc_incColumn (formatloc); } } @@ -1328,9 +1562,9 @@ checkPrintfArgs (/*@notnull@*/ /*@dependent@*/ exprNode f, uentry fcn, if (optgenerror (FLG_TYPE, message ("No argument corresponding to %q format " - "code %d (%%%h): \"%s\"", + "code %d (%%%s): \"%s\"", uentry_getName (fcn), - i, key, + i, codetext, cstring_fromChars (format)), f->loc)) { @@ -1369,9 +1603,10 @@ checkPrintfArgs (/*@notnull@*/ /*@dependent@*/ exprNode f, uentry fcn, expecttype = ctype_combine (ctype_int, modtype); /*@switchbreak@*/ break; - case 'x': /* unsigned int */ + case 'x': /* unsigned int */ case 'X': - expecttype = ctype_combine (ctype_uint, modtype); + expecttype = ctype_combine (ctype_uint, modtype); + /*@switchbreak@*/ break; case 'e': @@ -1383,7 +1618,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 */ @@ -1394,6 +1636,7 @@ checkPrintfArgs (/*@notnull@*/ /*@dependent@*/ exprNode f, uentry fcn, while (((key = *(++code)) != ']') && (key != '\0')) { + codetext = cstring_appendChar (codetext, key); fileloc_incColumn (formatloc); } @@ -1409,7 +1652,8 @@ checkPrintfArgs (/*@notnull@*/ /*@dependent@*/ exprNode f, uentry fcn, case 'p': /* pointer */ expecttype = ctype_makePointer (ctype_void); - /* really! */ + uentry_setDefState (regArg, SS_RELDEF); /* need not be defined */ + sRef_setPosNull (uentry_getSref (regArg), fileloc_undefined); /* could be null */ /*@switchbreak@*/ break; case 'n': /* pointer to int, modified by call! */ @@ -1450,11 +1694,12 @@ checkPrintfArgs (/*@notnull@*/ /*@dependent@*/ exprNode f, uentry fcn, if (llgenformattypeerror (expecttype, exprNode_undefined, a->typ, a, - message ("Format argument %d to %q (%%%h) expects " + message ("Format argument %d to %q (%%%s) expects " "%t gets %t: %s", i - argno, uentry_getName (fcn), - key, expecttype, + codetext, + expecttype, a->typ, exprNode_unparse (a)), a->loc)) { @@ -1480,7 +1725,7 @@ checkPrintfArgs (/*@notnull@*/ /*@dependent@*/ exprNode f, uentry fcn, uentry_setType (regArg, ctype_unknown); uentry_fixupSref (regArg); - + if (modified) { exprNode_checkCallModifyVal (a->sref, args, f, ret); @@ -1492,13 +1737,15 @@ checkPrintfArgs (/*@notnull@*/ /*@dependent@*/ exprNode f, uentry fcn, } } } + ocode = code; + cstring_free (codetext); } if (i < nargs) { voptgenerror (FLG_TYPE, - message ("Format string for %q has %d arg%p, given %d", + message ("Format string for %q has %d arg%&, given %d", uentry_getName (fcn), i - argno, nargs - argno), f->loc); } @@ -1506,8 +1753,17 @@ checkPrintfArgs (/*@notnull@*/ /*@dependent@*/ exprNode f, uentry fcn, else { /* no checking possible for compile-time unknown format strings */ + if (exprNode_isDefined (a)) + { + voptgenerror + (FLG_FORMATCONST, + message ("Format string parameter to %s is not a compile-time constant: %s", + exprNode_unparse (f), + exprNode_unparse (a)), + f->loc); + } } - + fileloc_free (formatloc); } @@ -1544,11 +1800,13 @@ checkScanfArgs (/*@notnull@*/ /*@dependent@*/ exprNode f, uentry fcn, { char *origcode = code; char key = *(++code); + cstring codetext = cstring_newEmpty (); ctype modtype = ctype_int; char modifier = '\0'; bool modified = TRUE; bool ignore = FALSE; + codetext = cstring_appendChar (codetext, key); fileloc_addColumn (formatloc, code - ocode); /* @@ -1561,6 +1819,7 @@ checkScanfArgs (/*@notnull@*/ /*@dependent@*/ exprNode f, uentry fcn, if (key == '*') { key = *(++code); + codetext = cstring_appendChar (codetext, key); modified = FALSE; ignore = TRUE; fileloc_incColumn (formatloc); @@ -1570,6 +1829,7 @@ checkScanfArgs (/*@notnull@*/ /*@dependent@*/ exprNode f, uentry fcn, while (isdigit ((int) key) != 0) { key = *(++code); + codetext = cstring_appendChar (codetext, key); fileloc_incColumn (formatloc); } @@ -1577,6 +1837,7 @@ checkScanfArgs (/*@notnull@*/ /*@dependent@*/ exprNode f, uentry fcn, { modtype = ctype_sint; /* short */ key = *(++code); + codetext = cstring_appendChar (codetext, key); fileloc_incColumn (formatloc); } else if (key == 'l' || key == 'L') @@ -1585,11 +1846,14 @@ checkScanfArgs (/*@notnull@*/ /*@dependent@*/ exprNode f, uentry fcn, modifier = key; key = *(++code); + codetext = cstring_appendChar (codetext, key); + fileloc_incColumn (formatloc); if (key == 'l' || key == 'L') { modtype = ctype_llint; /* long long */ key = *(++code); + codetext = cstring_appendChar (codetext, key); fileloc_incColumn (formatloc); } } @@ -1615,9 +1879,9 @@ checkScanfArgs (/*@notnull@*/ /*@dependent@*/ exprNode f, uentry fcn, if (optgenerror (FLG_TYPE, message ("No argument corresponding to %q format " - "code %d (%%%h): \"%s\"", + "code %d (%%%s): \"%s\"", uentry_getName (fcn), - i, key, + i, codetext, cstring_fromChars (format)), f->loc)) { @@ -1694,6 +1958,7 @@ checkScanfArgs (/*@notnull@*/ /*@dependent@*/ exprNode f, uentry fcn, while (((key = *(++code)) != ']') && (key != '\0')) { + codetext = cstring_appendChar (codetext, key); fileloc_incColumn (formatloc); } @@ -1706,10 +1971,17 @@ checkScanfArgs (/*@notnull@*/ /*@dependent@*/ exprNode f, uentry fcn, expecttype = ctype_string; /*@switchbreak@*/ break; + case 'p': /* pointer */ + voptgenerror + (FLG_FORMATCODE, + message ("Format code should not be used in scanf: %s", + cstring_fromChars (origcode)), + fileloc_isDefined (formatloc) + ? formatloc : g_currentloc); + expecttype = ctype_unknown; - /* really! */ /*@switchbreak@*/ break; case 'n': /* pointer to int, modified by call! */ @@ -1739,52 +2011,24 @@ checkScanfArgs (/*@notnull@*/ /*@dependent@*/ exprNode f, uentry fcn, } else { - if (modifier != '\0') - { - if (llgenformattypeerror - (expecttype, exprNode_undefined, - a->typ, a, - message ("Format argument %d to %q (%%%h%h) expects " - "%t gets %t: %s", - i - argno, - uentry_getName (fcn), - modifier, - key, expecttype, - a->typ, exprNode_unparse (a)), - a->loc)) - { - if (fileloc_isDefined (formatloc) - && context_getFlag (FLG_SHOWCOL)) - { - llgenindentmsg - (cstring_makeLiteral - ("Corresponding format code"), - formatloc); - } - } - - } - else + if (llgenformattypeerror + (expecttype, exprNode_undefined, + a->typ, a, + message ("Format argument %d to %q (%%%s) expects " + "%t gets %t: %s", + i - argno, + uentry_getName (fcn), + codetext, expecttype, + a->typ, exprNode_unparse (a)), + a->loc)) { - if (llgenformattypeerror - (expecttype, exprNode_undefined, - a->typ, a, - message ("Format argument %d to %q (%%%h) expects " - "%t gets %t: %s", - i - argno, - uentry_getName (fcn), - key, expecttype, - a->typ, exprNode_unparse (a)), - a->loc)) + if (fileloc_isDefined (formatloc) + && context_getFlag (FLG_SHOWCOL)) { - if (fileloc_isDefined (formatloc) - && context_getFlag (FLG_SHOWCOL)) - { - llgenindentmsg - (cstring_makeLiteral - ("Corresponding format code"), - formatloc); - } + llgenindentmsg + (cstring_makeLiteral + ("Corresponding format code"), + formatloc); } } } @@ -1807,13 +2051,15 @@ checkScanfArgs (/*@notnull@*/ /*@dependent@*/ exprNode f, uentry fcn, } } } + ocode = code; + cstring_free (codetext); } if (i < nargs) { voptgenerror (FLG_TYPE, - message ("Format string for %q has %d arg%p, given %d", + message ("Format string for %q has %d arg%&, given %d", uentry_getName (fcn), i - argno, nargs - argno), f->loc); } @@ -1878,13 +2124,17 @@ checkMessageArgs (/*@notnull@*/ /*@dependent@*/ exprNode f, { char *origcode = code; char key = *(++code); + cstring codetext = cstring_newEmpty (); bool isOnly = FALSE; + codetext = cstring_appendChar (codetext, key); + fileloc_addColumn (formatloc, code - ocode); while (key >= '0' && key <= '9') { key = *(++code); + codetext = cstring_appendChar (codetext, key); fileloc_incColumn (formatloc); } @@ -1893,7 +2143,7 @@ checkMessageArgs (/*@notnull@*/ /*@dependent@*/ exprNode f, if (key != '%') { - if (key == 'p') + if (key == '&') /* plural marker */ { goto nextKey; } @@ -1902,8 +2152,8 @@ checkMessageArgs (/*@notnull@*/ /*@dependent@*/ exprNode f, { voptgenerror (FLG_TYPE, - message ("Message missing format arg %d (%%%h): \"%s\"", - i + 1, key, format), + message ("Message missing format arg %d (%%%s): \"%s\"", + i + 1, codetext, format), f->loc); i++; } @@ -1937,7 +2187,7 @@ checkMessageArgs (/*@notnull@*/ /*@dependent@*/ exprNode f, case 'b': expecttype = ctype_bool; break; case 't': expecttype = ctypeType; break; case 'l': expecttype = filelocType; break; - case 'p': /* a wee bit of a hack methinks */ + case '&': /* a wee bit of a hack methinks */ expecttype = ctype_int; break; case 'r': expecttype = ctype_bool; break; @@ -1966,11 +2216,11 @@ checkMessageArgs (/*@notnull@*/ /*@dependent@*/ exprNode f, if (llgenformattypeerror (expecttype, exprNode_undefined, a->typ, a, - message ("Format argument %d to %q (%%%h) expects " + message ("Format argument %d to %q (%%%s) expects " "%t gets %t: %s", i - argno, uentry_getName (fcn), - key, expecttype, + codetext, expecttype, a->typ, exprNode_unparse (a)), a->loc)) { @@ -2007,12 +2257,14 @@ checkMessageArgs (/*@notnull@*/ /*@dependent@*/ exprNode f, } } } + + cstring_free (codetext); } if (i < nargs) { voptgenerror (FLG_TYPE, - message ("Format string for %q has %d arg%p, given %d", + message ("Format string for %q has %d arg%&, given %d", uentry_getName (fcn), i - argno, nargs -argno), f->loc); } @@ -2035,7 +2287,7 @@ static void { bool hadUncon = FALSE; - if (sRef_isGlobal (sRef_getRootBase (e1->sref)) && + if (sRef_isFileOrGlobalScope (sRef_getRootBase (e1->sref)) && sRefSet_hasUnconstrained (sets2)) { voptgenerror @@ -2049,7 +2301,7 @@ static void e2->loc); } - if (sRef_isGlobal (sRef_getRootBase (e2->sref)) && + if (sRef_isFileOrGlobalScope (sRef_getRootBase (e2->sref)) && sRefSet_hasUnconstrained (sets1)) { voptgenerror @@ -2167,8 +2419,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); @@ -2470,7 +2724,7 @@ checkSequencingOne (exprNode f, exprNodeList args, { sRefSet otheruses = jl->uses; - if (sRef_isGlobal (sRef_getRootBase (jl->sref)) && + if (sRef_isFileOrGlobalScope (sRef_getRootBase (jl->sref)) && sRefSet_hasUnconstrained (thissets)) { voptgenerror @@ -2600,6 +2854,8 @@ checkGlobMods (/*@notnull@*/ /*@dependent@*/ exprNode f, bool freshMods = FALSE; uentryList params = uentryList_undefined; + DPRINTF (("Check glob mods: %s", exprNode_unparse (ret))); + /* ** check globals and modifies */ @@ -2622,7 +2878,7 @@ checkGlobMods (/*@notnull@*/ /*@dependent@*/ exprNode f, if (!context_getFlag (FLG_MODNOMODS) && !context_getFlag (FLG_GLOBUNSPEC)) { - checkUnspecCall (f, params, args); + checkUnspecCall (f, params, args); } return; @@ -2649,6 +2905,7 @@ checkGlobMods (/*@notnull@*/ /*@dependent@*/ exprNode f, uentry_unparse (le))); params = ctype_argsFunction (ct); + return; /*@32 ! remove this? */ } /* @@ -2656,7 +2913,6 @@ checkGlobMods (/*@notnull@*/ /*@dependent@*/ exprNode f, */ setCodePoint (); - globSet_allElements (usesGlobs, el) { @@ -2767,6 +3023,8 @@ checkGlobMods (/*@notnull@*/ /*@dependent@*/ exprNode f, sRefSet_allElements (mods, s) /* s is something which may be modified */ { + DPRINTF (("Check modify: %s", sRef_unparse (s))); + if (sRef_isKindSpecial (s)) { if (sRef_isSpecInternalState (s)) @@ -2797,7 +3055,7 @@ checkGlobMods (/*@notnull@*/ /*@dependent@*/ exprNode f, { sRef rb = sRef_getRootBase (s); - if (sRef_isGlobal (rb)) + if (sRef_isFileOrGlobalScope (rb)) { context_usedGlobal (rb); } @@ -2910,7 +3168,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. */ @@ -2963,72 +3221,564 @@ void checkGlobUse (uentry glob, bool isCall, /*@notnull@*/ exprNode e) } } -static /*@only@*/ exprNode -functionCallSafe (/*@only@*/ /*@notnull@*/ exprNode f, - ctype t, /*@keep@*/ exprNodeList args) +static void +reflectEnsuresClause (exprNode ret, uentry le, exprNode f, exprNodeList args) { - /* requires f is a non-error exprNode, with type function */ - cstring fname = exprNode_unparse (f); - uentry le = exprNode_getUentry (f); - exprNode ret = exprNode_createPartialCopy (f); - int special; - - setCodePoint (); - - ret->typ = ctype_returnValue (t); - ret->kind = XPR_CALL; - - ret->edata = exprData_makeCall (f, args); - - /* - ** Order of these steps is very important! - ** - ** Must check for argument dependencies before messing up uses and sets. - */ + DPRINTF (("Reflect ensures clause: %s(%s) / %s / %s", + exprNode_unparse (f), exprNodeList_unparse (args), + uentry_unparseFull (le), + stateClauseList_unparse (uentry_getStateClauseList (le)))); - if (context_getFlag (FLG_EVALORDER)) + if (uentry_isValid (le) && uentry_isFunction (le)) { - exprNodeList_elements (args, current) - { - if (exprNode_isDefined (current)) - { - exprNode_addUse (current, current->sref); - } - } end_exprNodeList_elements; + stateClauseList sclauses = uentry_getStateClauseList (le); - if (context_maybeSet (FLG_EVALORDER) || context_maybeSet (FLG_EVALORDERUNCON)) - { - checkSequencing (f, args); - } - - exprNodeList_elements (args, current) + if (stateClauseList_isDefined (sclauses)) { - if (exprNode_isDefined (current) && sRef_isMeaningful (current->sref)) + DPRINTF (("Reflect ensures: %s / %s / %s", + uentry_unparse (le), + exprNode_unparse (f), exprNodeList_unparse (args))); + + stateClauseList_elements (sclauses, cl) { - exprNode_addUse (ret, sRef_makeDerived (current->sref)); - } - } end_exprNodeList_elements ; - } - - special = checkArgs (le, f, t, args, ret); - checkGlobMods (f, le, args, ret, special); + if (stateClause_hasEnsures (cl)) + { + /* Same in usymtab.c:1904 */ + if (stateClause_setsMetaState (cl)) + { + qual q = stateClause_getMetaQual (cl); + annotationInfo ainfo = qual_getAnnotationInfo (q); + metaStateInfo minfo = annotationInfo_getState (ainfo); + cstring key = metaStateInfo_getName (minfo); + int mvalue = annotationInfo_getValue (ainfo); + + sRefSet osrs = sRefSet_undefined; + sRefSet srs; + + if (stateClause_isGlobal (cl)) + { + srs = sRefSet_single (usymtab_lookupGlobalMarker ()); + osrs = srs; + } + else + { + srs = stateClause_getRefs (cl); + } + + DPRINTF (("Reflect ensures clause: %s", stateClause_unparse (cl))); + + + DPRINTF (("Sets meta state! %s", stateClause_unparse (cl))); + + sRefSet_elements (srs, sel) + { + sRef s; + + if (sRef_isResult (sRef_getRootBase (sel))) + { + s = exprNode_getSref (ret); + } + else + { + s = sRef_fixBaseParam (sel, args); + } - setCodePoint (); + DPRINTF (("Reflecting state clause on: %s / %s", + sRef_unparse (sel), sRef_unparse (s))); + + sRef_setMetaStateValueComplete (s, key, mvalue, exprNode_loc (f)); + } end_sRefSet_elements; - if (uentry_isValid (le) - && (uentry_isFunction (le) - || (uentry_isVariable (le) - && ctype_isFunction (uentry_getType (le))))) - { - exitkind exk = uentry_getExitCode (le); + sRefSet_free (osrs); + } + else + { + sRefSet srs = stateClause_getRefs (cl); + sRefModVal modf = stateClause_getEnsuresFunction (cl); + int eparam = stateClause_getStateParameter (cl); - /* f->typ is already set to the return type */ + llassert (modf != NULL); - ret->sref = uentry_returnedRef (le, args); + DPRINTF (("Reflect after clause: %s / %s", + stateClause_unparse (cl), + sRefSet_unparse (srs))); + + sRefSet_elements (srs, sel) + { + sRef s; + + DPRINTF (("elements: %s", sRef_unparse (sel))); + DPRINTF (("elements: %s", sRef_unparseFull (sel))); + + if (sRef_isResult (sRef_getRootBase (sel))) + { + 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); + } - if (uentry_isFunction (le) && exprNodeList_size (args) >= 1) - { - qual nullPred = uentry_nullPred (le); + 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); + + 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)); + + 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); + } + 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 */ + } + } + } + + 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); + } + } +} + +static void +checkRequiresClause (uentry le, exprNode f, exprNodeList args) +{ + DPRINTF (("Check requires clause: %s(%s) / %s / %s", + exprNode_unparse (f), exprNodeList_unparse (args), + uentry_unparseFull (le), + stateClauseList_unparse (uentry_getStateClauseList (le)))); + + if (uentry_isValid (le) && uentry_isFunction (le)) + { + stateClauseList sclauses = uentry_getStateClauseList (le); + + if (stateClauseList_isDefined (sclauses)) + { + DPRINTF (("Check requires: %s / %s / %s", + uentry_unparse (le), + exprNode_unparse (f), exprNodeList_unparse (args))); + + stateClauseList_elements (sclauses, cl) + { + DPRINTF (("Check clause: %s / %s", + stateClause_unparse (cl), + bool_unparse (stateClause_hasRequires (cl)))); + + if (stateClause_hasRequires (cl)) + { + sRefSet osrs = sRefSet_undefined; + sRefSet srs; + + if (stateClause_isGlobal (cl)) + { + srs = sRefSet_single (usymtab_lookupGlobalMarker ()); + osrs = srs; + } + else + { + srs = stateClause_getRefs (cl); + } + + DPRINTF (("Refs: %s", sRefSet_unparse (srs))); + + if (stateClause_setsMetaState (cl)) + { + qual q = stateClause_getMetaQual (cl); + annotationInfo ainfo = qual_getAnnotationInfo (q); + metaStateInfo minfo = annotationInfo_getState (ainfo); + cstring key = metaStateInfo_getName (minfo); + int mvalue = annotationInfo_getValue (ainfo); + + DPRINTF (("Requires meta state! %s = %d", key, mvalue)); + + sRefSet_elements (srs, sel) + { + sRef s = sRef_fixBaseParam (sel, args); + + if (sRef_isResult (sRef_getRootBase (sel))) + { + BADBRANCH; + } + else + { + DPRINTF (("Checking state clause on: %s / %s / %s = %d", + sRef_unparseFull (sel), sRef_unparseFull (s), + key, mvalue)); + + if (!sRef_checkMetaStateValue (s, key, mvalue)) + { + DPRINTF (("HERE: %s", sRef_unparse (s))); + if (optgenerror + (FLG_STATETRANSFER, + message + ("Requires clause of called function %q not satisfied%q (state is %q): %q", + uentry_getName (le), + sRef_isGlobalMarker (s) + ? message ("") + : message (" by %q", sRef_unparse (s)), + stateValue_unparseValue (sRef_getMetaStateValue (s, key), + minfo), + stateClause_unparse (cl)), + exprNode_loc (f))) + { + sRef_showAliasInfo (s); + } + else + { + DPRINTF (("Error supressed!")); + DPRINTF (("Loc: %s", fileloc_unparse (exprNode_loc (f)))); + DPRINTF (("Context supress: %s", + bool_unparse (context_suppressFlagMsg (FLG_STATETRANSFER, exprNode_loc (f))))); + } + } + } + } end_sRefSet_elements; + } + else + { + sRefModVal modf = stateClause_getRequiresBodyFunction (cl); + int eparam = stateClause_getStateParameter (cl); + + DPRINTF (("Reflect after clause: %s / %s", + stateClause_unparse (cl), + sRefSet_unparse (srs))); + + llassert (modf != NULL); + + sRefSet_elements (srs, sel) + { + sRef s; + + DPRINTF (("elements: %s", sRef_unparse (sel))); + DPRINTF (("elements: %s", sRef_unparseFull (sel))); + + s = sRef_fixBaseParam (sel, args); + + DPRINTF (("elements: %s", sRef_unparse (s))); + DPRINTF (("elements: %s", sRef_unparseFull (s))); + + if (sRef_isResult (sRef_getRootBase (sel))) + { + ; /*@i423 what do we do about results */ + } + else + { + DPRINTF (("Reflecting state clause on: %s / %s", + sRef_unparse (sel), sRef_unparse (s))); + + modf (s, eparam, exprNode_loc (f)); + } + } end_sRefSet_elements; + } + + sRefSet_free (osrs); + } + } end_stateClauseList_elements ; + } + } +} + +static /*@only@*/ exprNode +functionCallSafe (/*@only@*/ /*@notnull@*/ exprNode f, + ctype t, /*@keep@*/ exprNodeList args) +{ + /* requires f is a non-error exprNode, with type function */ + cstring fname = exprNode_unparse (f); + uentry le = exprNode_getUentry (f); + exprNode ret = exprNode_createPartialCopy (f); + int special; + + setCodePoint (); + + DPRINTF (("Call: %s %s",exprNode_unparse (f), exprNodeList_unparse (args))); + + ret->typ = ctype_getReturnType (t); + ret->kind = XPR_CALL; + + ret->edata = exprData_makeCall (f, args); + + /* + ** Order of these steps is very important! + ** + ** Must check for argument dependencies before messing up uses and sets. + */ + + if (context_getFlag (FLG_EVALORDER)) + { + exprNodeList_elements (args, current) + { + if (exprNode_isDefined (current)) + { + exprNode_addUse (current, current->sref); + } + } end_exprNodeList_elements; + + if (context_maybeSet (FLG_EVALORDER) || context_maybeSet (FLG_EVALORDERUNCON)) + { + checkSequencing (f, args); + } + + exprNodeList_elements (args, current) + { + if (exprNode_isDefined (current) && sRef_isMeaningful (current->sref)) + { + exprNode_addUse (ret, sRef_makeDerived (current->sref)); + } + } end_exprNodeList_elements ; + } + + special = checkArgs (le, f, t, args, ret); + checkGlobMods (f, le, args, ret, special); + checkRequiresClause (le, f, args); + setCodePoint (); + + if (uentry_isValid (le) + && (uentry_isFunction (le) + || (uentry_isVariable (le) + && ctype_isFunction (uentry_getType (le))))) + { + exitkind exk = uentry_getExitCode (le); + + /* 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); if (qual_isTrueNull (nullPred)) { @@ -3134,6 +3884,11 @@ functionCallSafe (/*@only@*/ /*@notnull@*/ exprNode f, 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); } @@ -3141,8 +3896,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)) { @@ -3157,6 +3911,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) { @@ -3260,8 +4027,9 @@ exprNode_functionCall (/*@only@*/ exprNode f, /*@only@*/ exprNodeList args) } } -exprNode -exprNode_fieldAccess (/*@only@*/ exprNode s, /*@only@*/ cstring f) +static exprNode +exprNode_fieldAccessAux (/*@only@*/ exprNode s, /*@observer@*/ fileloc loc, + /*@only@*/ cstring f) { exprNode ret = exprNode_createPartialCopy (s); @@ -3276,11 +4044,11 @@ exprNode_fieldAccess (/*@only@*/ exprNode s, /*@only@*/ cstring f) { ctype t = exprNode_getType (s); ctype tr = ctype_realType (t); - + checkMacroParen (s); ret->edata = exprData_makeField (s, f); - + if (ctype_isStructorUnion (tr)) { uentry tf = uentryList_lookupField (ctype_getFields (tr), f); @@ -3290,8 +4058,8 @@ exprNode_fieldAccess (/*@only@*/ exprNode s, /*@only@*/ cstring f) voptgenerror (FLG_TYPE, message ("Access non-existent field %s of %t: %s", f, t, exprNode_unparse (ret)), - s->loc); - + loc); + /*! cstring_free (f); */ /* evans 2001-03-25 self-detect */ return (ret); } else @@ -3302,6 +4070,7 @@ exprNode_fieldAccess (/*@only@*/ exprNode s, /*@only@*/ cstring f) checkSafeUse (ret, s->sref); ret->sref = sRef_makeField (s->sref, uentry_rawName (tf)); + /*!? exprNode_free (s); */ /* evans 2001-03-25 self-detect */ return (ret); } } @@ -3313,7 +4082,7 @@ exprNode_fieldAccess (/*@only@*/ exprNode s, /*@only@*/ cstring f) (FLG_ABSTRACT, message ("Access field of abstract type (%t): %s.%s", t, exprNode_unparse (s), f), - s->loc); + loc); ret->typ = ctype_unknown; } else @@ -3325,21 +4094,21 @@ exprNode_fieldAccess (/*@only@*/ exprNode s, /*@only@*/ cstring f) message ("Access field of non-struct or union (%t): %s.%s", t, exprNode_unparse (s), f), - s->loc); + loc); ret->typ = ctype_unknown; } else { cstring sn = cstring_copy (f); - + checkSafeUse (ret, s->sref); cstring_markOwned (sn); ret->sref = sRef_makeField (s->sref, sn); - return (ret); } } + return (ret); } } @@ -3347,197 +4116,216 @@ exprNode_fieldAccess (/*@only@*/ exprNode s, /*@only@*/ cstring f) } exprNode -exprNode_addParens (/*@only@*/ lltok lpar, /*@only@*/ exprNode e) -{ - exprNode ret = exprNode_createPartialCopy (e); - - ret->loc = fileloc_update (ret->loc, lltok_getLoc (lpar)); - ret->kind = XPR_PARENS; - ret->edata = exprData_makeUop (e, lpar); - - if (!exprNode_isError (e)) - { - ret->exitCode = e->exitCode; - ret->canBreak = e->canBreak; - ret->mustBreak = e->mustBreak; - ret->isJumpPoint = e->isJumpPoint; - ret->sref = e->sref; - } - - return ret; -} - -exprNode -exprNode_arrowAccess (/*@only@*/ exprNode s, /*@only@*/ cstring f) +exprNode_fieldAccess (/*@only@*/ exprNode s, /*@only@*/ lltok dot, + /*@only@*/ cstring f) +{ + exprNode res = exprNode_fieldAccessAux (s, lltok_getLoc (dot), f); + lltok_release (dot); + return res; +} + +exprNode +exprNode_addParens (/*@only@*/ lltok lpar, /*@only@*/ exprNode e) +{ + exprNode ret = exprNode_createPartialCopy (e); + + ret->loc = fileloc_update (ret->loc, lltok_getLoc (lpar)); + ret->kind = XPR_PARENS; + ret->edata = exprData_makeUop (e, lpar); + + if (!exprNode_isError (e)) + { + ret->exitCode = e->exitCode; + ret->canBreak = e->canBreak; + ret->mustBreak = e->mustBreak; + ret->isJumpPoint = e->isJumpPoint; + ret->sref = e->sref; + } + + return ret; +} + +static exprNode +exprNode_arrowAccessAux (/*@only@*/ exprNode s, /*@observer@*/ fileloc loc, + /*@only@*/ cstring f) +{ + exprNode ret = exprNode_createPartialCopy (s); + + ret->edata = exprData_makeField (s, f); + ret->kind = XPR_ARROW; + + if (exprNode_isError (s)) + { + return (ret); + } + else + { + ctype t = exprNode_getType (s); + ctype tr = ctype_realType (t); + + checkMacroParen (s); + + (void) ctype_fixArrayPtr (tr); /* REWRITE THIS */ + + if (ctype_isRealPointer (tr)) + { + ctype b = ctype_realType (ctype_baseArrayPtr (tr)); + + if (ctype_isStructorUnion (b)) + { + uentry fentry = uentryList_lookupField (ctype_getFields (b), f); + + if (sRef_isKnown (s->sref) && sRef_possiblyNull (s->sref)) + { + if (!usymtab_isGuarded (s->sref) && !context_inProtectVars ()) + { + if (optgenerror + (FLG_NULLDEREF, + message ("Arrow access from %s pointer%q: %s", + sRef_nullMessage (s->sref), + sRef_unparsePreOpt (s->sref), + exprNode_unparse (ret)), + loc)) + { + sRef_showNullInfo (s->sref); + sRef_setNullError (s->sref); + } + } + } + + if (uentry_isUndefined (fentry)) + { + voptgenerror + (FLG_TYPE, + message ("Access non-existent field %s of %t: %s", + f, t, exprNode_unparse (ret)), + loc); + ret->typ = ctype_unknown; + return (ret); + } + else + { + /* + ** was safeUse: shouldn't be safe! + ** + ** to do rec->field + ** rec must be defined, + ** *rec must be allocated + ** rec->field need only be defined it if is an rvalue + */ + + uentry_setUsed (fentry, exprNode_loc (ret)); + ret->typ = uentry_getType (fentry); + + exprNode_checkUse (ret, s->sref, s->loc); + + /* exprNode_checkUse (ret, sRef_makePointer (s->sref), s->loc); */ + ret->sref = sRef_makeArrow (s->sref, uentry_rawName (fentry)); + return (ret); + } + } + else /* Pointer to something that is not a struct or union*/ + { + if (ctype_isRealAbstract (tr)) + { + ctype xrt = ctype_forceRealType (tr); + + voptgenerror + (FLG_ABSTRACT, + message ("Arrow access field of abstract type (%t): %s->%s", + t, exprNode_unparse (s), f), + loc); + + /* + ** Set the state correctly, as if the abstraction is broken. + */ + + if (ctype_isRealPointer (xrt) && + (b = ctype_realType (ctype_baseArrayPtr (xrt)), + ctype_isStructorUnion (b))) + { + uentry fentry = uentryList_lookupField (ctype_getFields (b), f); + ret->typ = uentry_getType (fentry); + ret->sref = sRef_makeArrow (s->sref, uentry_rawName (fentry)); + } + else + { + ret->typ = ctype_unknown; + ret->sref = sRef_undefined; + } + } + else /* not a struct, union or abstract */ + { + if (ctype_isUnknown (tr)) { + cstring sn = cstring_copy (f); + + DPRINTF (("Here: %s", exprNode_unparse (s))); + + exprNode_checkUse (ret, s->sref, s->loc); + exprNode_checkUse (ret, sRef_makePointer (s->sref), s->loc); + + cstring_markOwned (sn); + ret->sref = sRef_makeArrow (s->sref, sn); + + ret->kind = XPR_ARROW; + return (ret); + } else { + voptgenerror + (FLG_TYPE, + message ("Arrow access field of non-struct or union " + "pointer (%t): %s->%s", + t, exprNode_unparse (s), f), + loc); + + ret->typ = ctype_unknown; + ret->sref = sRef_undefined; + } + } + } + } + else /* its not a pointer */ + { + if (!ctype_isUnknown (tr)) + { + voptgenerror + (FLG_TYPE, + message ("Arrow access of non-pointer (%t): %s->%s", + t, exprNode_unparse (s), f), + loc); + + ret->typ = ctype_unknown; + ret->sref = sRef_undefined; + } + else + { + cstring sn = cstring_copy (f); + + DPRINTF (("Here: %s", exprNode_unparse (s))); + + exprNode_checkUse (ret, s->sref, s->loc); + exprNode_checkUse (ret, sRef_makePointer (s->sref), s->loc); + + cstring_markOwned (sn); + ret->sref = sRef_makeArrow (s->sref, sn); + + ret->kind = XPR_ARROW; + return (ret); + } + } + + return (ret); + } + BADEXIT; +} + +exprNode +exprNode_arrowAccess (/*@only@*/ exprNode s, + /*@only@*/ lltok arrow, + /*@only@*/ cstring f) { - exprNode ret = exprNode_createPartialCopy (s); - - ret->edata = exprData_makeField (s, f); - ret->kind = XPR_ARROW; - - if (exprNode_isError (s)) - { - return (ret); - } - else - { - ctype t = exprNode_getType (s); - ctype tr = ctype_realType (t); - - checkMacroParen (s); - - (void) ctype_fixArrayPtr (tr); /* REWRITE THIS */ - - if (ctype_isRealPointer (tr)) - { - ctype b = ctype_realType (ctype_baseArrayPtr (tr)); - - if (ctype_isStructorUnion (b)) - { - uentry fentry = uentryList_lookupField (ctype_getFields (b), f); - - if (sRef_isKnown (s->sref) && sRef_possiblyNull (s->sref)) - { - if (!usymtab_isGuarded (s->sref) && !context_inProtectVars ()) - { - if (optgenerror - (FLG_NULLDEREF, - message ("Arrow access from %s pointer%q: %s", - sRef_nullMessage (s->sref), - sRef_unparsePreOpt (s->sref), - exprNode_unparse (ret)), - s->loc)) - { - sRef_showNullInfo (s->sref); - sRef_setNullError (s->sref); - } - } - } - - if (uentry_isUndefined (fentry)) - { - voptgenerror - (FLG_TYPE, - message ("Access non-existent field %s of %t: %s", - f, t, exprNode_unparse (ret)), - s->loc); - ret->typ = ctype_unknown; - - return (ret); - } - else - { - /* - ** was safeUse: shouldn't be safe! - ** - ** to do rec->field - ** rec must be defined, - ** *rec must be allocated - ** rec->field need only be defined it if is an rvalue - */ - - uentry_setUsed (fentry, exprNode_loc (ret)); - ret->typ = uentry_getType (fentry); - - exprNode_checkUse (ret, s->sref, s->loc); - - /* exprNode_checkUse (ret, sRef_makePointer (s->sref), s->loc); */ - ret->sref = sRef_makeArrow (s->sref, uentry_rawName (fentry)); - return (ret); - } - } - else /* Pointer to something that is not a struct or union*/ - { - if (ctype_isRealAbstract (tr)) - { - ctype xrt = ctype_forceRealType (tr); - - voptgenerror - (FLG_ABSTRACT, - message ("Arrow access field of abstract type (%t): %s->%s", - t, exprNode_unparse (s), f), - s->loc); - - /* - ** Set the state correctly, as if the abstraction is broken. - */ - - if (ctype_isRealPointer (xrt) && - (b = ctype_realType (ctype_baseArrayPtr (xrt)), - ctype_isStructorUnion (b))) - { - uentry fentry = uentryList_lookupField (ctype_getFields (b), f); - ret->typ = uentry_getType (fentry); - ret->sref = sRef_makeArrow (s->sref, uentry_rawName (fentry)); - } - else - { - ret->typ = ctype_unknown; - ret->sref = sRef_undefined; - } - } - else /* not a struct, union or abstract */ - { - if (ctype_isUnknown (tr)) { - cstring sn = cstring_copy (f); - - DPRINTF (("Here: %s", exprNode_unparse (s))); - - exprNode_checkUse (ret, s->sref, s->loc); - exprNode_checkUse (ret, sRef_makePointer (s->sref), s->loc); - - cstring_markOwned (sn); - ret->sref = sRef_makeArrow (s->sref, sn); - - ret->kind = XPR_ARROW; - return (ret); - } else { - voptgenerror - (FLG_TYPE, - message ("Arrow access field of non-struct or union " - "pointer (%t): %s->%s", - t, exprNode_unparse (s), f), - s->loc); - - ret->typ = ctype_unknown; - ret->sref = sRef_undefined; - } - } - } - } - else /* its not a pointer */ - { - if (!ctype_isUnknown (tr)) - { - voptgenerror - (FLG_TYPE, - message ("Arrow access of non-pointer (%t): %s->%s", - t, exprNode_unparse (s), f), - s->loc); - - ret->typ = ctype_unknown; - ret->sref = sRef_undefined; - } - else - { - cstring sn = cstring_copy (f); - - DPRINTF (("Here: %s", exprNode_unparse (s))); - - exprNode_checkUse (ret, s->sref, s->loc); - exprNode_checkUse (ret, sRef_makePointer (s->sref), s->loc); - - cstring_markOwned (sn); - ret->sref = sRef_makeArrow (s->sref, sn); - - ret->kind = XPR_ARROW; - return (ret); - } - } - - return (ret); - } - BADEXIT; + exprNode res = exprNode_arrowAccessAux (s, lltok_getLoc (arrow), f); + lltok_release (arrow); + return res; } /* @@ -3608,52 +4396,58 @@ exprNode_postOp (/*@only@*/ exprNode e, /*@only@*/ lltok op) exprNode_checkModify (e, ret); /* added 7/11/2000 D.L */ - - updateEnvironmentForPostOp (e); - - /* start modifications */ - /* added by Seejo on 4/16/2000 */ + /*@i223*/ + /*DRL 6/8/01 I decided to disable all Splint warnings here since the code + probably needs a rewrite any way */ - /* 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); - } - } - } + /*@i65234@*/ + /*@ignore@*/ - /* 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; } @@ -3708,7 +4502,6 @@ exprNode_preOp (/*@only@*/ exprNode e, /*@only@*/ lltok op) { case INC_OP: case DEC_OP: /* should also check modification! */ - if (sRef_isMacroParamRef (e->sref)) { voptgenerror @@ -3810,7 +4603,7 @@ exprNode_preOp (/*@only@*/ exprNode e, /*@only@*/ lltok op) case TEXCL: /* maybe this should be restricted */ guardSet_flip (ret->guards); - if (ctype_isRealBool (te)) + if (ctype_isRealBool (te) || ctype_isUnknown (te)) { ; } @@ -3822,7 +4615,7 @@ exprNode_preOp (/*@only@*/ exprNode e, /*@only@*/ lltok op) { ret->guards = guardSet_addFalseGuard (ret->guards, e->sref); } - + voptgenerror2n (FLG_BOOLOPS, FLG_PTRNEGATE, message ("Operand of %s is non-boolean (%t): %s", @@ -3916,8 +4709,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 @@ -3971,7 +4767,7 @@ ctype sizeof_resultType (void) } else { - sizet = ctype_ulint; + sizet = ctype_ulint; } } return sizet; @@ -4336,6 +5132,11 @@ exprNode_cast (/*@only@*/ lltok tok, /*@only@*/ exprNode e, /*@only@*/ qtype q) } else { + DPRINTF (("No access to: %s / %d", + ctype_unparse (bc), ctype_typeId (bc))); + DPRINTF (("Context %s %s", + bool_unparse (context_inFunctionLike ()), + context_unparse ())); voptgenerror (FLG_ABSTRACT, message ("Cast to abstract type %t: %s", bc, @@ -4474,6 +5275,7 @@ exprNode_makeOp (/*@keep@*/ exprNode e1, /*@keep@*/ exprNode e2, } ret->val = multiVal_undefined; + ret->kind = XPR_OP; ret->edata = exprData_makeOp (e1, e2, op); @@ -4502,6 +5304,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); @@ -4566,7 +5369,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; @@ -4574,7 +5388,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)) @@ -4591,6 +5416,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)) { @@ -4605,56 +5444,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); @@ -4698,61 +5533,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; } @@ -4763,7 +5593,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: @@ -4775,47 +5605,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)) { @@ -4844,6 +5707,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))) { @@ -4912,6 +5779,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 @@ -4947,6 +5817,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) && @@ -5042,10 +5927,10 @@ exprNode_makeOp (/*@keep@*/ exprNode e1, /*@keep@*/ exprNode e2, default: { llfatalbug (cstring_makeLiteral - ("There has been a problem in the parser. This is due to a bug " - "in either lclint, bison or gcc version 2.95 optimizations, " - "but it has not been confirmed. Please try rebuidling LCLint " - "without the -O option.")); + ("There has been a problem in the parser. This is believed to result " + "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.")); } } } @@ -5094,7 +5979,7 @@ void exprNode_checkAssignMod (exprNode e1, exprNode ret) sRef_unparseFull (ref))); if (sRef_isObserver (ref) - || ((sRef_isFileStatic (ref) || sRef_isGlobal (ref)) + || ((sRef_isFileStatic (ref) || sRef_isFileOrGlobalScope (ref)) && ctype_isArray (ctype_realType (sRef_getType (ref))))) { sRef base = sRef_getBase (ref); @@ -5115,11 +6000,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]", @@ -5131,7 +6016,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); @@ -5215,6 +6115,8 @@ exprNode_assign (/*@only@*/ exprNode e1, sRef_unparse (e1->sref)), g_currentloc); } + + exprNode_checkAssignMod (e1, ret); /* evans 2001-07-22 */ } } else @@ -5229,7 +6131,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)) { @@ -5246,12 +6158,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 @@ -5259,7 +6184,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); } } @@ -5285,11 +6210,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) { @@ -5440,7 +6365,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)); } } @@ -5646,6 +6571,7 @@ exprNode_mustBreak (exprNode e) { return e->mustBreak; } + return FALSE; } @@ -5675,6 +6601,8 @@ exprNode exprNode_concat (/*@only@*/ exprNode e1, /*@only@*/ exprNode e2) { exprNode ret = exprNode_createPartialCopy (e1); + DPRINTF (("Concat: %s / %s", exprNode_unparse (e1), exprNode_unparse (e2))); + ret->edata = exprData_makePair (e1, e2); ret->kind = XPR_STMTLIST; @@ -5766,7 +6694,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); } } @@ -5774,7 +6702,7 @@ exprNode exprNode_concat (/*@only@*/ exprNode e1, /*@only@*/ exprNode e2) } exprNode_mergeUSs (ret, e2); - ret = exprNode_mergeEnvironments (ret, e1, e2); + usymtab_setExitCode (ret->exitCode); if (ret->mustBreak) @@ -5782,12 +6710,14 @@ exprNode exprNode_concat (/*@only@*/ exprNode e1, /*@only@*/ exprNode e2) usymtab_setMustBreak (); } + DPRINTF (("==> %s", exprNode_unparse (ret))); return ret; } exprNode exprNode_createTok (/*@only@*/ lltok t) { - exprNode ret = exprNode_create (ctype_unknown); + exprNode ret; /*@i23 if on same line, bad things happen...!@*/ + ret = exprNode_create (ctype_unknown); ret->kind = XPR_TOK; ret->edata = exprData_makeTok (t); return ret; @@ -5797,7 +6727,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)); @@ -5852,6 +6782,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); @@ -5863,8 +6823,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; } @@ -5873,6 +6835,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) { @@ -5891,6 +6859,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; @@ -5924,7 +6913,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 { @@ -5940,8 +6929,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)) @@ -6046,7 +7035,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 { @@ -6070,7 +7059,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); @@ -6125,6 +7114,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) @@ -6134,7 +7126,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)); } @@ -6162,7 +7154,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); @@ -6229,6 +7221,7 @@ checkSwitchExpr (exprNode test, /*@dependent@*/ exprNode e, /*@out@*/ bool *allp g_currentloc); enumNameSList_free (unused); + *allpaths = FALSE; /* evans 2002-01-01 */ } else { @@ -6411,12 +7404,6 @@ exprNode exprNode_while (/*@keep@*/ exprNode t, /*@keep@*/ exprNode b) { exprNode ret; bool emptyErr = FALSE; - char *s; - // s = exprNode_generateConstraints (t); - // printf("pred: %s\n", s); - // s = exprNode_generateConstraints (b); - //printf ("body: %s\n", s); - //constraintList_print(b->constraints); if (context_maybeSet (FLG_WHILEEMPTY)) { @@ -6456,7 +7443,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 { @@ -6501,7 +7488,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)); } @@ -6547,12 +7534,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 { @@ -6562,11 +7552,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); @@ -6576,9 +7570,9 @@ exprNode exprNode_doWhile (/*@only@*/ exprNode b, /*@only@*/ exprNode t) ** forgot the copy's --- why wasn't this detected?? */ - ret->sets = sRefSet_copy (ret->sets, b->sets); - ret->msets = sRefSet_copy (ret->msets, b->msets); - ret->uses = sRefSet_copy (ret->uses, b->uses); + ret->sets = sRefSet_copyInto (ret->sets, b->sets); + ret->msets = sRefSet_copyInto (ret->msets, b->msets); + ret->uses = sRefSet_copyInto (ret->uses, b->uses); /* left this out --- causes and aliasing bug (infinite loop) should be detected?? */ @@ -6587,9 +7581,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; */ } } @@ -6597,7 +7598,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) @@ -6653,14 +7725,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); @@ -6673,9 +7744,9 @@ exprNode exprNode_for (/*@keep@*/ exprNode inc, /*@keep@*/ exprNode body) context_clearMessageAnnote (); - ret->uses = sRefSet_copy (ret->uses, inc->uses); - ret->sets = sRefSet_copy (ret->sets, inc->sets); - ret->msets = sRefSet_copy (ret->msets, inc->msets); + ret->uses = sRefSet_copyInto (ret->uses, inc->uses); + ret->sets = sRefSet_copyInto (ret->sets, inc->sets); + ret->msets = sRefSet_copyInto (ret->msets, inc->msets); } } @@ -7032,7 +8103,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 { @@ -7111,6 +8182,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, @@ -7125,12 +8200,43 @@ 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)) + { + int nelements = long_toInt (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) != nelements) + { + hasError = optgenerror + (exprNodeList_size (vals) > 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); @@ -7195,7 +8301,7 @@ static bool exprNode_checkOneInit (/*@notnull@*/ exprNode el, exprNode val) hasError = optgenerror (FLG_FULLINITBLOCK, message ("Initializer block for " - "%s has %d field%p, but %s has %d field%p: %q", + "%s has %d field%&, but %s has %d field%&: %q", exprNode_unparse (el), exprNodeList_size (vals), ctype_unparse (t1), @@ -7208,7 +8314,7 @@ static bool exprNode_checkOneInit (/*@notnull@*/ exprNode el, exprNode val) hasError = optgenerror (FLG_TYPE, message ("Initializer block for " - "%s has %d field%p, but %s has %d field%p: %q", + "%s has %d field%&, but %s has %d field%&: %q", exprNode_unparse (el), exprNodeList_size (vals), ctype_unparse (t1), @@ -7223,8 +8329,9 @@ static bool exprNode_checkOneInit (/*@notnull@*/ exprNode el, exprNode val) { uentry thisfield = uentryList_getN (fields, i); exprNode newel = - exprNode_fieldAccess (exprNode_fakeCopy (el), - uentry_getName (thisfield)); + exprNode_fieldAccessAux (exprNode_fakeCopy (el), + exprNode_loc (el), + uentry_getName (thisfield)); if (exprNode_isDefined (newel)) { @@ -7240,6 +8347,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 @@ -7272,37 +8423,109 @@ static bool exprNode_checkOneInit (/*@notnull@*/ exprNode el, exprNode val) return hasError; } +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)); + ret = exprNode_createId (ue); + + /*@i723 don't do this...but why? */ +# if 0 + ct = ctype_realishType (ret->typ); + + DPRINTF (("Type: %s", ctype_unparse (ret->typ))); + + if (ctype_isUnknown (ct)) + { + if (uentry_isAnyTag (ue)) + { + voptgenerror + (FLG_IMPTYPE, + message ("%s used but not previously declared: %s", + uentry_ekindName (ue), + idDecl_getName (t)), + g_currentloc); + + } + else + { + voptgenerror + (FLG_IMPTYPE, + message ("Variable has unknown (implicitly int) type: %s", + idDecl_getName (t)), + g_currentloc); + } + + ct = ctype_int; + } +# endif + } + else + { + 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); + + /* + ** No error - this happens in old style declarations: + + voptgenerror + (FLG_UNRECOG, + message ("Unrecognized identifier in intializer: %s", idDecl_observeId (t)), + g_currentloc); + + ** + */ + } + + exprData_free (ret->edata, ret->kind); + ret->edata = exprData_undefined; + + ret->exitCode = XK_NEVERESCAPE; + ret->mustBreak = FALSE; + ret->kind = XPR_INIT; + return ret; +} + +exprNode exprNode_makeEmptyInitialization (/*@only@*/ idDecl t) +{ + exprNode ret = exprNode_makeInitializationAux (t); + llassert (ret->edata == exprData_undefined); + ret->edata = exprData_makeInit (t, exprNode_undefined); + return ret; +} + exprNode exprNode_makeInitialization (/*@only@*/ idDecl t, /*@only@*/ exprNode e) { uentry ue = usymtab_lookup (idDecl_observeId (t)); - bool isUsed = uentry_isUsed (ue); - exprNode ret = exprNode_fromIdentifierAux (ue); - ctype ct = ctype_realishType (ret->typ); - fileloc loc; + exprNode ret = exprNode_makeInitializationAux (t); + fileloc loc = exprNode_loc (e); - if (ctype_isUnknown (ct)) - { - voptgenerror (FLG_IMPTYPE, - message ("Variable has unknown (implicitly int) type: %s", - idDecl_getName (t)), - exprNode_isDefined (e) ? exprNode_loc (e) : g_currentloc); - - ct = ctype_int; - } - if (exprNode_isError (e)) { e = exprNode_createUnknown (); - loc = g_currentloc; + idDecl_free (t); /* error: assume initializer is defined */ - sRef_setDefined (ret->sref, loc); + sRef_setDefined (ret->sref, g_currentloc); } else { - loc = exprNode_loc (e); - + ctype ct = ctype_realishType (ret->typ); + /* ** evs - 9 Apr 1995 ** @@ -7311,6 +8534,9 @@ exprNode exprNode_makeInitialization (/*@only@*/ idDecl t, ** int x = 3, y = x ? */ + exprData_free (ret->edata, ret->kind); + ret->edata = exprData_makeInit (t, e); + exprNode_checkUse (ret, e->sref, e->loc); if (ctype_isUnknown (e->typ) && uentry_isValid (ue)) @@ -7325,7 +8551,7 @@ exprNode exprNode_makeInitialization (/*@only@*/ idDecl t, { sRef_setDefState (lhs->sref, SS_PARTIAL, fileloc_undefined); } - + (void) exprNode_checkOneInit (lhs, e); if (uentry_isStatic (ue)) @@ -7348,8 +8574,8 @@ exprNode exprNode_makeInitialization (/*@only@*/ idDecl t, (void) gentypeerror (exprNode_getType (e), e, exprNode_getType (ret), ret, message - ("Variable %s initialized to type %t, expects %t: %s", - exprNode_unparse (ret), exprNode_getType (e), + ("Variable %q initialized to type %t, expects %t: %s", + uentry_getName (ue), exprNode_getType (e), exprNode_getType (ret), exprNode_unparse (e)), e->loc); @@ -7377,23 +8603,9 @@ exprNode exprNode_makeInitialization (/*@only@*/ idDecl t, } else { - if (!isUsed) /* could be @unused@-qualified variable */ - { - uentry_setNotUsed (ue); - } + ; } - ret->exitCode = XK_NEVERESCAPE; - ret->mustBreak = FALSE; - - /* - ** Must be before new kind is assigned! - */ - - exprData_free (ret->edata, ret->kind); - - ret->kind = XPR_INIT; - ret->edata = exprData_makeInit (t, e); exprNode_mergeUSs (ret, e); return ret; } @@ -7415,23 +8627,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)); } @@ -7482,7 +8694,7 @@ exprNode_iterNewId (/*@only@*/ cstring s) 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; @@ -7536,6 +8748,8 @@ exprNode_iterNewId (/*@only@*/ cstring s) cstring_free (s); + + exprNode_defineConstraints(e); return (e); } @@ -7556,7 +8770,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); @@ -7564,7 +8778,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); @@ -7607,7 +8821,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)) @@ -7721,7 +8935,7 @@ exprNode_unparseFirst (exprNode e) } /*@observer@*/ cstring -exprNode_unparse (exprNode e) +exprNode_unparse (/*@temp@*/ exprNode e) { if (exprNode_isError (e)) { @@ -8003,13 +9217,17 @@ static /*@only@*/ exprNode exprNode_effect (exprNode e) break; case XPR_FACCESS: - ret = exprNode_fieldAccess (exprNode_effect (exprData_getFieldNode (data)), - cstring_copy (exprData_getFieldName (data))); + ret = exprNode_fieldAccessAux + (exprNode_effect (exprData_getFieldNode (data)), + exprNode_loc (exprData_getFieldNode (data)), + cstring_copy (exprData_getFieldName (data))); break; case XPR_ARROW: - ret = exprNode_arrowAccess (exprNode_effect (exprData_getFieldNode (data)), - cstring_copy (exprData_getFieldName (data))); + ret = exprNode_arrowAccessAux + (exprNode_effect (exprData_getFieldNode (data)), + exprNode_loc (exprData_getFieldNode (data)), + cstring_copy (exprData_getFieldName (data))); break; case XPR_STRINGLITERAL: @@ -8063,6 +9281,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: @@ -8104,7 +9325,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: @@ -8117,7 +9337,6 @@ static /*@observer@*/ cstring exprNode_rootVarName (exprNode e) return ret; } - static /*@only@*/ cstring exprNode_doUnparse (exprNode e) { cstring ret; @@ -8316,17 +9535,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: @@ -8347,9 +9580,16 @@ static /*@only@*/ cstring exprNode_doUnparse (exprNode e) break; case XPR_INIT: - ret = message ("%s = %s", - idDecl_getName (exprData_getInitId (data)), - exprNode_unparse (exprData_getInitNode (data))); + if (exprNode_isError (exprData_getInitNode (data))) + { + ret = message ("%q", idDecl_unparseC (exprData_getInitId (data))); + } + else + { + ret = message ("%q = %s", + idDecl_unparseC (exprData_getInitId (data)), + exprNode_unparse (exprData_getInitNode (data))); + } break; case XPR_FACCESS: @@ -8365,7 +9605,14 @@ static /*@only@*/ cstring exprNode_doUnparse (exprNode e) break; case XPR_STRINGLITERAL: - ret = cstring_copy (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: @@ -8380,6 +9627,13 @@ static /*@only@*/ cstring exprNode_doUnparse (exprNode e) return ret; } +bool +exprNode_isInitializer (exprNode e) +{ + return (exprNode_isDefined (e) + && e->kind == XPR_INIT); +} + bool exprNode_isCharLit (exprNode e) { @@ -8487,7 +9741,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)) { @@ -8570,6 +9839,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)); } @@ -8719,7 +9992,7 @@ exprNode_mergeCondUSs (exprNode res, exprNode other1, exprNode other2) */ static void -exprNode_addUse (exprNode e, sRef s) +exprNode_addUse (exprNode e, /*@exposed@*/ sRef s) { if (exprNode_isDefined (e)) { @@ -8728,7 +10001,7 @@ exprNode_addUse (exprNode e, sRef s) } void -exprNode_checkUse (exprNode e, sRef s, fileloc loc) +exprNode_checkUse (exprNode e, /*@exposed@*/ sRef s, fileloc loc) { if (sRef_isKnown (s) && !sRef_isConst (s)) { @@ -8738,7 +10011,7 @@ exprNode_checkUse (exprNode e, sRef s, fileloc loc) DPRINTF (("Check use: %s / %s", exprNode_unparse (e), sRef_unparse (s))); - + exprNode_addUse (e, s); if (!context_inProtectVars ()) @@ -8755,7 +10028,10 @@ exprNode_checkUse (exprNode e, 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))); if (!(ynm_toBoolStrict (readable))) { @@ -8763,6 +10039,7 @@ exprNode_checkUse (exprNode e, 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; @@ -8778,6 +10055,7 @@ exprNode_checkUse (exprNode e, sRef s, fileloc loc) if (!sRef_isPartial (s)) { + DPRINTF (("Defining! %s", sRef_unparseFull (s))); sRef_setDefined (s, fileloc_undefined); } } @@ -8849,7 +10127,7 @@ exprNode_checkUse (exprNode e, sRef s, fileloc loc) } else { - DPRINTF (("HERE: %s", sRef_unparse (errorRef))); + DPRINTF (("HERE: %s", sRef_unparseFull (errorRef))); voptgenerror (FLG_USEDEF, @@ -8858,6 +10136,8 @@ exprNode_checkUse (exprNode e, sRef s, fileloc loc) sRef_unparseOpt (errorRef), cstring_makeLiteral (errorMaybe ? "may be " : "")), loc); + + DPRINTF (("Error: %s", sRef_unparseFull (errorRef))); } sRef_setDefined (errorRef, loc); @@ -8874,7 +10154,7 @@ exprNode_checkUse (exprNode e, sRef s, fileloc loc) } static void -checkSafeUse (exprNode e, sRef s) +checkSafeUse (exprNode e, /*@exposed@*/ sRef s) { if (exprNode_isDefined (e) && sRef_isKnown (s)) { @@ -8892,7 +10172,7 @@ exprNode_checkSetAny (exprNode e, /*@dependent@*/ cstring name) } void -exprNode_checkSet (exprNode e, sRef s) +exprNode_checkSet (exprNode e, /*@exposed@*/ sRef s) { sRef defines = sRef_undefined; @@ -8914,8 +10194,7 @@ exprNode_checkSet (exprNode e, sRef s) } if (sRef_isMeaningful (s)) - { - + { if (sRef_isDead (s)) { sRef base = sRef_getBaseSafe (s); @@ -8995,7 +10274,7 @@ exprNode_checkSet (exprNode e, sRef s) } void -exprNode_checkMSet (exprNode e, sRef s) +exprNode_checkMSet (exprNode e, /*@exposed@*/ sRef s) { if (sRef_isValid (s) && !sRef_isNothing (s)) { @@ -9110,7 +10389,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); } } @@ -9155,7 +10434,7 @@ static void if (specialArgs == 0 || (paramno < specialArgs)) { - checkOneArg (ucurrent, current, fcn, isSpec, paramno, nargs); + checkOneArg (ucurrent, current, fcn, isSpec, paramno, nargs); if (context_maybeSet (FLG_ALIASUNIQUE)) { @@ -9190,7 +10469,7 @@ static void sRef fb; sRef rb = sRef_getRootBase (s); - if (sRef_isGlobal (rb)) + if (sRef_isFileOrGlobalScope (rb)) { context_usedGlobal (rb); } @@ -9277,7 +10556,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 { @@ -9485,9 +10766,12 @@ checkOneRepExpose (sRef ysr, sRef base, sRef s2b) { if (!(sRef_isOnly (ysr) || sRef_isKeep (ysr) - || sRef_isOwned (ysr) || sRef_isExposed (ysr))) + || sRef_isOwned (ysr) + || sRef_isExposed (ysr))) { - if (sRef_isAnyParam (base) && !sRef_isExposed (base)) + if (sRef_isAnyParam (base) && !sRef_isExposed (base) + && !sRef_isObserver (base)) /* evans 2001-07-11: added isObserver */ + { if (sRef_isIReference (ysr)) { @@ -9552,7 +10836,7 @@ checkOneRepExpose (sRef ysr, sRef base, } } - if (sRef_isGlobal (s2b)) + if (sRef_isFileOrGlobalScope (s2b)) { if (sRef_sameName (base, sRef_getRootBase (e2->sref))) { @@ -9586,6 +10870,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))) { @@ -9652,7 +10940,7 @@ doAssign (/*@notnull@*/ exprNode e1, /*@notnull@*/ exprNode e2, bool isInit) } } - if (sRef_isGlobal (s2b)) + if (sRef_isFileOrGlobalScope (s2b)) { voptgenerror (FLG_ASSIGNEXPOSE, @@ -9693,11 +10981,13 @@ doAssign (/*@notnull@*/ exprNode e1, /*@notnull@*/ exprNode e2, bool isInit) { if (isInit) { - checkInitTransfer (e1, e2); + DPRINTF (("Check init: %s / %s", + exprNode_unparse (e1), exprNode_unparse (e2))); + transferChecks_initialization (e1, e2); } else { - checkAssignTransfer (e1, e2); + transferChecks_assign (e1, e2); } } else @@ -9731,15 +11021,20 @@ doAssign (/*@notnull@*/ exprNode e1, /*@notnull@*/ exprNode e2, bool isInit) } } - if (isInit && sRef_isGlobal (e1->sref)) + if (exprNode_isStringLiteral (e2)) + { + exprNode_checkStringLiteralLength (exprNode_getType (e1), e2); + } + + if (isInit && sRef_isFileOrGlobalScope (e1->sref)) { ; } else { + DPRINTF (("Update aliases: %s / %s", exprNode_unparse (e1), exprNode_unparse (e2))); updateAliases (e1, e2); } - updateEnvironment (e1, e2); } static void @@ -9803,13 +11098,27 @@ static void updateAliases (/*@notnull@*/ exprNode e1, /*@notnull@*/ exprNode e2) if (!ctype_isRealSU (t1)) { + DPRINTF (("Copying real! %s", ctype_unparse (t1))); sRef_copyRealDerivedComplete (s1, s2); } + else + { + /* + ** Fields should alias + */ + + DPRINTF (("Not COPYING!: %s", ctype_unparse (t1))); + } if (ctype_isMutable (t1) && sRef_isKnown (s1)) { usymtab_clearAlias (s1); usymtab_addMustAlias (s1, s2); + DPRINTF (("Add must alias: %s / %s", sRef_unparse (s1), sRef_unparse (s2))); + } + else + { + DPRINTF (("Not mutable: %s", ctype_unparse (t1))); } if (sRef_possiblyNull (s1) && usymtab_isGuarded (s1)) @@ -9954,21 +11263,22 @@ long exprNode_getLongValue (exprNode e) { } else { + /*@!! BADBRANCH;*/ value = 0; } return value; } -fileloc exprNode_getfileloc (exprNode p_e) +/*@observer@*/ fileloc exprNode_getfileloc (exprNode p_e) { - if (p_e) - return fileloc_copy ( p_e->loc ); + if (exprNode_isDefined (p_e) ) + return ( p_e->loc ); else return fileloc_undefined; } -fileloc exprNode_getNextSequencePoint (exprNode e) +/*@only@*/ fileloc exprNode_getNextSequencePoint (exprNode e) { /* ** Returns the location of the sequence point following e. @@ -9978,24 +11288,15 @@ fileloc exprNode_getNextSequencePoint (exprNode e) if (exprNode_isDefined (e) && e->kind == XPR_STMT) { lltok t = exprData_getUopTok (e->edata); - return lltok_getLoc (t); + return fileloc_copy(lltok_getLoc (t)); } else { - #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; } } - -/*drl added - */ -exprNode exprNode_fakeCopy (exprNode e) -{ - /*@-temptrans@*/ /*@-retalias@*/ - return e; - /*@=temptrans@*/ /*@=retalias@*/ -} - exprNode exprNode_createNew(ctype c) { exprNode ret; @@ -10004,3 +11305,8 @@ exprNode exprNode_createNew(ctype c) return ret; } + +bool exprNode_isInitBlock (exprNode e) +{ + return (exprNode_isDefined(e) && e->kind == XPR_INITBLOCK); +}