X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/e5081f8c08424e4511d50a3b1fc187666c95852c..419f7a7a4b388dfc03c75bebaffcf97116ea0410:/src/exprNode.c diff --git a/src/exprNode.c b/src/exprNode.c index 828ef6c..9ddccbe 100644 --- a/src/exprNode.c +++ b/src/exprNode.c @@ -1,6 +1,6 @@ /* ** Splint - annotation-assisted static program checker -** Copyright (C) 1994-2002 University of Virginia, +** Copyright (C) 1994-2003 University of Virginia, ** Massachusetts Institute of Technology ** ** This program is free software; you can redistribute it and/or modify it @@ -30,6 +30,7 @@ # include "basic.h" # include "cgrammar.h" # include "cscanner.h" +# include "cscannerHelp.h" # include "cgrammar_tokens.h" # include "exprChecks.h" @@ -1010,6 +1011,7 @@ exprNode exprNode_createId (/*@observer@*/ uentry c) } e->guards = guardSet_new (); + e->sets = sRefSet_new (); e->msets = sRefSet_new (); e->uses = sRefSet_new (); @@ -1036,7 +1038,7 @@ exprNode_fromIdentifier (/*@observer@*/ uentry c) if (context_justPopped ()) /* watch out! c could be dead */ { - uentry ce = usymtab_lookupSafe (cscanner_observeLastIdentifier ()); + uentry ce = usymtab_lookupSafe (cscannerHelp_observeLastIdentifier ()); if (uentry_isValid (ce)) { @@ -1246,18 +1248,21 @@ exprNode_arrayFetch (/*@only@*/ exprNode e1, /*@only@*/ exprNode e2) { if (!usymtab_isGuarded (arr->sref)) { - if (optgenerror (FLG_NULLDEREF, - message ("Index of %s pointer %q: %s", - sRef_nullMessage (arr->sref), - sRef_unparse (arr->sref), - exprNode_unparse (arr)), - arr->loc)) - { - DPRINTF (("ref: %s", sRef_unparseFull (arr->sref))); - sRef_showNullInfo (arr->sref); - - /* suppress future messages */ - sRef_setNullError (arr->sref); + if (!context_inSizeof() ) + { + if (optgenerror (FLG_NULLDEREF, + message ("Index of %s pointer %q: %s", + sRef_nullMessage (arr->sref), + sRef_unparse (arr->sref), + exprNode_unparse (arr)), + arr->loc)) + { + DPRINTF (("ref: %s", sRef_unparseFull (arr->sref))); + sRef_showNullInfo (arr->sref); + + /* suppress future messages */ + sRef_setNullError (arr->sref); + } } } } @@ -1326,6 +1331,15 @@ exprNode_arrayFetch (/*@only@*/ exprNode e1, /*@only@*/ exprNode e2) exprNode_unparse (e1), exprNode_unparse (e2)), arr->loc); } + else if (ctype_isNumAbstract (rt)) + { + vnoptgenerror + (FLG_NUMABSTRACTINDEX, + message ("Array fetch using numabstract type, %t: %s[%s]", + ind->typ, + exprNode_unparse (e1), exprNode_unparse (e2)), + arr->loc); + } else { voptgenerror @@ -1619,11 +1633,9 @@ checkPrintfArgs (/*@notnull@*/ /*@dependent@*/ exprNode f, uentry fcn, 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 */ @@ -1919,9 +1931,12 @@ checkScanfArgs (/*@notnull@*/ /*@dependent@*/ exprNode f, uentry fcn, case 'i': case 'd': + expecttype = ctype_makePointer (ctype_combine (ctype_int, modtype)); + /*@switchbreak@*/ break; + case 'x': case 'X': /* unsigned int */ - expecttype = ctype_makePointer (ctype_combine (ctype_int, modtype)); + expecttype = ctype_makePointer (ctype_combine (ctype_uint, modtype)); /*@switchbreak@*/ break; case 'e': @@ -2232,7 +2247,7 @@ checkMessageArgs (/*@notnull@*/ /*@dependent@*/ exprNode f, codetext, expecttype, a->typ, exprNode_unparse (a)), a->loc)) - { + { if (fileloc_isDefined (formatloc) && context_getFlag (FLG_SHOWCOL)) { @@ -2580,7 +2595,7 @@ static int f->guards = guardSet_union (f->guards, a->guards); DPRINTF (("match arg: %s / %s", ctype_unparse (ct), ctype_unparse (a->typ))); - + if (!(exprNode_matchArgType (ct, a))) { DPRINTF (("Args mismatch!")); @@ -2914,7 +2929,7 @@ checkGlobMods (/*@notnull@*/ /*@dependent@*/ exprNode f, uentry_unparse (le))); params = ctype_argsFunction (ct); - return; /*@32 ! remove this? */ + return; /* No checking for non-function */ } /* @@ -3697,7 +3712,7 @@ checkRequiresClause (uentry le, exprNode f, exprNodeList args) if (sRef_isResult (sRef_getRootBase (sel))) { - ; /*@i423 what do we do about results */ + ; /* what do we do about results? */ } else { @@ -4412,12 +4427,6 @@ exprNode_postOp (/*@only@*/ exprNode e, /*@only@*/ lltok op) exprNode_checkModify (e, ret); /* added 7/11/2000 D.L */ - /*@i223*/ - /*DRL 6/8/01 I decided to disable all Splint warnings here since the code - probably needs a rewrite any way */ - - /*@i65234@*/ - /*@ignore@*/ /* updateEnvironmentForPostOp (e); */ @@ -4451,6 +4460,8 @@ exprNode_postOp (/*@only@*/ exprNode e, /*@only@*/ lltok op) printf ("ret->sref is Possibly Null Terminated\n"); else if (sRef_isNotNullTerminated (ret->sref)) printf ("ret->sref is Not Null Terminated\n"); + else + {} } } @@ -4462,7 +4473,6 @@ exprNode_postOp (/*@only@*/ exprNode e, /*@only@*/ lltok op) } } } - /*@end@*/ /* end modifications */ return ret; @@ -5003,8 +5013,8 @@ exprNode_cast (/*@only@*/ lltok tok, /*@only@*/ exprNode e, /*@only@*/ qtype q) ret->edata = exprData_makeCast (tok, e, q); ret->sref = sRef_copy (e->sref); - - DPRINTF (("Cast 2: -> %s", sRef_unparseFull (ret->sref))); + + DPRINTF (("Cast: -> %s", sRef_unparseFull (ret->sref))); if (!sRef_isConst (e->sref)) { @@ -5360,10 +5370,14 @@ exprNode_makeOp (/*@keep@*/ exprNode e1, /*@keep@*/ exprNode e2, if (opid == OR_OP) { + exprNode_produceGuards (e2); ret->guards = guardSet_or (ret->guards, e2->guards); } else if (opid == AND_OP) { + exprNode_produceGuards (e2); /* evans 2003-08-13: need to produce guards for expression */ + /* Shouldn't this have already happened? */ + DPRINTF (("Anding guards: %s / %s", guardSet_unparse (ret->guards), guardSet_unparse (e2->guards))); ret->guards = guardSet_and (ret->guards, e2->guards); } else @@ -5588,34 +5602,38 @@ exprNode_makeOp (/*@keep@*/ exprNode e1, /*@keep@*/ exprNode e2, 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 !) */ + if (multiVal_isDefined (e1->val)) + { + int val = (int) multiVal_forceInt (e1->val); - sRef_setSize (ret->sref, sRef_getSize(e2->sref) - 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); + } + } + } - 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); + } } } - } - - /* 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); @@ -5811,12 +5829,24 @@ exprNode_makeOp (/*@keep@*/ exprNode e1, /*@keep@*/ exprNode e2, } else { - voptgenerror - (FLG_REALCOMPARE, - message ("Dangerous comparison involving %s types: %s", - ctype_unparse (rtype), - exprNode_unparse (ret)), - ret->loc); + if (opid == EQ_OP || opid == NE_OP) + { + voptgenerror + (FLG_REALCOMPARE, + message ("Dangerous equality comparison involving %s types: %s", + ctype_unparse (rtype), + exprNode_unparse (ret)), + ret->loc); + } + else + { + voptgenerror + (FLG_REALRELATECOMPARE, + message ("Possibly dangerous relational comparison involving %s types: %s", + ctype_unparse (rtype), + exprNode_unparse (ret)), + ret->loc); + } } } /*@fallthrough@*/ @@ -6466,8 +6496,8 @@ exprNode_vaArg (/*@only@*/ lltok tok, /*@only@*/ exprNode arg, /*@only@*/ qtype */ if (!ctype_isUA (targ) || - (!usymId_equal (ctype_typeId (targ), - usymtab_getTypeId (cstring_makeLiteralTemp ("va_list"))))) + (!typeId_equal (ctype_typeId (targ), + usymtab_getTypeId (cstring_makeLiteralTemp ("va_list"))))) { voptgenerror (FLG_TYPE, @@ -6778,8 +6808,7 @@ exprNode exprNode_concat (/*@only@*/ exprNode e1, /*@only@*/ exprNode e2) exprNode exprNode_createTok (/*@only@*/ lltok t) { - exprNode ret; /*@i23 if on same line, bad things happen...!@*/ - ret = exprNode_create (ctype_unknown); + exprNode ret = exprNode_create (ctype_unknown); ret->kind = XPR_TOK; ret->edata = exprData_makeTok (t); return ret; @@ -6992,7 +7021,6 @@ exprNode exprNode_if (/*@only@*/ exprNode pred, /*@only@*/ exprNode tclause) exprNode_loc (pred)); } - /*! exprNode_checkPred (cstring_makeLiteralTemp ("if"), pred); */ /*@i523@*/ exprNode_checkUse (pred, pred->sref, pred->loc); if (!exprNode_isError (tclause)) @@ -7121,9 +7149,7 @@ exprNode exprNode_ifelse (/*@only@*/ exprNode pred, exprNode_loc (pred)); } - /*@i3423 exprNode_checkPred (cstring_makeLiteralTemp ("if"), pred);*/ exprNode_checkUse (ret, pred->sref, pred->loc); - exprNode_mergeCondUSs (ret, tclause, eclause); } @@ -8497,37 +8523,6 @@ exprNode_makeInitializationAux (/*@temp@*/ idDecl 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 { @@ -8536,9 +8531,6 @@ exprNode_makeInitializationAux (/*@temp@*/ idDecl t) 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); /* @@ -9920,11 +9912,11 @@ exprNode_matchLiteral (ctype expected, exprNode e) } else if (multiVal_isChar (m)) { - char val = multiVal_forceChar (m); + /*signed? */ char val = multiVal_forceChar (m); if (ctype_isChar (expected)) { - if (ctype_isUnsigned (expected) && ((int)val) < 0) + if (ctype_isUnsigned (expected) && ((int) val) < 0) { return FALSE; } @@ -10192,16 +10184,20 @@ exprNode_checkUse (exprNode e, /*@exposed@*/ sRef s, fileloc loc) { lastRef = errorRef; errorRef = s; + DPRINTF (("Setting ERROR: %s", sRef_unparseFull (s))); deadRef = sRef_isDead (errorRef); unuseable = sRef_isUnuseable (errorRef); errorMaybe = FALSE; } + /* if (!sRef_isPartial (s)) { DPRINTF (("Defining! %s", sRef_unparseFull (s))); - sRef_setDefined (s, fileloc_undefined); + sRef_setDefined (s, loc); + DPRINTF (("Defining! %s", sRef_unparseFull (s))); } + */ } s = sRef_getBaseSafe (s); @@ -10213,6 +10209,7 @@ exprNode_checkUse (exprNode e, /*@exposed@*/ sRef s, fileloc loc) && sRef_isPointer (errorRef)) { errorRef = lastRef; + DPRINTF (("errorRef: %s", sRef_unparseFull (errorRef))); } if (deadRef) @@ -10236,7 +10233,7 @@ exprNode_checkUse (exprNode e, /*@exposed@*/ sRef s, fileloc loc) } else { - DPRINTF (("HERE: %s", sRef_unparse (errorRef))); + DPRINTF (("HERE: %s", sRef_unparseFull (errorRef))); if (optgenerror (FLG_USERELEASED, @@ -10273,13 +10270,16 @@ exprNode_checkUse (exprNode e, /*@exposed@*/ sRef s, fileloc loc) { DPRINTF (("HERE: %s", sRef_unparseFull (errorRef))); - voptgenerror - (FLG_USEDEF, - message ("%q %q%qused before definition", - sRef_unparseKindName (errorRef), - sRef_unparseOpt (errorRef), - cstring_makeLiteral (errorMaybe ? "may be " : "")), - loc); + if (optgenerror + (FLG_USEDEF, + message ("%q %q%qused before definition", + sRef_unparseKindName (errorRef), + sRef_unparseOpt (errorRef), + cstring_makeLiteral (errorMaybe ? "may be " : "")), + loc)) + { + ; + } DPRINTF (("Error: %s", sRef_unparseFull (errorRef))); } @@ -10703,8 +10703,20 @@ static ctype DPRINTF (("No error: [%s] %s / [%s] %s", exprNode_unparse (e1), ctype_unparse (tr1), exprNode_unparse (e2), ctype_unparse (tr2))); + + /* + ** evans 2003-06-15: changed this so if either type is a literal, + ** the other type is used. + ** (Need to look at the ISO C99 rules on this...) + */ - ret = ctype_biggerType (tr1, tr2); + if (exprNode_isNumLiteral (e1)) { + ret = tr2; + } else if (exprNode_isNumLiteral (e2)) { + ret = tr1; + } else { + ret = ctype_biggerType (tr1, tr2); + } } else { @@ -10875,12 +10887,24 @@ abstractOpError (ctype tr1, ctype tr2, lltok op, } else { - return optgenerror - (FLG_ABSTRACT, - message ("Operands of %s are abstract type (%t): %s %s %s", - lltok_unparse (op), tr1, - exprNode_unparse (e1), lltok_unparse (op), exprNode_unparse (e2)), - loc1); + if (lltok_isEqOp (op) || lltok_isNotEqOp (op)) + { + return optgenerror + (FLG_ABSTRACTCOMPARE, + message ("Object equality comparison (%s) on objects of abstract type (%t): %s %s %s", + lltok_unparse (op), tr1, + exprNode_unparse (e1), lltok_unparse (op), exprNode_unparse (e2)), + loc1); + } + else + { + return optgenerror + (FLG_ABSTRACT, + message ("Operands of %s are abstract type (%t): %s %s %s", + lltok_unparse (op), tr1, + exprNode_unparse (e1), lltok_unparse (op), exprNode_unparse (e2)), + loc1); + } } } else @@ -11088,6 +11112,7 @@ doAssign (/*@notnull@*/ exprNode e1, /*@notnull@*/ exprNode e2, bool isInit) ctype ct = sRef_getType (sr); if (ctype_isAbstract (t2) + && !ctype_isNumAbstract (t2) && !(uentry_isMutableDatatype (usymtab_getTypeEntry (ctype_typeId (t2))))) { /* it is immutable, okay to reference */ @@ -11449,31 +11474,22 @@ static void checkUniqueParams (exprNode fcn, } end_exprNodeList_elements; } -long exprNode_getLongValue (exprNode e) { +long exprNode_getLongValue (exprNode e) +{ long value; - - if (exprNode_hasValue (e) - && multiVal_isInt (exprNode_getValue (e))) + + if (exprNode_hasValue (e) && multiVal_isInt (exprNode_getValue (e))) { value = multiVal_forceInt (exprNode_getValue (e)); } else { - /*@!! BADBRANCH;*/ - value = 0; + value = 0; /* Unknown value */ } return value; } -/*@observer@*/ fileloc exprNode_getfileloc (exprNode p_e) -{ - if (exprNode_isDefined (p_e) ) - return ( p_e->loc ); - else - return fileloc_undefined; -} - /*@only@*/ fileloc exprNode_getNextSequencePoint (exprNode e) { /* @@ -11506,3 +11522,32 @@ bool exprNode_isInitBlock (exprNode e) { return (exprNode_isDefined(e) && e->kind == XPR_INITBLOCK); } + +/*drl 3/2/2003 moved this function out of constraint.c */ +exprNode exprNode_copyConstraints (/*@returned@*/ exprNode dst, exprNode src) +{ + + llassert (exprNode_isDefined (dst) ); + llassert (exprNode_isDefined (src) ); + + constraintList_free (dst->ensuresConstraints); + constraintList_free (dst->requiresConstraints); + constraintList_free (dst->trueEnsuresConstraints); + constraintList_free (dst->falseEnsuresConstraints); + + dst->ensuresConstraints = constraintList_copy (src->ensuresConstraints); + dst->requiresConstraints = constraintList_copy (src->requiresConstraints); + dst->trueEnsuresConstraints = constraintList_copy (src->trueEnsuresConstraints); + dst->falseEnsuresConstraints = constraintList_copy (src->falseEnsuresConstraints); + return dst; +} + +void exprNode_revealState (exprNode e) +{ + if (exprNode_isDefined (e)) { + llmsg (message ("%s: State of %s: %s", fileloc_unparse (exprNode_loc (e)), + exprNode_unparse (e), sRef_unparseFull (e->sref))); + } else { + llmsg (message ("%s: Reveal state undefined", fileloc_unparse (g_currentloc))); + } +}