X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/b941db6b4a970ba02fb88f587cf4e40b10c9e286..419f7a7a4b388dfc03c75bebaffcf97116ea0410:/src/exprNode.c diff --git a/src/exprNode.c b/src/exprNode.c index 41b0a6d..9ddccbe 100644 --- a/src/exprNode.c +++ b/src/exprNode.c @@ -1011,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 (); @@ -1330,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 @@ -1623,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 */ @@ -1923,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': @@ -2236,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)) { @@ -2584,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!")); @@ -2918,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 */ } /* @@ -3701,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 { @@ -4416,10 +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 */ - /* updateEnvironmentForPostOp (e); */ @@ -5006,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)) { @@ -5363,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 @@ -5591,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); @@ -5814,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@*/ @@ -6469,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, @@ -6781,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; @@ -6995,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)) @@ -7124,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); } @@ -8500,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 { @@ -8539,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); /* @@ -9923,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; } @@ -10714,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 { @@ -11111,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 */ @@ -11472,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) { /* @@ -11548,3 +11541,13 @@ exprNode exprNode_copyConstraints (/*@returned@*/ exprNode dst, exprNode src) 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))); + } +}