X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/4cccc6ad3936684419c0c7613b6d5aa443e5e9ce..8c56b1d88bedb8a9f88581737bf4cc97ff541291:/src/Headers/uentry.h diff --git a/src/Headers/uentry.h b/src/Headers/uentry.h index fcb6788..67d8953 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,9 @@ ** vkind --- need to fix value for consistency in dump files */ -typedef struct _ucinfo +typedef struct { - /*@only@*/ multiVal val; - typeIdSet access; + typeIdSet access; } *ucinfo; typedef enum @@ -47,19 +46,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 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 +69,7 @@ typedef struct _uvinfo } *uvinfo ; /* end modifications */ -typedef struct _udinfo +typedef struct { ynm abs; ynm mut; @@ -88,7 +87,7 @@ typedef enum SPC_LAST } specCode; -typedef struct _ufinfo +typedef struct { qual nullPred; specCode specialCode; @@ -98,26 +97,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; + + 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; } *ueinfo ; -typedef union _uinfo +typedef union { ucinfo uconst; uvinfo var; @@ -127,7 +130,7 @@ typedef union _uinfo ueinfo enditer; } *uinfo ; -struct _uentry +struct s_uentry { ekind ukind; cstring uname; @@ -142,8 +145,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; @@ -159,7 +165,7 @@ 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) @@ -291,6 +297,8 @@ extern /*@falsenull@*/ 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) @@ -323,6 +331,9 @@ extern /*@falsenull@*/ bool uentry_isVariable (/*@special@*/ uentry p_e) 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@*/ /*@*/ ; @@ -348,7 +359,7 @@ extern /*@notnull@*/ uentry uentry_makeExpandedMacro (cstring p_s, extern void uentry_checkMatchParam (uentry p_u1, uentry p_u2, int p_paramno, exprNode p_e) /*@modifies g_msgstream@*/ ; -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@*/ ; @@ -398,14 +409,15 @@ extern /*@notnull@*/ /*@only@*/ uentry /*@keep@*/ fileloc p_f, bool p_priv, /*@only@*/ multiVal p_m) /*@*/ ; 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) \ @@ -422,6 +434,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 @@ -444,18 +457,18 @@ extern /*@notnull@*/ /*@only@*/ uentry # ifndef NOLCL extern /*@notnull@*/ /*@only@*/ - uentry uentry_makeVariableParam (cstring p_n, ctype p_t); + 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, - 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); @@ -486,7 +499,12 @@ 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); @@ -520,12 +538,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); @@ -541,7 +562,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, /*@owned@*/ 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) /*@*/ ; @@ -579,16 +600,12 @@ 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 */ extern void uentry_setNullTerminatedState (uentry p_e); extern void uentry_setPossiblyNullTerminatedState (uentry p_e); -extern void uentry_setNotNullTerminated (uentry p_e); extern void uentry_setSize(uentry p_e, int p_size); extern void uentry_setLen(uentry p_e, int p_len); @@ -598,17 +615,17 @@ extern bool uentry_hasBufStateInfo (uentry p_ue); # define uentry_hasBufStateInfo(p_ue) \ (((p_ue)->info->var->bufinfo != NULL) ? TRUE : FALSE) -extern bool uentry_isNullTerminated(/*@sef@*/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 \ == BB_NULLTERMINATED) : FALSE) -extern bool uentry_isPossiblyNullTerminated( /*@sef@*/ uentry p_ue); +/*@unused@*/ extern bool uentry_isPossiblyNullTerminated( /*@sef@*/ uentry p_ue); # define uentry_isPossiblyNullTerminated(p_ue) \ ( uentry_hasBufStateInfo((p_ue)) ? ( (p_ue)->info->var->bufinfo->bufstate \ == BB_POSSIBLYNULLTERMINATED) : FALSE) -extern bool uentry_isNotNullTerminated( /*@sef@*/ uentry p_ue); +/*@unused@*/ extern bool uentry_isNotNullTerminated( /*@sef@*/ uentry p_ue); # define uentry_isNotNullTerminated(p_ue) \ ( uentry_hasBufStateInfo( (p_ue) ) ? ( (p_ue)->info->var->bufinfo->bufstate \ == BB_NOTNULLTERMINATED) : FALSE) @@ -616,6 +633,11 @@ extern bool uentry_isNotNullTerminated( /*@sef@*/ uentry p_ue); /* 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 @@ -626,8 +648,19 @@ 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 p_ue); +extern constraintList uentry_getFcnPostconditions (uentry p_ue); + +extern void uentry_setPostconditions (uentry p_ue, /*@only@*/ functionConstraint p_postconditions); + +extern void uentry_setPreconditions (uentry p_ue, /*@only@*/ functionConstraint p_preconditions); +/*end mods*/ # else # error "Multiple include"