/*
-** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2000.
+** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2003.
** See ../LICENSE for license information.
*/
/*
# ifndef USYMTAB_H
# define USYMTAB_H
-#include "environmentTable.h"
/*@constant null usymtab GLOBAL_ENV; @*/
# define GLOBAL_ENV usymtab_undefined
US_CBRANCH, US_SWITCH
} uskind;
-typedef struct _refentry { int level; int index; } *refentry;
+typedef struct { int level; int index; } *refentry;
typedef /*@only@*/ refentry o_refentry;
typedef o_refentry *refTable;
-struct _usymtab
+struct s_usymtab
{
uskind kind;
int nentries;
bool mustBreak;
exitkind exitCode;
/*@reldef@*/ /*@only@*/ o_uentry *entries;
- /*@null@*/ /*@only@*/ hashTable htable; /* for the global environment */
+ /*@null@*/ /*@only@*/ cstringTable htable; /* for the global environment */
/*@null@*/ /*@only@*/ refTable reftable; /* for branched environments */
/*@only@*/ guardSet guards; /* guarded references (not null) */
aliasTable aliases;
/*@owned@*/ usymtab env;
- environmentTable environment;
} ;
/*
extern void usymtab_printTypes (void)
/*@globals internalState@*/
- /*@modifies g_msgstream@*/ ;
+ /*@modifies g_warningstream@*/ ;
extern void usymtab_setMustBreak (void) /*@modifies internalState@*/ ;
extern bool usymtab_inFileScope (void) /*@globals internalState@*/ ;
extern void usymtab_checkFinalScope (bool p_isReturn)
/*@globals internalState@*/
- /*@modifies *g_msgstream@*/ ;
+ /*@modifies *g_warningstream@*/ ;
extern void usymtab_allUsed (void)
/*@globals internalState@*/
- /*@modifies *g_msgstream@*/ ;
+ /*@modifies *g_warningstream@*/ ;
extern void usymtab_allDefined (void)
/*@globals internalState@*/
- /*@modifies *g_msgstream@*/ ;
+ /*@modifies *g_warningstream@*/ ;
extern void usymtab_prepareDump (void)
/*@modifies internalState@*/ ;
extern /*@exposed@*/ uentry usymtab_lookupExpose (cstring p_k)
/*@globals internalState@*/ ;
+
extern /*@observer@*/ uentry usymtab_lookup (cstring p_k)
/*@globals internalState@*/ ;
+
# define usymtab_lookup(s) (usymtab_lookupExpose (s))
extern /*@observer@*/ uentry usymtab_lookupGlob (cstring p_k)
extern /*@observer@*/ uentry usymtab_lookupEither (cstring p_k)
/*@globals internalState@*/ ;
-# ifndef NOLCL
extern ctype usymtab_lookupType (cstring p_k)
/*@globals internalState@*/ ;
-# endif
-extern bool usymtab_isProbableNull (sRef p_s)
+extern bool usymtab_isDefinitelyNull (sRef p_s)
/*@globals internalState@*/ ;
-extern bool usymtab_isProbableDeepNull (sRef p_s)
+extern bool usymtab_isDefinitelyNullDeep (sRef p_s)
/*@globals internalState@*/ ;
-# ifndef NOLCL
extern usymId usymtab_supExposedTypeEntry (/*@only@*/ uentry p_e, bool p_dodef)
/*@modifies internalState, p_e@*/ ;
-# endif
extern ctype usymtab_supTypeEntry (/*@only@*/ uentry p_e)
/*@modifies internalState, p_e@*/ ;
extern bool usymtab_exists (cstring p_k)
/*@globals internalState@*/ ;
-# ifndef NOLCL
extern bool usymtab_existsVar (cstring p_k)
/*@globals internalState@*/ ;
-# endif
extern bool usymtab_existsGlob (cstring p_k)
/*@globals internalState@*/ ;
extern bool usymtab_existsType (cstring p_k)
/*@globals internalState@*/ ;
-# ifndef NOLCL
extern bool usymtab_existsEither (cstring p_k)
/*@globals internalState@*/ ;
-# endif
extern bool usymtab_existsTypeEither (cstring p_k)
/*@globals internalState@*/ ;
extern usymId usymtab_getId (cstring p_k) /*@globals internalState@*/ ;
-extern usymId usymtab_getTypeId (cstring p_k) /*@globals internalState@*/ ;
+extern typeId usymtab_getTypeId (cstring p_k) /*@globals internalState@*/ ;
extern void usymtab_supEntry (/*@only@*/ uentry p_e)
/*@modifies internalState, p_e@*/ ;
-# ifndef NOLCL
extern void usymtab_replaceEntry (/*@only@*/ uentry p_s)
/*@modifies internalState, p_s@*/ ;
-# endif
extern void usymtab_supEntrySref (/*@only@*/ uentry p_e)
/*@modifies internalState, p_e@*/ ;
/*@modifies internalState, p_e@*/ ;
extern ctype usymtab_lookupAbstractType (cstring p_k)
- /*@globals internalState@*/ ;
-extern bool usymtab_matchForwardStruct (usymId p_u1, usymId p_u2)
- /*@globals internalState@*/ ;
+ /*@globals internalState@*/ /*@modifies nothing@*/ ;
+
+extern bool usymtab_matchForwardStruct (typeId p_u1, typeId p_u2)
+ /*@globals internalState@*/ ;
extern bool usymtab_existsEnumTag (cstring p_k)
/*@globals internalState@*/ ;
extern bool usymtab_existsStructTag (cstring p_k)
/*@globals internalState@*/ ;
-extern usymId usymId_fromInt (int p_i) /*@*/ ;
-# define usymId_fromInt(i) ((usymId)(i))
-
-extern bool usymId_isInvalid (usymId p_u) /*@*/ ;
-# define usymId_isInvalid(u) ((u) == USYMIDINVALID)
-
-extern bool usymId_isValid (usymId p_u) /*@*/ ;
-# define usymId_isValid(u) ((u) != USYMIDINVALID)
-
-extern bool typeId_isInvalid (typeId p_u) /*@*/ ;
-# define typeId_isInvalid(u) ((u) == typeId_invalid)
-
-extern bool typeId_isValid (typeId p_u) /*@*/ ;
-# define typeId_isValid(u) ((u) != typeId_invalid)
-
-extern bool typeId_equal (typeId p_u1, typeId p_u2) /*@*/ ;
-# define typeId_equal(u1,u2) ((u1) == (u2))
-
-extern typeId typeId_fromInt (int p_i);
-# define typeId_fromInt(i) ((typeId)(i))
-
/*@iter usymtab_entries (sef usymtab u, yield exposed uentry el); @*/
# define usymtab_entries(x, m_i) \
{ int m_ind; \
extern /*@unused@*/ void usymtab_displayAllUses (void)
/*@globals internalState@*/
- /*@modifies *g_msgstream@*/ ;
+ /*@modifies *g_warningstream@*/ ;
extern /*@unused@*/ void usymtab_printOut (void)
/*@globals internalState@*/
- /*@modifies *g_msgstream@*/ ;
+ /*@modifies *g_warningstream@*/ ;
extern /*@unused@*/ void usymtab_printAll (void)
/*@globals internalState@*/
- /*@modifies *g_msgstream@*/ ;
+ /*@modifies *g_warningstream@*/ ;
extern void usymtab_enterScope (void)
/*@modifies internalState;@*/ ;
/*@globals internalState@*/ ;
extern usymId usymtab_convertId (usymId p_uid) /*@globals internalState@*/ ;
+extern typeId usymtab_convertTypeId (typeId p_uid) /*@globals internalState@*/ ;
extern void usymtab_initMod (void) /*@modifies internalState@*/ ;
+extern void usymtab_destroyMod (void) /*@modifies internalState@*/ ;
extern void usymtab_initBool (void) /*@modifies internalState@*/ ;
+extern void usymtab_initGlobalMarker (void) /*@modifies internalState@*/ ;
extern void usymtab_exportHeader (void)
/*@modifies internalState@*/ ;
extern ctype usymtab_enumEnumNameListType (enumNameList p_f)
/*@globals internalState@*/ ;
-extern /*@exposed@*/ uentry usymtab_getTypeEntrySafe (usymId p_uid)
+extern /*@exposed@*/ uentry usymtab_getTypeEntrySafe (typeId p_uid)
/*@globals internalState@*/ ;
extern void usymtab_popOrBranch (exprNode p_pred, exprNode p_expr)
extern void usymtab_popTrueBranch (exprNode p_pred, exprNode p_expr, clause p_cl)
/*@modifies internalState@*/ ;
+
extern void
usymtab_popTrueExecBranch (exprNode p_pred, exprNode p_expr, clause p_cl)
/*@modifies internalState@*/ ;
extern void usymtab_unguard (sRef p_s) /*@modifies internalState@*/ ;
extern bool usymtab_isGuarded (sRef p_s) /*@globals internalState@*/ ;
-extern void usymtab_printGuards (void) /*@globals internalState@*/ /*@modifies *g_msgstream@*/ ;
+extern void usymtab_printGuards (void) /*@globals internalState@*/ /*@modifies *g_warningstream@*/ ;
extern void usymtab_quietPlainExitScope (void) /*@modifies internalState@*/ ;
extern void usymtab_printComplete (void) /*@globals internalState@*/ /*@modifies *stdout@*/ ;
-# ifndef NOLCL
extern bool usymtab_existsGlobEither (cstring p_k) /*@globals internalState@*/ ;
-# endif
-extern bool usymtab_isBoolType (usymId p_uid) /*@globals internalState@*/ ;
-extern /*@only@*/ cstring
- usymtab_getTypeEntryName (usymId p_uid)
+extern bool usymtab_isBoolType (typeId p_uid) /*@globals internalState@*/ ;
+extern /*@only@*/ cstring usymtab_getTypeEntryName (typeId p_uid)
/*@globals internalState@*/ ;
-extern /*@exposed@*/ uentry usymtab_getTypeEntry (usymId p_uid)
+extern /*@exposed@*/ uentry usymtab_getTypeEntry (typeId p_uid)
/*@globals internalState@*/ ;
-extern usymId
+extern typeId
usymtab_supAbstractTypeEntry (/*@only@*/ uentry p_e, bool p_dodef)
/*@modifies internalState, p_e@*/ ;
extern ctype usymtab_supForwardTypeEntry (/*@only@*/ uentry p_e)
usymtab_supEntrySrefReturn (/*@only@*/ uentry p_e)
/*@modifies internalState, p_e@*/ ;
-extern int uentry_directParamNo (uentry p_ue)
+extern usymId usymtab_directParamNo (uentry p_ue)
/*@globals internalState@*/ ;
extern bool usymtab_newCase (exprNode p_pred, exprNode p_last)
extern void usymtab_clearAlias (sRef p_s)
/*@modifies internalState, p_s@*/ ;
-extern void usymtab_addMustAlias (sRef p_s, sRef p_al)
+extern void usymtab_addMustAlias (/*@exposed@*/ sRef p_s, /*@exposed@*/ sRef p_al)
/*@modifies internalState@*/ ;
-extern void usymtab_addForceMustAlias (sRef p_s, sRef p_al)
+extern void usymtab_addForceMustAlias (/*@exposed@*/ sRef p_s, /*@exposed@*/ sRef p_al)
/*@modifies internalState@*/ ;
extern /*@only@*/ cstring usymtab_unparseAliases (void)
usymtab_supReturnFileEntry (/*@only@*/ uentry p_e)
/*@modifies internalState@*/ ;
-extern bool usymtab_isAltProbablyDeepNull (sRef p_s)
+extern bool usymtab_isAltDefinitelyNullDeep (sRef p_s)
/*@globals internalState@*/ ;
extern bool usymtab_existsReal (cstring p_k)
/*@constant int functionScope;@*/
# define functionScope 3
-extern /*@falsenull@*/ bool usymtab_isDefined (usymtab p_u) /*@*/ ;
+extern /*@falsewhennull@*/ bool usymtab_isDefined (usymtab p_u) /*@*/ ;
/*@constant null usymtab usymtab_undefined; @*/
# define usymtab_undefined ((usymtab)NULL)
extern void usymtab_checkDistinctName (uentry p_e, int p_scope)
/*@globals internalState@*/
- /*@modifies *g_msgstream, p_e@*/ ;
+ /*@modifies *g_warningstream, p_e@*/ ;
+extern /*@exposed@*/ sRef usymtab_lookupGlobalMarker (void) /*@globals internalState@*/ ;
+extern void usymtab_addReallyForceMustAlias (/*@exposed@*/ sRef p_s, /*@exposed@*/ sRef p_al) /*@modifies internalState@*/ ;
+extern int usymtab_getCurrentDepth (void) /*@globals internalState@*/ ;
- /*DRL add 9/4/00 */
-extern void usymtab_testInRange (sRef p_s, int p_index) /*@modifies internalState;@*/;
-extern void usymtab_postopVar (sRef p_sr) /*@modifies internalState;@*/ ;
-
+# ifdef DEBUGSPLINT
+extern void usymtab_checkAllValid (void) /*@modifies g_errorstream@*/ ;
+# endif
# else
# error "Multiple include"