X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/7ebcc5bb1729918edf2ba5b4b9d5a67cdea4afb5..146e25eb1ce61cf25ba20fd3db7b55fc6c74d3ad:/src/uentry.c diff --git a/src/uentry.c b/src/uentry.c index ab662c7..27ccb47 100644 --- a/src/uentry.c +++ b/src/uentry.c @@ -1,5 +1,5 @@ /* -** LCLint - annotation-assisted static program checker +** Splint - annotation-assisted static program checker ** Copyright (C) 1994-2001 University of Virginia, ** Massachusetts Institute of Technology ** @@ -19,7 +19,7 @@ ** ** 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 more information: http://www.splint.org */ /* ** uentry.c @@ -43,6 +43,8 @@ static bool uentry_isReallySpecified (uentry p_e) /*@*/ ; static void uentry_checkIterArgs (uentry p_ue); static cstring uentry_dumpAux (uentry p_v, bool p_isParam); +static void uentry_showWhereLastKind (uentry p_spec) /*@modifies g_msgstream@*/ ; + static void uentry_combineModifies (uentry p_ue, /*@owned@*/ sRefSet p_sr) /*@modifies p_ue@*/ ; @@ -1436,6 +1438,7 @@ uentry_fixupSref (uentry ue) if (uentry_isVariable (ue)) { + /*@i634 ue->sref = sRef_saveCopyShallow (ue->info->var->origsref); */ sRef_setDefState (sr, ue->info->var->defstate, fileloc_undefined); sRef_setNullState (sr, ue->info->var->nullstate, fileloc_undefined); } @@ -1610,7 +1613,19 @@ uentry_setPreconditions (uentry ue, /*@only@*/ functionConstraint preconditions) if (functionConstraint_isDefined (ue->info->fcn->preconditions)) { - BADBRANCH; /* should conjoin constraints? */ + /* drl 11-29-2001 + I changed this so it didn't appear as a Splint bug + among other things this gets triggered when there is + a function with two requires clauses. Now Splint + prints an error and tries to conjoin the lists. + */ + llparseerror + (message ("Duplicate precondition list" + "Attemping the conjoin the requires clauses" + )); + + + /* should conjoin constraints? */ /*@notreached@*/ ue->info->fcn->preconditions = functionConstraint_conjoin (ue->info->fcn->preconditions, preconditions); } @@ -2439,7 +2454,7 @@ uentry_reflectOtherQualifier (/*@notnull@*/ uentry ue, qual qel) { if (optgenerror (FLG_ANNOTATIONERROR, - message ("Meta state annotation %s used in inconsistent context: %q", + message ("Attribute annotation %s used in inconsistent context: %q", qual_unparse (qel), uentry_unparse (ue)), uentry_whereLast (ue))) @@ -3141,6 +3156,7 @@ uentry uentry_makeConstantAux (cstring n, ctype t, uentry_reflectQualifiers (ue, idDecl_getQuals (t)); DPRINTF (("Constant: %s", uentry_unparseFull (ue))); + DPRINTF (("Value: %s", multiVal_unparse (uentry_getConstantValue (ue)))); return ue; } @@ -3259,6 +3275,7 @@ static /*@only@*/ /*@notnull@*/ e->info->var = (uvinfo) dmalloc (sizeof (*e->info->var)); e->info->var->kind = kind; + /*@i523 e->info->var->origsref = sRef_saveCopy (e->sref); */ e->info->var->checked = CH_UNKNOWN; DPRINTF (("Here we are: %s", sRef_unparseFull (e->sref))); @@ -3572,7 +3589,8 @@ uentry_setGlobals (uentry ue, /*@owned@*/ globSet globs) /*@=mustfree@*/ } - /*@i23 ??? + /*@i23*/ + /* ??? - evans 2001-09-09 not sure what's going on here...? if (globSet_hasStatic (globs)) { context_recordFileGlobals (globs); @@ -4161,7 +4179,7 @@ uentry_compare (uentry u1, uentry u2) ** Functions are never equivalent */ - if ((int) u1 < (int) u2) + if (u1 - u2 < 0) /* evans 2001-08-21: was: ((int) u1 < (int) u2), changed to remove gcc warning */ { return -1; } @@ -6142,6 +6160,28 @@ sRef uentry_getSref (uentry e) sRef uentry_getOrigSref (uentry e) { + /*@i523*/ /* evans 2001-09-09 - need to fix this + if (uentry_isValid (e)) + { + if (uentry_isVariable (e)) + { + return e->info->var->origsref; + } + else + { + sRef sr = sRef_copy (uentry_getSref (e)); + + sRef_resetState (sr); + sRef_clearDerived (sr); + return (sr); + } + } + else + { + return sRef_undefined; + } + */ + if (uentry_isValid (e)) { sRef sr = sRef_copy (uentry_getSref (e)); @@ -6571,6 +6611,8 @@ uvinfo_copy (uvinfo u) ret->defstate = u->defstate; ret->checked = u->checked; + /*@i523 ret->origsref = sRef_copy (u->origsref); */ + /* drl added 07-02-001 */ /* copy null terminated information */ @@ -6782,9 +6824,9 @@ KindConformanceError (/*@unique@*/ uentry old, uentry unew, bool mustConform) uentry_getName (unew), ekind_unparseLong (unew->ukind), unew->utype), - uentry_whereDeclared (unew))) + uentry_whereLast (unew))) /* evans 2001-12-30: was uentry_whereDeclared */ { - uentry_showWhereLast (old); + uentry_showWhereLastKind (old); } } else @@ -6801,9 +6843,9 @@ KindConformanceError (/*@unique@*/ uentry old, uentry unew, bool mustConform) uentry_getName (unew), ekind_unparseLong (unew->ukind), unew->utype), - uentry_whereDeclared (unew))) + uentry_whereLast (unew))) /* evans 2001-12-30: was uentry_whereDeclared */ { - uentry_showWhereLast (old); + uentry_showWhereLastKind (old); } } } @@ -6811,15 +6853,18 @@ KindConformanceError (/*@unique@*/ uentry old, uentry unew, bool mustConform) { llassert (uentry_isDeclared (unew)); + DPRINTF (("Old: \n\t%s", uentry_unparseFull (old))); + DPRINTF (("New: \n\t%s", uentry_unparseFull (unew))); + if (optgenerror (FLG_INCONDEFS, message ("%s %q inconsistently redeclared as %s", ekind_capName (old->ukind), uentry_getName (unew), ekind_unparseLong (unew->ukind)), - uentry_whereDeclared (unew))) + uentry_whereLast (unew))) /* evans 2001-12-30: was uentry_whereDeclared */ { - uentry_showWhereLast (old); + uentry_showWhereLastKind (old); } } } @@ -6843,7 +6888,7 @@ uentry_showWhereLast (uentry spec) { if (fileloc_isDefined (spec->whereDefined) && !fileloc_isLib (spec->whereDefined) - && !fileloc_isPreproc (spec->whereDefined)) + /*!! && !fileloc_isPreproc (spec->whereDefined) */ ) { llgenindentmsg (message ("Previous definition of %q: %t", uentry_getName (spec), @@ -6879,6 +6924,54 @@ uentry_showWhereLast (uentry spec) } } +static void +uentry_showWhereLastKind (uentry spec) +{ + if (uentry_isValid (spec)) + { + if (fileloc_isDefined (spec->whereDefined) + && !fileloc_isLib (spec->whereDefined) + /*!! && !fileloc_isPreproc (spec->whereDefined) */ ) + { + llgenindentmsg (message ("Previous definition of %q as %s: %t", + uentry_getName (spec), + ekind_unparseLong (spec->ukind), + uentry_getType (spec)), + uentry_whereDefined (spec)); + } + else if (uentry_isDeclared (spec)) + { + llgenindentmsg (message ("Previous declaration of %q as %s: %t", + uentry_getName (spec), + ekind_unparseLong (spec->ukind), + uentry_getType (spec)), + uentry_whereDeclared (spec)); + } + else if (uentry_isSpecified (spec)) + { + if (uentry_hasName (spec)) + { + llgenindentmsg (message ("Specification of %q as %s: %t", + uentry_getName (spec), + ekind_unparseLong (spec->ukind), + uentry_getType (spec)), + uentry_whereSpecified (spec)); + } + else + { + llgenindentmsg (message ("Specification as %s: %t", + ekind_unparseLong (spec->ukind), + uentry_getType (spec)), + uentry_whereSpecified (spec)); + } + } + else + { + /* nothing to show */ + } + } +} + void uentry_showDefSpecInfo (uentry ce, fileloc fwhere) { @@ -8323,7 +8416,7 @@ checkFunctionConformance (/*@unique@*/ /*@notnull@*/ uentry old, cstring nnamefix; if (cstring_isDefined (pfx) - && cstring_equalPrefix (oldname, cstring_toCharsSafe (pfx))) + && cstring_equalPrefix (oldname, pfx)) { oname = cstring_suffix (oldname, cstring_length (pfx)); } @@ -8333,7 +8426,7 @@ checkFunctionConformance (/*@unique@*/ /*@notnull@*/ uentry old, /*@-branchstate@*/ } /*@=branchstate@*/ if (cstring_isDefined (pfx) - && cstring_equalPrefix (nname, cstring_toCharsSafe (pfx))) + && cstring_equalPrefix (nname, pfx)) { nnamefix = cstring_suffix (nname, cstring_length (pfx)); } @@ -8483,8 +8576,8 @@ checkFunctionConformance (/*@unique@*/ /*@notnull@*/ uentry old, unew->info->fcn->specclauses = stateClauseList_undefined; /*@-branchstate@*/ } - /*@=branchstate@*/ /*@i23 shouldn't need this@*/ } + /*@=branchstate@*/ /*@i23 shouldn't need this@*/ if (fileloc_isUndefined (old->whereDeclared)) { @@ -8498,7 +8591,7 @@ checkFunctionConformance (/*@unique@*/ /*@notnull@*/ uentry old, { /* no change */ } -} +/*@i523 @*/ } void uentry_mergeConstantValue (uentry ue, /*@only@*/ multiVal m) @@ -9884,7 +9977,7 @@ static void } } -static bool incompatibleStates (sRef rs, sRef os) +static bool uentry_incompatibleMemoryStates (sRef rs, sRef os) { alkind rk = sRef_getAliasKind (rs); alkind ok = sRef_getAliasKind (os); @@ -9963,29 +10056,32 @@ uentry_mergeAliasStates (uentry res, uentry other, fileloc loc, bool mustReturn, bool flip, bool opt, clause cl) { + sRef rs = res->sref; + sRef os = other->sref; + DPRINTF (("Merge alias states: %s / %s", uentry_unparseFull (res), uentry_unparseFull (other))); - if (sRef_isValid (res->sref)) + if (sRef_isValid (rs)) { if (!mustReturn) { - DPRINTF (("1")); - if (incompatibleStates (res->sref, other->sref)) + if (uentry_incompatibleMemoryStates (rs, os)) { - DPRINTF (("2")); + DPRINTF (("Incompatible: \n\t%s / \n\t%s", + sRef_unparseFull (rs), sRef_unparseFull (os))); - if (sRef_isThroughArrayFetch (res->sref) + if (sRef_isThroughArrayFetch (rs) && !context_getFlag (FLG_STRICTBRANCHSTATE)) { - if (sRef_isKept (res->sref) || sRef_isKept (other->sref)) + if (sRef_isKept (rs) || sRef_isKept (os)) { - sRef_maybeKill (res->sref, loc); + sRef_maybeKill (rs, loc); } - else if (sRef_isPossiblyDead (other->sref)) + else if (sRef_isPossiblyDead (os)) { - sRef_maybeKill (res->sref, loc); + sRef_maybeKill (rs, loc); } else { @@ -9994,20 +10090,19 @@ uentry_mergeAliasStates (uentry res, uentry other, fileloc loc, } else { - if (uentry_relevantReference (other->sref, flip)) + if (uentry_relevantReference (os, flip)) { - DPRINTF (("4")); - if (sRef_isLocalParamVar (res->sref) - && (sRef_isLocalState (other->sref) - || sRef_isDependent (other->sref))) + if (sRef_isLocalParamVar (rs) + && (sRef_isLocalState (os) + || sRef_isDependent (os))) { - if (sRef_isDependent (res->sref)) + if (sRef_isDependent (rs)) { - sRef_setDependent (other->sref, loc); + sRef_setDependent (os, loc); } else { - sRef_setDefState (res->sref, SS_UNUSEABLE, loc); + sRef_setDefState (rs, SS_UNUSEABLE, loc); } } else @@ -10017,33 +10112,34 @@ uentry_mergeAliasStates (uentry res, uentry other, fileloc loc, } } - if (sRef_isKept (res->sref)) + if (sRef_isKept (rs)) { - sRef_setKept (other->sref, loc); + DPRINTF (("Setting kept: %s", sRef_unparseFull (os))); + sRef_setKept (os, loc); } } else { - if (incompatibleStates (other->sref, res->sref)) + if (uentry_incompatibleMemoryStates (os, rs)) { - if (uentry_relevantReference (res->sref, !flip)) + if (uentry_relevantReference (rs, !flip)) { - if (sRef_isLocalParamVar (res->sref) - && (sRef_isDependent (res->sref) - || sRef_isLocalState (res->sref))) + if (sRef_isLocalParamVar (rs) + && (sRef_isDependent (rs) + || sRef_isLocalState (rs))) { - if (sRef_isDependent (other->sref)) + if (sRef_isDependent (os)) { - sRef_setDependent (res->sref, loc); + sRef_setDependent (rs, loc); } else { - sRef_setDefState (res->sref, SS_UNUSEABLE, loc); + sRef_setDefState (rs, SS_UNUSEABLE, loc); } } else { - if (sRef_isParam (other->sref)) + if (sRef_isParam (os)) { /* ** If the local variable associated @@ -10055,9 +10151,9 @@ uentry_mergeAliasStates (uentry res, uentry other, fileloc loc, uentry uvar = usymtab_lookupSafe (other->uname); if (uentry_isValid (uvar) - && ((sRef_isDead (other->sref) + && ((sRef_isDead (os) && sRef_isOnly (uvar->sref)) - || (sRef_isDependent (other->sref) + || (sRef_isDependent (os) && sRef_isOwned (uvar->sref)))) { /* no error */ @@ -10081,41 +10177,51 @@ uentry_mergeAliasStates (uentry res, uentry other, fileloc loc, } } - if (sRef_isKept (other->sref)) + if (sRef_isKept (os)) { - sRef_setKept (res->sref, loc); + sRef_setKept (rs, loc); } } if (opt) { DPRINTF (("Merge opt...")); - sRef_mergeOptState (res->sref, other->sref, cl, loc); + sRef_mergeOptState (rs, os, cl, loc); DPRINTF (("Done!")); } else { - sRef_mergeState (res->sref, other->sref, cl, loc); + DPRINTF (("Merging states: \n\t%s / \n\t%s", sRef_unparseFull (rs), sRef_unparseFull (os))); + sRef_mergeState (rs, os, cl, loc); + DPRINTF (("After merging : \n\t%s / \n\t%s", sRef_unparseFull (rs), sRef_unparseFull (os))); } } else { - if (sRef_isModified (other->sref)) + if (sRef_isModified (os)) { - sRef_setModified (res->sref); + sRef_setModified (rs); } } } + + DPRINTF (("After merge: %s", sRef_unparseFull (res->sref))); } static void -uentry_mergeValueStates (uentry res, uentry other, fileloc loc) +uentry_mergeValueStates (uentry res, uentry other, fileloc loc, bool mustReturn, /*@unused@*/ bool flip) { valueTable rvalues; valueTable ovalues; DPRINTF (("Merge values: %s / %s", sRef_unparseFull (res->sref), sRef_unparseFull (other->sref))); + if (mustReturn) + { + return; + } + /* flip? */ + rvalues = sRef_getValueTable (res->sref); ovalues = sRef_getValueTable (other->sref); @@ -10166,7 +10272,7 @@ uentry_mergeValueStates (uentry res, uentry other, fileloc loc) { sRef_setMetaStateValueComplete (res->sref, fkey, stateValue_getValue (fval), - loc); + stateValue_getLoc (fval)); DPRINTF (("Setting res: %s", sRef_unparseFull (res->sref))); } else if (stateValue_isError (tval) @@ -10174,6 +10280,11 @@ uentry_mergeValueStates (uentry res, uentry other, fileloc loc) { DPRINTF (("Other branch is definitely null!")); } + else if (sRef_isStateUndefined (res->sref) + || sRef_isDead (res->sref)) + { + ; /* Combination state doesn't matter if it is undefined or dead */ + } else { DPRINTF (("Check: %s / %s / %s / %s", fkey, @@ -10199,7 +10310,7 @@ uentry_mergeValueStates (uentry res, uentry other, fileloc loc) DPRINTF (("nval: %d / %d / %d", nval, stateValue_getValue (fval), stateValue_getValue (tval))); - if (cstring_isDefined (msg)) + if (nval == stateValue_error) { /*@i32 print extra info for assignments@*/ @@ -10208,10 +10319,11 @@ uentry_mergeValueStates (uentry res, uentry other, fileloc loc) if (optgenerror (FLG_STATEMERGE, message - ("Control branches merge with incompatible global states (%s and %s): %s", + ("Control branches merge with incompatible global states (%s and %s)%q", metaStateInfo_unparseValue (minfo, stateValue_getValue (fval)), metaStateInfo_unparseValue (minfo, stateValue_getValue (tval)), - msg), + cstring_isDefined (msg) + ? message (": %s", msg) : cstring_undefined), loc)) { sRef_showMetaStateInfo (res->sref, fkey); @@ -10223,11 +10335,12 @@ uentry_mergeValueStates (uentry res, uentry other, fileloc loc) if (optgenerror (FLG_STATEMERGE, message - ("Control branches merge with incompatible states for %q (%s and %s): %s", + ("Control branches merge with incompatible states for %q (%s and %s)%q", uentry_getName (res), metaStateInfo_unparseValue (minfo, stateValue_getValue (fval)), metaStateInfo_unparseValue (minfo, stateValue_getValue (tval)), - msg), + cstring_isDefined (msg) + ? message (": %s", msg) : cstring_undefined), loc)) { sRef_showMetaStateInfo (res->sref, fkey); @@ -10353,7 +10466,7 @@ uentry_mergeState (uentry res, uentry other, fileloc loc, uentry_unparseFull (other))); uentry_mergeAliasStates (res, other, loc, mustReturn, flip, opt, cl); - uentry_mergeValueStates (res, other, loc); + uentry_mergeValueStates (res, other, loc, mustReturn, flip); uentry_mergeSetStates (res, other, loc, flip, cl); } @@ -10973,64 +11086,8 @@ bool uentry_isGlobalMarker (uentry ue) && (cstring_equal (uentry_rawName (ue), GLOBAL_MARKER_NAME))); } - -// /* new start modifications */ -/*@ignore@*/ - - -# if 0 - -static void uentry_testInRange (uentry p_e, uentry cconstant) { - if (uentry_isValid(p_e)) { - if (sRef_isValid (p_e->sref)) { - /* char * t = cstring_toCharsSafe (uentry_unparse(cconstant) ); - int index = atoi( t ); - free (t); - */ - long index = multiVal_forceInt (uentry_getConstantValue (cconstant)); - // usymtab_testInRange (p_e->sref, index); - }//end if - }//endif -} - - -/* void uentry_setStringLength (uentry p_e, uentry cconstant) { */ -/* if( uentry_isValid(p_e) ) { */ -/* if( p_e->info != NULL) { */ -/* if( p_e->info->var != NULL) { */ -/* char *t = cstring_toCharsSafe (uentry_unparse(cconstant)); */ -/* int length = atoi( t ); */ -/* free (t); */ -/* p_e->info->var->bufinfo->len = length; */ -/* p_e->sref->bufinfo.len = length; */ -/* printf("Set string length of buff to %d \n", p_e->sref->bufinfo.size); */ -/* }//end if */ -/* }//endif */ -/* }//end if */ -/* } */ - - -static void uentry_setBufferSize (uentry p_e, exprNode cconstant) { -if( uentry_isValid(p_e) ) { - if( p_e->info != NULL) { - if( p_e->info->var != NULL) { - int size = atoi(cstring_toCharsSafe(exprNode_unparse(cconstant) ) ); - p_e->info->var->bufinfo->size = size; - p_e->sref->bufinfo.size = size; - printf("Set buffer size to %d \n", p_e->sref->bufinfo.size); - // fprintf(stderr, "For %s and %s\n", uentry_unparse(p_e) ); - // fprintf(stderr, "and %d\n", size ); - - }//end if - }//endif -}//end if -} - -# endif - - /* start modifications */ /* requires: p_e is defined, is a ptr/array variable @@ -11040,15 +11097,17 @@ effects: sets the state of the variable void uentry_setPossiblyNullTerminatedState (uentry p_e) { + /*@access sRef@*/ /*i523 shouldn't do this! */ if( uentry_isValid(p_e) ) { if( p_e->info != NULL) { if( p_e->info->var != NULL) { p_e->info->var->bufinfo->bufstate = BB_POSSIBLYNULLTERMINATED; p_e->sref->bufinfo.bufstate = BB_POSSIBLYNULLTERMINATED; return; - }/* End if */ - }/* End if */ - }/* End if */ + } + } + } + /*@noaccess sRef@*/ fprintf(stderr, "uentry:Error in setPossiblyNullTerminatedState\n"); } @@ -11064,37 +11123,17 @@ void uentry_setNullTerminatedState (uentry p_e) { if( p_e->info != NULL) { if( p_e->info->var != NULL) { p_e->info->var->bufinfo->bufstate = BB_NULLTERMINATED; + /*@access sRef@*/ /*@i523 bad!*/ p_e->sref->bufinfo.bufstate = BB_NULLTERMINATED; + /*@noaccess sRef@*/ return; - }//End if - }//End if - }//End if + } + } + } fprintf(stderr, "uentry:Error in setNullTerminatedState\n"); } - -/* -requires: p_e is defined, is a ptr/array variable -modifies: p_e -effects: sets the state of the variable -*/ - -/* void uentry_setNotNullTerminatedState (uentry p_e) { */ -/* if( uentry_isValid(p_e) ) { */ -/* if( p_e->info != NULL) { */ -/* if( p_e->info->var != NULL) { */ -/* p_e->info->var->bufinfo->bufstate = BB_NOTNULLTERMINATED; */ -/* p_e->sref->bufinfo.bufstate = BB_NOTNULLTERMINATED; */ -/* return; */ -/* }//End if */ -/* }//End if */ -/* }//End if */ - -/* fprintf(stderr, "uentry:Error in setNotNullTerminatedState\n"); */ -/* } */ - - /* requires: p_e is defined, is a ptr/array variable modifies: p_e @@ -11106,11 +11145,13 @@ void uentry_setSize (uentry p_e, int size) { if( p_e->info != NULL) { if( p_e->info->var != NULL) { p_e->info->var->bufinfo->size = size; + /*@access sRef@*/ /*@i523 bad!*/ p_e->sref->bufinfo.size = size; + /*@noaccess sRef@*/ return; - }//End if - }//End if - }//End if + } + } + } fprintf(stderr, "uentry:Error in setSize\n"); } @@ -11122,20 +11163,22 @@ modifies: p_e effects: sets the length of the buffer */ - void uentry_setLen (uentry p_e, int len) { +void uentry_setLen (uentry p_e, int len) { if( uentry_isValid(p_e) ) { if( p_e->info != NULL) { if( p_e->info->var != NULL) { p_e->info->var->bufinfo->len = len; + /*@access sRef@*/ /*@i523 bad!*/ p_e->sref->bufinfo.len = len; + /*@noaccess sRef@*/ return; - }//End if - }//End if - }//End if - + } + } + } + fprintf(stderr, "uentry:Error in setLen\n"); } -/*@end@*/ + /*@=type*/ bool uentry_hasMetaStateEnsures (uentry e)