X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/dc92450fdc57d377a0b65c158540a5e41b61fa9a..abd7f89523564e5e238e5852585b98f72c3b48f4:/src/Headers/sRef.h diff --git a/src/Headers/sRef.h b/src/Headers/sRef.h index 0bc6d92..0b007f1 100644 --- a/src/Headers/sRef.h +++ b/src/Headers/sRef.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. ** */ @@ -22,7 +22,8 @@ typedef enum { SR_NOTHING, SR_INTERNAL, SR_SPECSTATE, - SR_SYSTEM + SR_SYSTEM, + SR_GLOBALMARKER } speckind; typedef enum { @@ -45,67 +46,65 @@ typedef enum { SK_UNKNOWN } skind; -typedef struct _cref +typedef struct { int lexlevel; usymId index; } *cref; -typedef struct _ainfo +typedef struct { /*@exposed@*/ /*@notnull@*/ sRef arr; bool indknown; int ind; } *ainfo; -typedef struct _fldinfo +typedef struct { /*@exposed@*/ /*@notnull@*/ sRef rec; /*@observer@*/ cstring field; } *fldinfo ; -typedef struct _cjinfo +typedef struct { /*@exposed@*/ /*@notnull@*/ sRef a; /*@exposed@*/ /*@notnull@*/ sRef b; } *cjinfo ; -typedef union _sinfo +typedef union { /*@only@*/ cref cvar; int paramno; /*@only@*/ ainfo arrayfetch; - /*@only@*/ fldinfo field; + /*@only@*/ fldinfo field; ctype object; /*@observer@*/ cstring fname; /* unconstrained, new */ - /*@exposed@*/ /*@notnull@*/ sRef ref; + /*@exposed@*/ /*@notnull@*/ sRef ref; /*@only@*/ cjinfo conj; speckind spec; } *sinfo; -typedef /*@null@*/ struct _alinfo -{ - /*@only@*/ fileloc loc; - /*@observer@*/ sRef ref; - /*@observer@*/ uentry ue; -} *alinfo; - -struct _sRef +struct s_sRef { /* does it need to be inside parens (macros) */ - bool safe BOOLBITS; + bool safe; /* has it been modified */ - bool modified BOOLBITS; + bool modified; /* BOOLBITS; */ + + /* for debugging: make this sRef as immutable. */ + bool immut; /* BOOLBITS; */ skind kind; ctype type; + multiVal val; /* Some sRef's have known values */ + sstate defstate; nstate nullstate; /* start modifications: We keep a track of the buf state(nullterm info)*/ - struct _bbufinfo bufinfo; + struct s_bbufinfo bufinfo; /* end modifications */ alkind aliaskind; @@ -115,37 +114,44 @@ struct _sRef exkind oexpkind; /* where it becomes observer/exposed */ - /*@null@*/ /*@only@*/ alinfo expinfo; + /*@null@*/ /*@only@*/ stateInfo expinfo; /* where it changed alias kind */ - /*@null@*/ /*@only@*/ alinfo aliasinfo; + /*@null@*/ /*@only@*/ stateInfo aliasinfo; /* where it is defined/allocated */ - /*@null@*/ /*@only@*/ alinfo definfo; + /*@null@*/ /*@only@*/ stateInfo definfo; - /* where it changes null state */ - /*@null@*/ /*@only@*/ alinfo nullinfo; + /* where it is null */ + /*@null@*/ /*@only@*/ stateInfo nullinfo; /*@only@*/ /*@relnull@*/ sinfo info; /* stores fields for structs, elements for arrays, derefs for pointers */ /*@only@*/ sRefSet deriv; + + /* sRef's include a lookup table of state variables. */ + /*@only@*/ valueTable state; } ; extern bool sRef_perhapsNull (sRef p_s); extern bool sRef_possiblyNull (sRef p_s); extern bool sRef_definitelyNull (sRef p_s); +extern bool sRef_definitelyNullContext (sRef p_s); +extern bool sRef_definitelyNullAltContext (sRef p_s); + extern void sRef_setNullError (sRef p_s); extern void sRef_setNullUnknown (sRef p_s, fileloc p_loc); extern void sRef_setNotNull (sRef p_s, fileloc p_loc); extern void sRef_setNullState (sRef p_s, nstate p_n, fileloc p_loc); +extern void sRef_setNullStateN (sRef p_s, nstate p_n); extern void sRef_setNullStateInnerComplete (sRef p_s, nstate p_n, fileloc p_loc); extern void sRef_setPosNull (sRef p_s, fileloc p_loc); extern void sRef_setDefNull (sRef p_s, fileloc p_loc); -extern /*@truenull@*/ bool sRef_isInvalid (sRef p_s) /*@*/ ; -extern /*@falsenull@*/ bool sRef_isValid (sRef p_s) /*@*/ ; +extern /*@nullwhentrue@*/ bool sRef_isInvalid (sRef p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool sRef_isValid (sRef p_s) /*@*/ ; /*@constant null sRef sRef_undefined; @*/ # define sRef_undefined ((sRef) NULL) @@ -157,14 +163,13 @@ extern void sRef_copyRealDerivedComplete (sRef p_s1, sRef p_s2) /*@modifies p_s1 extern nstate sRef_getNullState (/*@sef@*/ sRef p_s) /*@*/ ; extern bool sRef_isNotNull (sRef p_s) /*@*/ ; -# define sRef_getNullState(s) (sRef_isValid(s) ? (s)->nullstate : NS_UNKNOWN) extern bool sRef_isDefinitelyNull (sRef p_s) /*@*/ ; -extern /*@falsenull@*/ bool sRef_isLocalVar (sRef p_s) /*@*/ ; -extern /*@falsenull@*/ bool sRef_isNSLocalVar (sRef p_s) /*@*/ ; -extern /*@falsenull@*/ bool sRef_isRealLocalVar (sRef p_s) /*@*/ ; -extern /*@falsenull@*/ bool sRef_isLocalParamVar (sRef p_s) /*@*/ ; -extern /*@falsenull@*/ bool sRef_isKnown (/*@sef@*/ sRef p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool sRef_isLocalVar (sRef p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool sRef_isNSLocalVar (sRef p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool sRef_isRealLocalVar (sRef p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool sRef_isLocalParamVar (sRef p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool sRef_isKnown (/*@sef@*/ sRef p_s) /*@*/ ; extern bool sRef_hasLastReference (sRef p_s) /*@*/ ; # define sRef_hasLastReference(s) (sRef_hasAliasInfoRef (s)) @@ -193,12 +198,11 @@ extern bool sRef_stateKnown (/*@sef@*/ sRef p_s) /*@*/ ; # define sRef_stateKnown(s) (sRef_isValid(s) && (s)->defstate != SS_UNKNOWN) extern alkind sRef_getAliasKind (/*@sef@*/ sRef p_s) /*@*/ ; -# define sRef_getAliasKind(s) (sRef_isValid(s) ? (s)->aliaskind : AK_ERROR) extern alkind sRef_getOrigAliasKind (/*@sef@*/ sRef p_s) /*@*/ ; # define sRef_getOrigAliasKind(s) (sRef_isValid(s) ? (s)->oaliaskind : AK_ERROR) -extern /*@falsenull@*/ bool sRef_isConj (/*@sef@*/ sRef p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool sRef_isConj (/*@sef@*/ sRef p_s) /*@*/ ; # define sRef_isConj(s) (sRef_isValid(s) && (s)->kind == SK_CONJ) extern /*@exposed@*/ sRef sRef_buildArrow (sRef p_s, /*@dependent@*/ cstring p_f); @@ -213,7 +217,7 @@ extern void sRef_clearDerived (sRef p_s); extern void sRef_clearDerivedComplete (sRef p_s); extern /*@exposed@*/ sRef sRef_getBaseSafe (sRef p_s); -extern /*@observer@*/ sRefSet sRef_derivedFields (/*@dependent@*/ sRef p_rec) /*@*/ ; +extern /*@observer@*/ sRefSet sRef_derivedFields (/*@temp@*/ sRef p_rec) /*@*/ ; extern bool sRef_sameName (sRef p_s1, sRef p_s2) /*@*/ ; extern bool sRef_isDirectParam (sRef p_s) /*@*/ ; extern /*@exposed@*/ sRef sRef_makeAnyArrayFetch (/*@exposed@*/ sRef p_arr); @@ -230,36 +234,39 @@ extern bool sRef_aliasCompleteSimplePred (bool (p_predf) (sRef), sRef p_s); extern void sRef_clearExKindComplete (sRef p_s, fileloc p_loc); -extern /*@falsenull@*/ bool sRef_isKindSpecial (/*@sef@*/ sRef p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool sRef_isKindSpecial (/*@sef@*/ sRef p_s) /*@*/ ; # define sRef_isKindSpecial(s) (sRef_isValid (s) && (s)->kind == SK_SPECIAL) extern /*@observer@*/ cstring sRef_nullMessage (sRef p_s) /*@*/ ; extern bool sRef_isSystemState (sRef p_s) /*@*/ ; +extern bool sRef_isGlobalMarker (sRef p_s) /*@*/ ; extern bool sRef_isInternalState (sRef p_s) /*@*/ ; extern bool sRef_isResult (sRef p_s) /*@*/ ; extern bool sRef_isSpecInternalState (sRef p_s) /*@*/ ; extern bool sRef_isSpecState (sRef p_s) /*@*/ ; extern bool sRef_isNothing (sRef p_s) /*@*/ ; -extern bool sRef_isGlobal (sRef p_s) /*@*/ ; +extern bool sRef_isFileOrGlobalScope (sRef p_s) /*@*/ ; extern bool sRef_isReference (sRef p_s) /*@*/ ; extern ctype sRef_deriveType (sRef p_s, uentryList p_cl) /*@*/ ; extern ctype sRef_getType (sRef p_s) /*@*/ ; -extern /*@falsenull@*/ bool sRef_isAddress (sRef p_s) /*@*/ ; -extern /*@falsenull@*/ bool sRef_isArrayFetch (sRef p_s) /*@*/ ; -extern /*@falsenull@*/ bool sRef_isConst (sRef p_s) /*@*/ ; -extern /*@falsenull@*/ bool sRef_isCvar (sRef p_s) /*@*/ ; -extern /*@falsenull@*/ bool sRef_isField (sRef p_s) /*@*/ ; -extern /*@falsenull@*/ bool sRef_isParam (sRef p_s) /*@*/ ; -extern /*@falsenull@*/ bool sRef_isPointer (sRef p_s) /*@*/ ; +extern void sRef_markImmutable (sRef p_s) /*@modifies p_s@*/ ; + +extern /*@falsewhennull@*/ bool sRef_isAddress (sRef p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool sRef_isArrayFetch (sRef p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool sRef_isConst (sRef p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool sRef_isCvar (sRef p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool sRef_isField (sRef p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool sRef_isParam (sRef p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool sRef_isPointer (sRef p_s) /*@*/ ; extern void sRef_setType (sRef p_s, ctype p_t); extern void sRef_setTypeFull (sRef p_s, ctype p_t); extern void sRef_mergeNullState (sRef p_s, nstate p_n); -extern void sRef_setLastReference (sRef p_s, sRef p_ref, fileloc p_loc); +extern void sRef_setLastReference (/*@temp@*/ sRef p_s, /*@exposed@*/ sRef p_ref, fileloc p_loc); extern bool sRef_canModify (sRef p_s, sRefSet p_sl) /*@modifies p_s@*/ ; extern bool sRef_canModifyVal (sRef p_s, sRefSet p_sl) /*@modifies p_s@*/ ; extern bool sRef_isIReference (sRef p_s) /*@*/ ; @@ -269,6 +276,7 @@ extern bool sRef_isModified (sRef p_s) /*@*/ ; extern bool sRef_isExternallyVisible (sRef p_s) /*@*/ ; extern int sRef_compare (sRef p_s1, sRef p_s2) /*@*/ ; extern bool sRef_realSame (sRef p_s1, sRef p_s2) /*@*/ ; +extern bool sRef_sameObject (sRef p_s1, sRef p_s2) /*@*/ ; extern bool sRef_same (sRef p_s1, sRef p_s2) /*@*/ ; extern bool sRef_similar (sRef p_s1, sRef p_s2) /*@*/ ; extern /*@observer@*/ cstring sRef_getField (sRef p_s) /*@*/ ; @@ -280,28 +288,34 @@ extern /*@only@*/ cstring sRef_unparseDebug (sRef p_s) /*@*/ ; extern void sRef_killComplete (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ; extern int sRef_getIndex (sRef p_arr) /*@*/ ; extern /*@dependent@*/ sRef sRef_fixOuterRef (/*@returned@*/ sRef p_s); -extern void sRef_setDefinedComplete (sRef p_s, fileloc p_loc); -extern void sRef_setDefinedNCComplete (sRef p_s, fileloc p_loc); + +/* Use this one to clear after error */ +extern void sRef_setDefinedCompleteDirect (sRef p_s, fileloc p_loc) ; + +extern void sRef_setDefinedComplete (sRef p_s, fileloc p_loc) ; +extern void sRef_setDefinedNCComplete (sRef p_s, fileloc p_loc) ; extern int sRef_getParam (sRef p_s) /*@*/ ; extern int sRef_lexLevel (sRef p_s) /*@*/ ; extern void sRef_setOrigAliasKind (sRef p_s, alkind p_kind); + extern /*@exposed@*/ sRef - sRef_fixBase (/*@returned@*/ sRef p_s, /*@returned@*/ sRef p_base) + sRef_fixBase (/*@returned@*/ sRef p_s, /*@returned@*/ sRef p_base) /*@modifies p_s, p_base@*/ ; extern void sRef_showNotReallyDefined (sRef p_s) /*@modifies g_msgstream@*/ ; -extern void sRef_enterFunctionScope (void); -extern void sRef_setGlobalScope (void); -extern void sRef_exitFunctionScope (void); -extern void sRef_clearGlobalScopeSafe (void); -extern void sRef_setGlobalScopeSafe (void); +extern void sRef_enterFunctionScope (void) /*@modifies internalState@*/ ; +extern void sRef_setGlobalScope (void) /*@modifies internalState@*/ ; +extern bool sRef_inGlobalScope (void) /*@*/ ; +extern void sRef_exitFunctionScope (void) /*@modifies internalState@*/ ; +extern void sRef_clearGlobalScopeSafe (void) /*@modifies internalState@*/ ; +extern void sRef_setGlobalScopeSafe (void) /*@modifies internalState@*/ ; extern /*@notnull@*/ /*@exposed@*/ sRef sRef_buildArrayFetch (/*@exposed@*/ sRef p_arr); extern /*@notnull@*/ /*@exposed@*/ sRef sRef_buildArrayFetchKnown (/*@exposed@*/ sRef p_arr, int p_i); extern /*@exposed@*/ sRef - sRef_buildField (sRef p_rec, /*@dependent@*/ cstring p_f) + sRef_buildField (/*@exposed@*/ sRef p_rec, /*@dependent@*/ cstring p_f) /*@modifies p_rec@*/ ; extern /*@exposed@*/ sRef sRef_buildPointer (/*@exposed@*/ sRef p_t) /*@modifies p_t@*/ ; @@ -309,49 +323,50 @@ extern /*@exposed@*/ sRef sRef_buildPointer (/*@exposed@*/ sRef p_t) extern /*@exposed@*/ sRef sRef_makeAddress (/*@exposed@*/ sRef p_t); extern /*@notnull@*/ /*@dependent@*/ sRef sRef_makeUnconstrained (/*@exposed@*/ cstring) /*@*/ ; -extern /*@falsenull@*/ bool sRef_isUnconstrained (sRef p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool sRef_isUnconstrained (sRef p_s) /*@*/ ; extern /*@observer@*/ cstring sRef_unconstrainedName (sRef p_s) /*@*/ ; -extern /*@notnull@*/ /*@exposed@*/ sRef sRef_makeArrayFetch (sRef p_arr) /*@*/ ; +extern /*@notnull@*/ /*@exposed@*/ sRef sRef_makeArrayFetch (/*@exposed@*/ sRef p_arr) /*@*/ ; extern /*@notnull@*/ /*@exposed@*/ sRef - sRef_makeArrayFetchKnown (sRef p_arr, int p_i); + sRef_makeArrayFetchKnown (/*@exposed@*/ sRef p_arr, int p_i); extern /*@notnull@*/ /*@dependent@*/ sRef sRef_makeConj (/*@exposed@*/ /*@returned@*/ sRef p_a, /*@exposed@*/ sRef p_b); extern /*@notnull@*/ /*@dependent@*/ sRef - sRef_makeCvar (int p_level, usymId p_index, ctype p_ct); + sRef_makeCvar (int p_level, usymId p_index, ctype p_ct, /*@only@*/ stateInfo p_stinfo); extern /*@notnull@*/ /*@dependent@*/ sRef sRef_makeConst (ctype p_ct); extern /*@exposed@*/ sRef sRef_makeField (sRef p_rec, /*@dependent@*/ cstring p_f); extern /*@notnull@*/ /*@dependent@*/ sRef - sRef_makeGlobal (usymId p_l, ctype p_ct); + sRef_makeGlobal (usymId p_l, ctype p_ct, /*@only@*/ stateInfo); extern /*@exposed@*/ sRef - sRef_makeNCField (sRef p_rec, /*@dependent@*/ cstring p_f) /*@*/ ; + sRef_makeNCField (/*@exposed@*/ sRef p_rec, /*@dependent@*/ cstring p_f) /*@*/ ; extern void sRef_maybeKill (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ; extern /*@unused@*/ /*@notnull@*/ /*@dependent@*/ sRef sRef_makeObject (ctype p_o) /*@*/ ; extern /*@notnull@*/ /*@dependent@*/ sRef sRef_makeType (ctype p_ct) /*@*/ ; -extern /*@notnull@*/ /*@dependent@*/ sRef sRef_makeParam (int p_l, ctype p_ct) /*@*/ ; -extern /*@exposed@*/ sRef sRef_makePointer (sRef p_s) /*@modifies p_s@*/ ; +extern /*@notnull@*/ /*@dependent@*/ sRef sRef_makeParam (int p_l, ctype p_ct, /*@only@*/ stateInfo p_stinfo) /*@*/ ; +extern /*@exposed@*/ sRef sRef_makePointer (/*@exposed@*/ sRef p_s) /*@modifies p_s@*/ ; extern void sRef_makeSafe (sRef p_s) /*@modifies p_s@*/ ; extern void sRef_makeUnsafe (sRef p_s) /*@modifies p_s@*/ ; -extern sRef sRef_makeUnknown (void) /*@*/ ; -extern sRef sRef_makeNothing (void) /*@*/ ; -extern sRef sRef_makeInternalState (void) /*@*/ ; -extern sRef sRef_makeSpecState (void) /*@*/ ; -extern sRef sRef_makeSystemState (void) /*@*/ ; +extern /*@dependent@*/ sRef sRef_makeUnknown (void) /*@*/ ; +extern /*@dependent@*/ sRef sRef_makeNothing (void) /*@*/ ; +extern /*@dependent@*/ sRef sRef_makeInternalState (void) /*@*/ ; +extern /*@dependent@*/ sRef sRef_makeSpecState (void) /*@*/ ; +extern /*@dependent@*/ sRef sRef_makeGlobalMarker (void) /*@*/ ; +extern /*@dependent@*/ sRef sRef_makeSystemState (void) /*@*/ ; -extern /*@notnull@*/ sRef sRef_makeResult (void) /*@*/ ; +extern /*@dependent@*/ /*@notnull@*/ sRef sRef_makeResult (ctype) /*@*/ ; extern /*@exposed@*/ sRef sRef_fixResultType (/*@returned@*/ sRef p_s, ctype p_typ, uentry p_ue) /*@modifies p_s@*/; extern void sRef_setParamNo (sRef p_s, int p_l) /*@modifies p_s;@*/; -extern /*@notnull@*/ sRef - sRef_makeNew (ctype p_ct, sRef p_t, /*@exposed@*/ cstring p_name); +extern /*@notnull@*/ /*@dependent@*/ sRef + sRef_makeNew (ctype p_ct, sRef p_t, /*@exposed@*/ cstring p_name) ; extern usymId sRef_getScopeIndex (sRef p_s) /*@*/ ; extern /*@exposed@*/ uentry sRef_getBaseUentry (sRef p_s); @@ -365,7 +380,8 @@ extern /*@exposed@*/ sRef added function 12/24/2000 */ -extern constraintExpr sRef_fixConstraintParam ( sRef p_s, exprNodeList p_args); + +/*@only@*/ constraintExpr sRef_fixConstraintParam (/*@observer@*/ sRef p_s, /*@observer@*/ /*@temp@*/ exprNodeList p_args); extern bool sRef_isUnionField (sRef p_s); extern void sRef_setModified (sRef p_s); @@ -389,7 +405,7 @@ extern /*@dependent@*/ sRef sRef_copy (sRef p_s); extern cstring sRef_unparseState (sRef p_s) /*@*/ ; extern ynm sRef_isWriteable (sRef p_s) /*@*/ ; -extern ynm sRef_isReadable (sRef p_s) /*@*/ ; +extern ynm sRef_isValidLvalue (sRef p_s) /*@*/ ; extern bool sRef_isStrictReadable (sRef p_s) /*@*/ ; extern bool sRef_hasNoStorage (sRef p_s) /*@*/ ; extern void sRef_showExpInfo (sRef p_s) /*@modifies g_msgstream*/ ; @@ -403,6 +419,7 @@ extern void sRef_setKeptComplete (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ; extern void sRef_setFresh (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ; extern void sRef_setShared (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ; extern void sRef_showAliasInfo (sRef p_s) /*@modifies g_msgstream@*/ ; +extern void sRef_showMetaStateInfo (sRef p_s, cstring p_key) /*@modifies g_msgstream@*/ ; extern void sRef_showNullInfo (sRef p_s) /*@modifies g_msgstream@*/ ; extern void sRef_showStateInfo (sRef p_s) /*@modifies g_msgstream@*/ ; extern void sRef_setStateFromType (sRef p_s, ctype p_ct) /*@modifies p_s@*/ ; @@ -411,18 +428,18 @@ extern void sRef_setAllocated (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ; extern void sRef_setAllocatedShallowComplete (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ; extern void sRef_setAllocatedComplete (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ; extern /*@only@*/ cstring sRef_unparseKindNamePlain (sRef p_s) /*@*/ ; -extern /*@falsenull@*/ bool sRef_isRealGlobal(sRef p_s) /*@*/ ; -extern /*@falsenull@*/ bool sRef_isFileStatic (sRef p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool sRef_isRealGlobal(sRef p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool sRef_isFileStatic (sRef p_s) /*@*/ ; extern int sRef_getScope (sRef p_s) /*@*/ ; extern /*@observer@*/ cstring sRef_getScopeName (sRef p_s) /*@*/ ; /* must be real function (passed as function param) */ -extern /*@falsenull@*/ bool sRef_isDead (sRef p_s) /*@*/ ; -extern /*@falsenull@*/ bool sRef_isDeadStorage (sRef p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool sRef_isDead (sRef p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool sRef_isDeadStorage (sRef p_s) /*@*/ ; extern bool sRef_isStateLive (sRef p_s) /*@*/ ; -extern /*@falsenull@*/ bool sRef_isPossiblyDead (sRef p_s) /*@*/ ; -extern /*@truenull@*/ bool sRef_isStateUndefined (sRef p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool sRef_isPossiblyDead (sRef p_s) /*@*/ ; +extern /*@nullwhentrue@*/ bool sRef_isStateUndefined (sRef p_s) /*@*/ ; extern bool sRef_isUnuseable (sRef p_s) /*@*/ ; extern /*@exposed@*/ sRef sRef_constructDeref (sRef p_t) @@ -433,7 +450,7 @@ extern /*@exposed@*/ sRef sRef_constructDeadDeref (sRef p_t) extern bool sRef_isJustAllocated (sRef p_s) /*@*/ ; -extern /*@falsenull@*/ bool sRef_isAllocated (sRef p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool sRef_isAllocated (sRef p_s) /*@*/ ; extern bool sRef_isUndefGlob (/*@sef@*/ sRef p_s) /*@*/ ; # define sRef_isUndefGlob(s) \ @@ -457,6 +474,10 @@ extern bool sRef_isStateSpecial (/*@sef@*/ sRef p_s) /*@*/ ; # define sRef_isStateSpecial(s) \ ((sRef_isValid(s)) && ((s)->defstate == SS_SPECIAL)) +extern bool sRef_makeStateSpecial (sRef p_s) + /*@modifies p_s@*/ + /* returns false is sRef already has an inconsistend defstate */ ; + extern bool sRef_isStateDefined (/*@sef@*/ sRef p_s) /*@*/ ; # define sRef_isStateDefined(s) \ ((sRef_isValid(s)) && (((s)->defstate == SS_DEFINED) \ @@ -468,7 +489,7 @@ extern bool sRef_isAnyDefined (/*@sef@*/ sRef p_s) /*@*/ ; || ((s)->defstate == SS_RELDEF) \ || ((s)->defstate == SS_PARTIAL))) -extern /*@falsenull@*/ bool sRef_isPdefined (/*@sef@*/ sRef p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool sRef_isPdefined (/*@sef@*/ sRef p_s) /*@*/ ; # define sRef_isPdefined(s) \ ((sRef_isValid(s)) && ((s)->defstate == SS_PDEFINED)) @@ -478,15 +499,15 @@ extern bool sRef_isStateUnknown (/*@sef@*/ sRef p_s) /*@*/ ; # define sRef_isStateUnknown(s) \ ((sRef_isValid(s)) && ((s)->defstate == SS_UNKNOWN)) -extern /*@falsenull@*/ bool sRef_isRefCounted (/*@sef@*/ sRef p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool sRef_isRefCounted (/*@sef@*/ sRef p_s) /*@*/ ; # define sRef_isRefCounted(s) \ ((sRef_isValid(s)) && ((s)->aliaskind == AK_REFCOUNTED)) -extern /*@falsenull@*/ bool sRef_isNewRef (/*@sef@*/ sRef p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool sRef_isNewRef (/*@sef@*/ sRef p_s) /*@*/ ; # define sRef_isNewRef(s) \ ((sRef_isValid(s)) && ((s)->aliaskind == AK_NEWREF)) -extern /*@falsenull@*/ bool sRef_isKillRef (/*@sef@*/ sRef p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool sRef_isKillRef (/*@sef@*/ sRef p_s) /*@*/ ; # define sRef_isKillRef(s) \ ((sRef_isValid(s)) && ((s)->aliaskind == AK_KILLREF)) @@ -522,10 +543,10 @@ extern void sRef_setExKind (sRef p_s, exkind p_exp, fileloc p_loc) /*@modifies p extern void sRef_setExposed (sRef p_s, fileloc p_loc) /*@modifies p_s@*/; extern bool sRef_isAnyParam (sRef p_s) /*@*/ ; -extern /*@observer@*/ sRef sRef_getAliasInfoRef (/*@exposed@*/ sRef p_s) /*@*/ ; +extern /*@observer@*/ sRef sRef_getAliasInfoRef (/*@temp@*/ sRef p_s) /*@*/ ; extern bool sRef_hasAliasInfoRef (sRef p_s) /*@*/ ; -extern /*@exposed@*/ sRef sRef_constructPointer (sRef p_t) /*@modifies p_t*/ ; +extern /*@exposed@*/ sRef sRef_constructPointer (/*@exposed@*/ sRef p_t) /*@modifies p_t*/ ; extern bool sRef_isAliasCheckedGlobal (sRef p_s) /*@*/ ; extern bool sRef_includedBy (sRef p_small, sRef p_big) /*@*/ ; extern /*@dependent@*/ /*@exposed@*/ sRef sRef_makeExternal (/*@exposed@*/ sRef p_t) /*@*/ ; @@ -544,7 +565,7 @@ extern void sRef_mergeOptState (sRef p_res, sRef p_other, clause p_cl, fileloc p /*@modifies p_res, p_other@*/ ; extern void sRef_mergeStateQuiet (sRef p_res, sRef p_other) /*@modifies p_res@*/ ; -extern void sRef_mergeStateQuietReverse (sRef p_res, sRef p_other) +extern void sRef_mergeStateQuietReverse (/*@dependent@*/ sRef p_res, /*@dependent@*/ sRef p_other) /*@modifies p_res@*/ ; extern void sRef_setStateFromUentry (sRef p_s, uentry p_ue) /*@modifies p_s@*/ ; @@ -559,7 +580,7 @@ extern void sRef_setDerivNullState (sRef p_set, sRef p_guide, nstate p_ns) extern void sRef_clearGlobalScope (void) /*@modifies internalState@*/ ; -extern sRef sRef_makeDerived (/*@exposed@*/ sRef p_t); +extern /*@dependent@*/ sRef sRef_makeDerived (/*@exposed@*/ sRef p_t); extern sstate sRef_getDefState (sRef p_s) /*@*/ ; extern void sRef_setDefState (sRef p_s, sstate p_defstate, fileloc p_loc); @@ -567,6 +588,9 @@ extern void sRef_showRefLost (sRef p_s); extern void sRef_showRefKilled (sRef p_s); extern /*@exposed@*/ sRef sRef_updateSref (sRef p_s); +extern void sRef_reflectAnnotation (sRef p_s, annotationInfo p_a, fileloc p_loc); +extern /*@observer@*/ valueTable sRef_getValueTable (sRef p_s) /*@*/ ; + extern void sRef_aliasCheckPred (bool (p_predf) (sRef, exprNode, sRef, exprNode), /*@null@*/ bool (p_checkAliases) (sRef), sRef p_s, exprNode p_e, exprNode p_err); @@ -586,15 +610,13 @@ extern /*@exposed@*/ /*@notnull@*/ sRef sRef_getConjB (sRef p_s) /*@*/ ; extern /*@only@*/ cstring sRef_unparsePreOpt (sRef p_s) /*@*/ ; extern bool sRef_hasName (sRef p_s) /*@*/ ; - extern void sRef_free (/*@only@*/ sRef p_s); - extern void sRef_setObserver (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ; /* start modifications */ /* functions for making modification to null-term info */ -extern void sRef_setNullTerminatedStateInnerComplete(sRef p_s, struct _bbufinfo p_b, fileloc p_loc); -extern struct _bbufinfo sRef_getNullTerminatedState(sRef p_s); +extern void sRef_setNullTerminatedStateInnerComplete(sRef p_s, struct s_bbufinfo p_b, fileloc p_loc); +extern struct s_bbufinfo sRef_getNullTerminatedState(sRef p_s); extern void sRef_setNullTerminatedState (sRef p_s); extern void sRef_setPossiblyNullTerminatedState (sRef p_s); extern void sRef_setNotNullTerminatedState (sRef p_s); @@ -602,6 +624,9 @@ extern void sRef_setSize(sRef p_s, int p_size); extern void sRef_setLen(sRef p_s, int p_len); extern int sRef_getSize(sRef p_s); + +/*@-nullderef@*/ + #define sRef_getSize(p_s) \ ((p_s)->bufinfo.size) @@ -609,33 +634,69 @@ extern int sRef_getLen(sRef p_s); #define sRef_getLen(p_s) \ ((p_s)->bufinfo.len) -extern void sRef_hasBufStateInfo(sRef p_s); +extern bool sRef_hasBufStateInfo(sRef p_s); # define sRef_hasBufStateInfo(p_s) \ (sRef_isValid(p_s)) -extern bool sRef_isNullTerminated(sRef p_s); +extern bool sRef_isNullTerminated(/*@sef@*/sRef p_s); # define sRef_isNullTerminated(p_s) \ - ( sRef_hasBufStateInfo(p_s) ? (p_s->bufinfo.bufstate \ + ( sRef_hasBufStateInfo((p_s)) ? ((p_s)->bufinfo.bufstate \ == BB_NULLTERMINATED) : FALSE) -extern bool sRef_isPossiblyNullTerminated(sRef p_s); +extern bool sRef_isPossiblyNullTerminated(/*@sef@*/sRef p_s); # define sRef_isPossiblyNullTerminated(p_s) \ - ( sRef_hasBufStateInfo((p_s)) ? ( (p_s)->bufinfo.bufstate \ + ( sRef_hasBufStateInfo((p_s)) ? ((p_s)->bufinfo.bufstate \ == BB_POSSIBLYNULLTERMINATED) : FALSE) -extern bool sRef_isNotNullTerminated(sRef p_s); +extern bool sRef_isNotNullTerminated(/*@sef@*/sRef p_s); # define sRef_isNotNullTerminated(p_s) \ - ( sRef_hasBufStateInfo(p_s) ? (p_s->bufinfo.bufstate \ + ( sRef_hasBufStateInfo((p_s)) ? ((p_s)->bufinfo.bufstate \ == BB_NOTNULLTERMINATED) : FALSE) +/*@=nullderef@*/ + + /*drl7x 11/28/00*/ extern bool sRef_isFixedArray (sRef p_s) /*@*/; extern long int sRef_getArraySize (sRef p_s) /*@*/; extern /*@observer@*/ cstring sRef_ntMessage (sRef p_s); +extern void sRef_resetLen (sRef p_s) /*@modifies p_s@*/ ; + /* end modifications */ +extern void sRef_setMetaStateValueComplete (sRef p_s, cstring p_key, int p_value, fileloc p_loc) + /*@modifies p_s@*/ ; + +extern void sRef_setMetaStateValue (sRef p_s, cstring p_key, int p_value, fileloc p_loc) + /*@modifies p_s@*/ ; + +extern /*@observer@*/ stateValue sRef_getMetaStateValue (sRef p_s, cstring p_key) /*@*/ ; + +extern bool sRef_checkMetaStateValue (sRef p_s, cstring p_key, int p_value) + /*@modifies p_s@*/ ; + +extern void sRef_setValue (sRef p_s, /*@only@*/ multiVal p_val) /*@modifies p_s@*/ ; +extern bool sRef_hasValue (sRef p_s) /*@*/ ; +extern /*@observer@*/ multiVal sRef_getValue (sRef p_s) /*@*/ ; + +extern /*@maynotreturn@*/ void sRef_checkValid (/*@temp@*/ sRef p_s) /*@modifies stderr@*/ ; + +extern void +sRef_aliasSetComplete (void (p_predf) (sRef, fileloc), sRef p_s, fileloc p_loc) + /*@modifies p_s@*/ ; + +extern void +sRef_aliasSetCompleteParam (void (p_predf) (sRef, int, fileloc), sRef p_s, + int p_kind, fileloc p_loc) + /*@modifies p_s@*/ ; + +extern void +sRef_aliasSetCompleteAlkParam (void (p_predf) (sRef, alkind, fileloc), sRef p_s, + alkind p_kind, fileloc p_loc) + /*@modifies p_s@*/ ; + # else # error "Multiple include" # endif