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 /*@nullwhentrue@*/ bool sRef_isInvalid (sRef p_s) /*@*/ ;
extern /*@falsewhennull@*/ bool sRef_isValid (sRef p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool sRef_isReasonable (sRef p_s) /*@*/ ;
/*@constant null sRef sRef_undefined; @*/
# define sRef_undefined ((sRef) NULL)
extern bool sRef_isMeaningful (/*@sef@*/ sRef p_s) /*@*/ ;
# define sRef_isMeaningful(s) (sRef_isValid(s) && sRef_isKnown(s) \
&& (s)->kind != SK_NEW && (s)->kind != SK_TYPE)
+
+extern bool sRef_isSomewhatMeaningful (/*@sef@*/ sRef p_s) /*@*/ ;
+# define sRef_isSomewhatMeaningful(s) (sRef_isValid(s) && sRef_isKnown(s) \
+ && (s)->kind != SK_TYPE)
extern bool sRef_isNew (/*@sef@*/ sRef p_s) /*@*/ ;
# define sRef_isNew(s) (sRef_isValid(s) && (s)->kind == SK_NEW)
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_showNotReallyDefined (sRef p_s) /*@modifies g_warningstream@*/ ;
extern void sRef_enterFunctionScope (void) /*@modifies internalState@*/ ;
extern void sRef_setGlobalScope (void) /*@modifies internalState@*/ ;
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*/ ;
+extern void sRef_showExpInfo (sRef p_s) /*@modifies g_warningstream*/ ;
extern void sRef_setDefined (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
extern void sRef_setUndefined (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
extern void sRef_setOnly (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
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_showAliasInfo (sRef p_s) /*@modifies g_warningstream@*/ ;
+extern void sRef_showMetaStateInfo (sRef p_s, cstring p_key) /*@modifies g_warningstream@*/ ;
+extern void sRef_showNullInfo (sRef p_s) /*@modifies g_warningstream@*/ ;
+extern void sRef_showStateInfo (sRef p_s) /*@modifies g_warningstream@*/ ;
extern void sRef_setStateFromType (sRef p_s, ctype p_ct) /*@modifies p_s@*/ ;
extern void sRef_kill (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
extern void sRef_setAllocated (sRef p_s, fileloc p_loc) /*@modifies 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(/*@sef@*/sRef p_s);
/*drl7x 11/28/00*/
-extern bool sRef_isFixedArray (sRef p_s) /*@*/;
-
-extern long int sRef_getArraySize (sRef p_s) /*@*/;
+extern bool sRef_isFixedArray (sRef p_s) /*@*/;
+extern size_t sRef_getArraySize (sRef p_s) /*@*/;
extern /*@observer@*/ cstring sRef_ntMessage (sRef p_s);
extern void sRef_resetLen (sRef p_s) /*@modifies p_s@*/ ;
alkind p_kind, fileloc p_loc)
/*@modifies p_s@*/ ;
-
-
-
+# ifdef DEBUGSPLINT
+extern void sRef_checkCompletelyReasonable (sRef p_s) /*@modifies g_errorstream@*/ ;
+# endif
# else
# error "Multiple include"