X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/abd7f89523564e5e238e5852585b98f72c3b48f4..f6099dac655d3fc5409f54302dd3b5c1b6be6ac6:/src/Headers/uentry.h diff --git a/src/Headers/uentry.h b/src/Headers/uentry.h index 4b89966..314f009 100644 --- a/src/Headers/uentry.h +++ b/src/Headers/uentry.h @@ -1,5 +1,5 @@ /* -** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2001. +** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2003. ** See ../LICENSE for license information. */ # ifndef UENTRY_H @@ -72,7 +72,7 @@ typedef struct typedef struct { - ynm abs; + qual abs; /* oneof QU_UNKNOWN, QU_ABSTRACT, QU_NUMABSTRACT, QU_CONCRETE */ ynm mut; ctype type; } *udinfo ; @@ -118,7 +118,7 @@ typedef struct typedef struct { - typeIdSet access; + typeIdSet access; } *ueinfo ; typedef union @@ -254,7 +254,7 @@ extern void uentry_setMessageLike (uentry p_ue) /*@modifies p_ue@*/ ; extern void uentry_setScanfLike (uentry p_ue) /*@modifies p_ue@*/ ; extern void uentry_setPrintfLike (uentry p_ue) /*@modifies p_ue@*/ ; -extern void uentry_checkName (uentry p_ue) /*@modifies g_msgstream, p_ue@*/ ; +extern void uentry_checkName (uentry p_ue) /*@modifies g_warningstream, p_ue@*/ ; extern bool uentry_sameObject (uentry p_e1, uentry p_e2); # define uentry_sameObject(e1,e2) ((e1) == (e2)) @@ -262,7 +262,7 @@ extern bool uentry_sameObject (uentry p_e1, uentry p_e2); extern void uentry_addAccessType (uentry p_ue, typeId p_tid) /*@modifies p_ue@*/ ; extern void uentry_showWhereAny (uentry p_spec) - /*@modifies g_msgstream@*/ ; + /*@modifies g_warningstream@*/ ; extern void uentry_checkParams (uentry p_ue); extern void uentry_mergeUses (uentry p_res, uentry p_other); @@ -358,17 +358,17 @@ extern /*@notnull@*/ uentry uentry_makeExpandedMacro (cstring p_s, /*@temp@*/ fileloc p_f) /*@*/ ; -extern void uentry_checkMatchParam (uentry p_u1, uentry p_u2, int p_paramno, exprNode p_e) /*@modifies g_msgstream@*/ ; +extern void uentry_checkMatchParam (uentry p_u1, uentry p_u2, int p_paramno, exprNode p_e) /*@modifies g_warningstream@*/ ; extern /*@observer@*/ stateClauseList uentry_getStateClauseList (uentry p_ue) /*@*/ ; extern void uentry_showWhereLastExtra (uentry p_spec, /*@only@*/ cstring p_extra) - /*@modifies g_msgstream@*/ ; + /*@modifies g_warningstream@*/ ; -# ifndef NOLCL extern void uentry_setRefCounted (uentry p_e); extern /*@notnull@*/ /*@only@*/ uentry uentry_makeUnnamedVariable (ctype p_t); +extern /*@falsewhennull@*/ bool uentry_isUnnamedVariable (uentry) /*@*/; extern /*@notnull@*/ uentry uentry_makeUnspecFunction (cstring p_n, ctype p_t, typeIdSet p_access, @@ -394,7 +394,6 @@ extern /*@notnull@*/ uentry uentry_makeSpecFunction (cstring p_n, ctype p_t, typeIdSet p_access, /*@only@*/ globSet p_globs, /*@only@*/ sRefSet p_mods, /*@keep@*/ fileloc p_f); -# endif extern /*@notnull@*/ uentry uentry_makeEnumConstant (cstring p_n, ctype p_t) /*@*/ ; @@ -416,11 +415,11 @@ extern /*@notnull@*/ /*@only@*/ uentry /*@*/ ; extern /*@notnull@*/ /*@only@*/ uentry - uentry_makeDatatype (/*@temp@*/ cstring p_n, ctype p_t, ynm p_mut, ynm p_abstract, + uentry_makeDatatype (/*@temp@*/ cstring p_n, ctype p_t, ynm p_mut, qual p_abstract, /*@only@*/ fileloc p_f) /*@*/ ; extern /*@notnull@*/ /*@only@*/ uentry uentry_makeDatatypeAux (/*@temp@*/ cstring p_n, ctype p_t, ynm p_mut, - ynm p_abstract, /*@keep@*/ fileloc p_f, bool p_priv) /*@*/ ; + qual p_abstract, /*@keep@*/ fileloc p_f, bool p_priv) /*@*/ ; extern /*@notnull@*/ uentry uentry_makeElipsisMarker (void) /*@*/ ; extern void uentry_makeVarFunction (/*@temp@*/ uentry p_ue) /*@modifies p_ue@*/ ; @@ -462,10 +461,8 @@ extern /*@notnull@*/ uentry extern /*@notnull@*/ /*@only@*/ uentry uentry_makeVariableLoc (cstring p_n, ctype p_t); -# ifndef NOLCL extern /*@notnull@*/ /*@only@*/ uentry uentry_makeVariableParam (cstring p_n, ctype p_t, fileloc p_loc); -# endif extern /*@notnull@*/ /*@only@*/ uentry uentry_makeVariableSrefParam (cstring p_n, ctype p_t, /*@only@*/ fileloc p_loc, @@ -475,7 +472,7 @@ extern /*@notnull@*/ /*@only@*/ extern /*@notnull@*/ /*@only@*/ uentry uentry_makeIdDatatype (idDecl p_id); extern /*@notnull@*/ /*@only@*/ - uentry uentry_makeBoolDatatype (ynm p_abstract); + uentry uentry_makeBoolDatatype (qual p_abstract); extern void uentry_mergeDefinition (uentry p_old, /*@only@*/ uentry p_unew); extern void uentry_mergeEntries (uentry p_spec, /*@only@*/ uentry p_def); extern uentry uentry_nameCopy (/*@only@*/ cstring p_name, uentry p_e); @@ -517,18 +514,19 @@ extern void uentry_setStateClauseList (uentry p_ue, /*@only@*/ stateClauseList p extern void uentry_setType (uentry p_e, ctype p_t); extern /*@unused@*/ /*@observer@*/ cstring uentry_checkedName (uentry p_ue); -extern void uentry_showWhereLastPlain (uentry p_spec) /*@modifies g_msgstream@*/ ; +extern void uentry_showWhereLastPlain (uentry p_spec) /*@modifies g_warningstream@*/ ; extern void uentry_showWhereSpecifiedExtra (uentry p_spec, /*@only@*/ cstring p_s) - /*@modifies g_msgstream@*/ ; + /*@modifies g_warningstream@*/ ; -extern void uentry_showWhereSpecified (uentry p_spec) /*@modifies g_msgstream@*/ ; -extern void uentry_showWhereLast (uentry p_spec) /*@modifies g_msgstream@*/ ; -extern void uentry_showWhereDeclared (uentry p_spec) /*@modifies g_msgstream@*/ ; +extern void uentry_showWhereSpecified (uentry p_spec) /*@modifies g_warningstream@*/ ; +extern void uentry_showWhereLast (uentry p_spec) /*@modifies g_warningstream@*/ ; +extern void uentry_showWhereDeclared (uentry p_spec) /*@modifies g_warningstream@*/ ; extern /*@notnull@*/ /*@only@*/ uentry uentry_makeIdVariable (idDecl p_t) /*@*/ ; extern uentry uentry_copy (uentry p_e) /*@*/ ; +extern uentry uentry_copyNoSave (uentry p_e) /*@*/ ; /* for use for uentries that do not live beyond function exits */ extern void uentry_freeComplete (/*@only@*/ uentry p_e) ; extern void uentry_clearDefined (uentry p_e) /*@modifies p_e@*/; extern /*@observer@*/ cstring uentry_specDeclName (uentry p_u) /*@*/ ; @@ -569,7 +567,7 @@ extern alkind uentry_getAliasKind (uentry p_u) /*@*/ ; extern exkind uentry_getExpKind (uentry p_u) /*@*/ ; extern /*@observer@*/ multiVal uentry_getConstantValue (uentry p_e) /*@*/ ; extern void uentry_fixupSref (uentry p_ue) /*@modifies p_ue@*/ ; -extern void uentry_setGlobals (uentry p_ue, /*@owned@*/ globSet p_globs) /*@modifies p_ue, p_globs@*/ ; +extern void uentry_setGlobals (uentry p_ue, /*@only@*/ globSet p_globs) /*@modifies p_ue, p_globs@*/ ; extern bool uentry_isYield (uentry p_ue) /*@*/ ; extern /*@notnull@*/ uentry uentry_makeIdConstant (idDecl p_t) /*@*/ ; extern /*@observer@*/ cstring uentry_getRealName (uentry p_e) /*@*/ ; @@ -578,7 +576,7 @@ extern int uentry_xcompareuses (uentry *p_p1, uentry *p_p2) /*@*/ ; extern /*@observer@*/ cstring uentry_specOrDefName (uentry p_u) /*@*/ ; extern void uentry_copyState (uentry p_res, uentry p_other); extern bool uentry_sameKind (uentry p_u1, uentry p_u2); -extern /*@exposed@*/ sRef uentry_returnedRef (uentry p_u, exprNodeList p_args); +extern /*@exposed@*/ sRef uentry_returnedRef (uentry p_u, exprNodeList p_args, fileloc p_loc); extern bool uentry_isReturned (uentry p_u); extern bool uentry_isRefCountedDatatype (uentry p_e); extern sstate uentry_getDefState (uentry p_u); @@ -671,6 +669,14 @@ extern void uentry_setPostconditions (uentry p_ue, /*@only@*/ functionConstraint extern void uentry_setPreconditions (uentry p_ue, /*@only@*/ functionConstraint p_preconditions); /*end mods*/ +/* +** For debugging only +*/ + +# ifdef DEBUGSPLINT +extern void uentry_checkValid (uentry p_ue) /*@modifies g_errorstream@*/ ; +# endif + # else # error "Multiple include" # endif