X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/920a3797c23377bfb7332b0c11bda1d708cabb72..e015e0876e6dea76409cc6f82753dd4f185ae950:/src/Headers/uentry.h diff --git a/src/Headers/uentry.h b/src/Headers/uentry.h index caaa6c3..ec9e60b 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-2000. +** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2001. ** See ../LICENSE for license information. */ # ifndef UENTRY_H @@ -15,10 +15,10 @@ ** vkind --- need to fix value for consistency in dump files */ -typedef struct _ucinfo +typedef struct { - /*@only@*/ multiVal val; - typeIdSet access; + typeIdSet access; + bool macro; } *ucinfo; typedef enum @@ -47,19 +47,19 @@ typedef enum } chkind; /* start modifications */ -typedef enum _bbufstate { +typedef enum { BB_POSSIBLYNULLTERMINATED, /* buffer is possibly nullterm(can't decide statically) */ BB_NULLTERMINATED, /*buffer is known to be nullterminated */ BB_NOTNULLTERMINATED /* buffer is known to be not nullterm */ } bbufstate; -typedef struct _bbufinfo { +typedef /*@null@*/ struct s_bbufinfo { bbufstate bufstate; /* state of the buffer */ int size; /* size of the buffer allocated */ int len; /* len of the buffer VALID ONLY IF state is NULLTERM */ } *bbufinfo ; -typedef struct _uvinfo +typedef struct { vkind kind; /* kind (parameter, specified) */ chkind checked; /* how is it checked */ @@ -70,7 +70,7 @@ typedef struct _uvinfo } *uvinfo ; /* end modifications */ -typedef struct _udinfo +typedef struct { ynm abs; ynm mut; @@ -88,7 +88,7 @@ typedef enum SPC_LAST } specCode; -typedef struct _ufinfo +typedef struct { qual nullPred; specCode specialCode; @@ -98,30 +98,30 @@ typedef struct _ufinfo /*@owned@*/ globSet globs; /* globals list */ /*@owned@*/ sRefSet mods; /* modifies */ - specialClauses specclauses; + stateClauseList specclauses; /*@dependent@*/ uentryList defparams; bool hasGlobs BOOLBITS; bool hasMods BOOLBITS; - constraintList preconditions; - constraintList postconditions; + functionConstraint preconditions; + functionConstraint postconditions; } *ufinfo ; -typedef struct _uiinfo +typedef struct { typeIdSet access; /*@owned@*/ globSet globs; /* globals list */ /*@owned@*/ sRefSet mods; /* modifies */ } *uiinfo ; -typedef struct _ueinfo +typedef struct { - typeIdSet access; + typeIdSet access; } *ueinfo ; -typedef union _uinfo +typedef union { ucinfo uconst; uvinfo var; @@ -131,7 +131,7 @@ typedef union _uinfo ueinfo enditer; } *uinfo ; -struct _uentry +struct s_uentry { ekind ukind; cstring uname; @@ -146,8 +146,11 @@ struct _uentry ** functions state of return value ** types state of datatype */ + /*@exposed@*/ /*@null@*/ sRef sref; + warnClause warn; + /* Location list is complete only if showalluses is set. */ filelocList uses; @@ -163,14 +166,14 @@ struct _uentry /* ** There is no uentry_isDefined to avoid confusion with ** uentry_isCodeDefined (which was previously called -** uentry_isDefined. +** uentry_isDefined). */ -extern /*@truenull@*/ bool uentry_isUndefined (/*@special@*/ uentry p_e) +extern /*@nullwhentrue@*/ bool uentry_isUndefined (/*@special@*/ uentry p_e) /*@*/ ; -extern /*@truenull@*/ bool uentry_isInvalid (/*@special@*/ uentry p_e) +extern /*@nullwhentrue@*/ bool uentry_isInvalid (/*@special@*/ uentry p_e) /*@*/ ; -extern /*@falsenull@*/ bool uentry_isValid (/*@special@*/ uentry p_e) +extern /*@falsewhennull@*/ bool uentry_isValid (/*@special@*/ uentry p_e) /*@*/ ; /*@constant null uentry uentry_undefined; @*/ @@ -190,51 +193,51 @@ extern void uentry_setAbstract (uentry p_e) /*@modifies p_e@*/ ; extern void uentry_setConcrete (uentry p_e) /*@modifies p_e@*/ ; extern void uentry_setHasNameError (uentry p_ue) /*@modifies p_ue@*/ ; -extern /*@falsenull@*/ bool uentry_isLset (/*@sef@*/ uentry p_e); +extern /*@falsewhennull@*/ bool uentry_isLset (/*@sef@*/ uentry p_e); # define uentry_isLset(e) \ (uentry_isValid(e) && (e)->lset) -extern /*@falsenull@*/ bool uentry_isUsed (/*@sef@*/ uentry p_e); +extern /*@falsewhennull@*/ bool uentry_isUsed (/*@sef@*/ uentry p_e); # define uentry_isUsed(e) (uentry_isValid(e) && (e)->used) -extern /*@unused@*/ /*@falsenull@*/ bool +extern /*@unused@*/ /*@falsewhennull@*/ bool uentry_isAbstractType (uentry p_e) /*@*/ ; # define uentry_isAbstractType(e) (uentry_isAbstractDatatype(e)) -extern /*@falsenull@*/ bool uentry_isConstant (/*@sef@*/ uentry p_e) /*@*/ ; +extern /*@falsewhennull@*/ bool uentry_isConstant (/*@sef@*/ uentry p_e) /*@*/ ; # define uentry_isConstant(e) \ (uentry_isValid(e) && ekind_isConst ((e)->ukind)) -extern /*@falsenull@*/ bool uentry_isEitherConstant (/*@sef@*/ uentry p_e) /*@*/ ; +extern /*@falsewhennull@*/ bool uentry_isEitherConstant (/*@sef@*/ uentry p_e) /*@*/ ; # define uentry_isEitherConstant(e) \ (uentry_isValid(e) && (ekind_isConst ((e)->ukind) || ekind_isEnumConst ((e)->ukind))) -extern /*@falsenull@*/ bool uentry_isEnumConstant (/*@sef@*/ uentry p_e) /*@*/ ; +extern /*@falsewhennull@*/ bool uentry_isEnumConstant (/*@sef@*/ uentry p_e) /*@*/ ; # define uentry_isEnumConstant(e) \ (uentry_isValid(e) && ekind_isEnumConst ((e)->ukind)) -extern /*@falsenull@*/ bool uentry_isExternal (/*@sef@*/ uentry p_e) /*@*/ ; +extern /*@falsewhennull@*/ bool uentry_isExternal (/*@sef@*/ uentry p_e) /*@*/ ; # define uentry_isExternal(c) \ (uentry_isValid(c) && fileloc_isExternal (uentry_whereDefined (c))) -extern /*@falsenull@*/ bool uentry_isExtern (/*@sef@*/ uentry p_e) /*@*/ ; +extern /*@falsewhennull@*/ bool uentry_isExtern (/*@sef@*/ uentry p_e) /*@*/ ; # define uentry_isExtern(c) \ (uentry_isValid(c) && (c)->storageclass == SCEXTERN) extern bool uentry_isForward (uentry p_e) /*@*/ ; -extern /*@falsenull@*/ bool uentry_isFunction (/*@sef@*/ uentry p_e) /*@*/ ; +extern /*@falsewhennull@*/ bool uentry_isFunction (/*@sef@*/ uentry p_e) /*@*/ ; # define uentry_isFunction(e) \ (uentry_isValid(e) && ekind_isFunction ((e)->ukind)) -extern /*@falsenull@*/ bool uentry_isPriv (/*@sef@*/ uentry p_e) /*@*/ ; +extern /*@falsewhennull@*/ bool uentry_isPriv (/*@sef@*/ uentry p_e) /*@*/ ; # define uentry_isPriv(e) \ (uentry_isValid(e) && (e)->isPrivate) -extern /*@falsenull@*/ bool uentry_isFileStatic (uentry p_ue) /*@*/ ; -extern /*@falsenull@*/ bool uentry_isExported (uentry p_ue) /*@*/ ; +extern /*@falsewhennull@*/ bool uentry_isFileStatic (uentry p_ue) /*@*/ ; +extern /*@falsewhennull@*/ bool uentry_isExported (uentry p_ue) /*@*/ ; -extern /*@falsenull@*/ bool uentry_isStatic (/*@sef@*/ uentry p_e) /*@*/ ; +extern /*@falsewhennull@*/ bool uentry_isStatic (/*@sef@*/ uentry p_e) /*@*/ ; # define uentry_isStatic(c) \ (uentry_isValid(c) && (c)->storageclass == SCSTATIC) @@ -251,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)) @@ -259,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); @@ -281,52 +284,57 @@ extern /*@observer@*/ fileloc uentry_whereEarliest (uentry p_e) /*@*/ ; extern /*@observer@*/ cstring uentry_rawName (uentry p_e) /*@*/ ; extern /*@observer@*/ fileloc uentry_whereDeclared (uentry p_e) /*@*/ ; extern bool uentry_equiv (uentry p_p1, uentry p_p2) /*@*/ ; -extern /*@falsenull@*/ bool uentry_hasName (uentry p_e) /*@*/ ; -extern /*@falsenull@*/ bool uentry_hasRealName (uentry p_e) /*@*/ ; -extern /*@falsenull@*/ bool uentry_isAbstractDatatype (uentry p_e) /*@*/ ; -extern /*@falsenull@*/ bool uentry_isAnyTag (/*@special@*/ uentry p_ue) +extern /*@falsewhennull@*/ bool uentry_hasName (uentry p_e) /*@*/ ; +extern /*@falsewhennull@*/ bool uentry_hasRealName (uentry p_e) /*@*/ ; +extern /*@falsewhennull@*/ bool uentry_isAbstractDatatype (uentry p_e) /*@*/ ; +extern /*@falsewhennull@*/ bool uentry_isAnyTag (/*@special@*/ uentry p_ue) /*@uses p_ue->ukind@*/ /*@*/ ; -extern /*@falsenull@*/ bool uentry_isDatatype (uentry p_e) /*@*/ ; +extern /*@falsewhennull@*/ bool uentry_isDatatype (uentry p_e) /*@*/ ; -extern /*@falsenull@*/ bool uentry_isCodeDefined (uentry p_e) /*@*/ ; +extern /*@falsewhennull@*/ bool uentry_isCodeDefined (uentry p_e) /*@*/ ; -extern /*@falsenull@*/ bool uentry_isDeclared (/*@special@*/ uentry p_e) +extern /*@falsewhennull@*/ bool uentry_isDeclared (/*@special@*/ uentry p_e) /*@uses p_e->whereDeclared@*/ /*@*/ ; extern /*@observer@*/ cstring uentry_ekindName (uentry p_ue) /*@*/ ; +extern /*@observer@*/ cstring uentry_ekindNameLC (uentry p_ue) /*@*/ ; + extern void uentry_showWhereDefined (uentry p_spec); -extern /*@falsenull@*/ bool uentry_isEndIter (uentry p_e) /*@*/ ; -extern /*@falsenull@*/ bool uentry_isEnumTag (/*@special@*/ uentry p_ue) +extern /*@falsewhennull@*/ bool uentry_isEndIter (uentry p_e) /*@*/ ; +extern /*@falsewhennull@*/ bool uentry_isEnumTag (/*@special@*/ uentry p_ue) /*@uses p_ue->ukind@*/ /*@*/ ; -extern /*@falsenull@*/ bool uentry_isFakeTag (uentry p_e) /*@*/ ; -extern /*@falsenull@*/ bool uentry_isIter (uentry p_e) /*@*/ ; -extern /*@falsenull@*/ bool uentry_isMutableDatatype (uentry p_e) /*@*/ ; -extern /*@falsenull@*/ bool uentry_isParam (uentry p_u) /*@*/ ; -extern /*@falsenull@*/ bool uentry_isExpandedMacro (uentry p_u) /*@*/ ; -extern /*@falsenull@*/ bool uentry_isSefParam (uentry p_u) /*@*/ ; -extern /*@falsenull@*/ bool uentry_isAnyParam (/*@special@*/ uentry p_u) +extern /*@falsewhennull@*/ bool uentry_isFakeTag (uentry p_e) /*@*/ ; +extern /*@falsewhennull@*/ bool uentry_isIter (uentry p_e) /*@*/ ; +extern /*@falsewhennull@*/ bool uentry_isMutableDatatype (uentry p_e) /*@*/ ; +extern /*@falsewhennull@*/ bool uentry_isParam (uentry p_u) /*@*/ ; +extern /*@falsewhennull@*/ bool uentry_isExpandedMacro (uentry p_u) /*@*/ ; +extern /*@falsewhennull@*/ bool uentry_isSefParam (uentry p_u) /*@*/ ; +extern /*@falsewhennull@*/ bool uentry_isAnyParam (/*@special@*/ uentry p_u) /*@uses p_u->ukind, p_u->info@*/ /*@*/ ; -extern /*@falsenull@*/ bool uentry_isRealFunction (uentry p_e) /*@*/ ; -extern /*@falsenull@*/ bool uentry_isSpecified (uentry p_e) /*@*/ ; +extern /*@falsewhennull@*/ bool uentry_isRealFunction (uentry p_e) /*@*/ ; +extern /*@falsewhennull@*/ bool uentry_isSpecified (uentry p_e) /*@*/ ; -extern /*@falsenull@*/ bool uentry_isStructTag (/*@special@*/ uentry p_ue) +extern /*@falsewhennull@*/ bool uentry_isStructTag (/*@special@*/ uentry p_ue) /*@uses p_ue->ukind@*/ /*@*/ ; -extern /*@falsenull@*/ bool uentry_isUnionTag (/*@special@*/ uentry p_ue) +extern /*@falsewhennull@*/ bool uentry_isUnionTag (/*@special@*/ uentry p_ue) /*@uses p_ue->ukind@*/ /*@*/ ; -extern /*@falsenull@*/ bool uentry_isVar (/*@special@*/ uentry p_e) +extern /*@falsewhennull@*/ bool uentry_isVar (/*@special@*/ uentry p_e) /*@uses p_e->ukind@*/ /*@*/ ; -extern /*@falsenull@*/ bool uentry_isVariable (/*@special@*/ uentry p_e) +extern /*@falsewhennull@*/ bool uentry_isVariable (/*@special@*/ uentry p_e) /*@uses p_e->ukind@*/ /*@*/ ; extern cstring uentry_dump (uentry p_v) ; extern cstring uentry_dumpParam (uentry p_v); + +extern /*@observer@*/ cstring uentry_observeRealName (uentry p_e) /*@*/ ; + extern cstring uentry_getName (/*@special@*/ uentry p_e) /*@uses p_e->ukind, p_e->info, p_e->uname@*/ /*@*/ ; @@ -350,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@*/ specialClauses uentry_getSpecialClauses (uentry p_ue) /*@*/ ; +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, @@ -386,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) /*@*/ ; @@ -397,19 +404,26 @@ extern /*@notnull@*/ uentry extern /*@notnull@*/ /*@only@*/ uentry uentry_makeConstant (/*@temp@*/ cstring p_n, ctype p_t, /*@keep@*/ fileloc p_f) /*@*/ ; + +extern /*@only@*/ /*@notnull@*/ uentry + uentry_makeConstantValue (/*@temp@*/ cstring p_n, ctype p_t, /*@keep@*/ fileloc p_f, + bool p_priv, /*@only@*/ multiVal p_val) + /*@*/ ; + extern /*@notnull@*/ /*@only@*/ uentry - uentry_makeConstantAux (/*@temp@*/ cstring p_n, ctype p_t, - /*@keep@*/ fileloc p_f, bool p_priv, - /*@only@*/ multiVal p_m) /*@*/ ; + uentry_makeMacroConstant (/*@temp@*/ cstring p_n, ctype p_t, /*@keep@*/ fileloc p_f) + /*@*/ ; + extern /*@notnull@*/ /*@only@*/ uentry - uentry_makeDatatype (/*@temp@*/ cstring p_n, ctype p_t, ynm p_mut, ynm p_abs, + uentry_makeDatatype (/*@temp@*/ cstring p_n, ctype p_t, ynm p_mut, ynm p_abstract, /*@only@*/ fileloc p_f) /*@*/ ; extern /*@notnull@*/ /*@only@*/ uentry uentry_makeDatatypeAux (/*@temp@*/ cstring p_n, ctype p_t, ynm p_mut, - ynm p_abs, /*@keep@*/ fileloc p_f, bool p_priv) /*@*/ ; + ynm 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@*/ ; +extern void uentry_makeConstantFunction (/*@temp@*/ uentry p_ue) /*@modifies p_ue@*/ ; extern bool uentry_isElipsisMarker (/*@sef@*/ uentry p_u) /*@*/ ; # define uentry_isElipsisMarker(u) \ @@ -426,6 +440,7 @@ extern /*@notnull@*/ uentry uentry_makeFunction (cstring p_n, ctype p_t, typeId p_access, /*@only@*/ globSet p_globs, /*@only@*/ sRefSet p_mods, + /*@only@*/ warnClause p_warn, /*@only@*/ fileloc p_f); extern /*@notnull@*/ uentry @@ -446,20 +461,18 @@ 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); -# endif + uentry uentry_makeVariableParam (cstring p_n, ctype p_t, fileloc p_loc); extern /*@notnull@*/ /*@only@*/ - uentry uentry_makeVariableSrefParam (cstring p_n, ctype p_t, - sRef p_s); +uentry uentry_makeVariableSrefParam (cstring p_n, ctype p_t, /*@only@*/ fileloc p_loc, + /*@exposed@*/ sRef p_s); extern /*@notnull@*/ /*@only@*/ uentry uentry_makeIdFunction (idDecl p_id); extern /*@notnull@*/ /*@only@*/ uentry uentry_makeIdDatatype (idDecl p_id); extern /*@notnull@*/ /*@only@*/ - uentry uentry_makeBoolDatatype (ynm p_abs); + uentry uentry_makeBoolDatatype (ynm 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); @@ -490,24 +503,30 @@ extern void uentry_setStatic (uentry p_c); extern void uentry_setModifies (uentry p_ue, /*@owned@*/ sRefSet p_sr) /*@modifies p_ue, p_sr@*/; -extern void uentry_setSpecialClauses (uentry p_ue, /*@only@*/ specialClauses p_clauses) +extern bool uentry_hasWarning (uentry p_ue) /*@*/ ; + +extern void uentry_addWarning (uentry p_ue, /*@only@*/ warnClause p_warn) + /*@modifies p_ue*/; + +extern void uentry_setStateClauseList (uentry p_ue, /*@only@*/ stateClauseList p_clauses) /*@modifies p_ue@*/ ; 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) /*@*/ ; @@ -524,12 +543,15 @@ extern void uentry_setRefParam (uentry p_e) /*@modifies p_e@*/ ; extern void uentry_setDeclaredForce (uentry p_e, fileloc p_f) /*@modifies p_e@*/; extern bool uentry_isNonLocal (uentry p_ue) /*@*/ ; -extern bool uentry_isGlobal (uentry p_ue) /*@*/; +extern bool uentry_isGlobalVariable (uentry p_ue) /*@*/; +extern bool uentry_isVisibleExternally (uentry p_ue) /*@*/; extern bool uentry_isRefParam (uentry p_u) /*@*/ ; extern bool uentry_hasGlobs (uentry p_ue) /*@*/ ; extern bool uentry_hasMods (uentry p_ue) /*@*/ ; -extern bool uentry_hasSpecialClauses (uentry p_ue) /*@*/ ; +extern bool uentry_hasStateClauseList (uentry p_ue) /*@*/ ; +extern bool uentry_hasConditions (uentry p_ue) /*@*/ ; + extern exitkind uentry_getExitCode (uentry p_ue) /*@*/ ; extern void uentry_checkYieldParam (uentry p_old, uentry p_unew); @@ -545,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@*/ ; +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) /*@*/ ; @@ -554,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); @@ -583,18 +605,14 @@ extern void uentry_setCheckedStrict (uentry p_ue) /*@modifies p_ue@*/ ; extern bool uentry_hasAccessType (uentry p_e); -extern /*@exposed@*/ uentry uentry_makeUnrecognized (cstring p_c, /*@keep@*/ fileloc p_loc); - - -/* start modifications */ -//extern void uentry_setBufferSize (uentry p_e, exprNode cconstant); +/*@constant cstring GLOBAL_MARKER_NAME@*/ +# define GLOBAL_MARKER_NAME cstring_makeLiteralTemp ("#GM#") /* functions for making modification to null-term info */ - void uentry_setNullTerminatedState (uentry p_e); - void uentry_setPossiblyNullTerminatedState (uentry p_e); -//extern void uentry_setNotNullTerminated (uentry p_e); -void uentry_setSize(uentry p_e, int p_size); - void uentry_setLen(uentry p_e, int p_len); +extern void uentry_setNullTerminatedState (uentry p_e); +extern void uentry_setPossiblyNullTerminatedState (uentry p_e); +extern void uentry_setSize(uentry p_e, int p_size); +extern void uentry_setLen(uentry p_e, int p_len); /*@i66*/ /*@-nullderef@*/ @@ -604,44 +622,60 @@ extern bool uentry_hasBufStateInfo (uentry p_ue); /*@unused@*/ extern bool uentry_isNullTerminated(/*@sef@*/uentry p_ue); # define uentry_isNullTerminated(p_ue) \ - ( uentry_hasBufStateInfo( (p_ue ) ) ? ( (p_ue)->info->var->bufinfo->bufstate \ + ( uentry_hasBufStateInfo((p_ue ) ) ? ((p_ue)->info->var->bufinfo->bufstate \ == BB_NULLTERMINATED) : FALSE) /*@unused@*/ extern bool uentry_isPossiblyNullTerminated( /*@sef@*/ uentry p_ue); # define uentry_isPossiblyNullTerminated(p_ue) \ - ( uentry_hasBufStateInfo((p_ue)) ? ( (p_ue)->info->var->bufinfo->bufstate \ + ( uentry_hasBufStateInfo((p_ue)) ? ((p_ue)->info->var->bufinfo->bufstate \ == BB_POSSIBLYNULLTERMINATED) : FALSE) /*@unused@*/ extern bool uentry_isNotNullTerminated( /*@sef@*/ uentry p_ue); # define uentry_isNotNullTerminated(p_ue) \ - ( uentry_hasBufStateInfo( (p_ue) ) ? ( (p_ue)->info->var->bufinfo->bufstate \ + ( uentry_hasBufStateInfo((p_ue) ) ? ((p_ue)->info->var->bufinfo->bufstate \ == BB_NOTNULLTERMINATED) : FALSE) /*@=nullderef@*/ /* end modifications */ +extern uentry uentry_makeGlobalMarker (void) ; +extern bool uentry_isGlobalMarker (uentry) /*@*/ ; + +extern /*@exposed@*/ uentry uentry_makeUnrecognized (cstring p_c, /*@only@*/ fileloc p_loc); + # ifdef DOANNOTS -typedef enum { AN_UNKNOWN, AN_FCNRETURN, AN_FCNPARAM, AN_SUFIELD, AN_TDEFN, AN_GSVAR, - AN_CONST, AN_LAST - } ancontext; +typedef enum +{ + AN_UNKNOWN, AN_FCNRETURN, AN_FCNPARAM, AN_SUFIELD, AN_TDEFN, AN_GSVAR, + AN_CONST, AN_LAST +} ancontext; extern void initAnnots (); extern void printAnnots (void); extern void uentry_tallyAnnots (uentry u, ancontext kind); # endif /* DOANNOTS */ +extern bool uentry_hasMetaStateEnsures (uentry p_e) /*@*/ ; +extern /*@only@*/ metaStateConstraintList uentry_getMetaStateEnsures (uentry p_e); + /* start modifications */ -//extern void uentry_setBufferSize (uentry p_e, exprNode p_cconstant); + /*drl7x*/ -extern constraintList uentry_getFcnPreconditions (uentry ue); -extern constraintList uentry_getFcnPostconditions (uentry ue); -extern void -uentry_setPostconditions (uentry ue, /*@only@*/ constraintList postconditions); +extern constraintList uentry_getFcnPreconditions (uentry p_ue); +extern constraintList uentry_getFcnPostconditions (uentry p_ue); -extern void -uentry_setPreconditions (uentry ue, /*@only@*/ constraintList preconditions); +extern void uentry_setPostconditions (uentry p_ue, /*@only@*/ functionConstraint p_postconditions); - /*end mods*/ +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"