[splint.git] / src / Headers / usymtab.h

/*
** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2003.
** See ../LICENSE for license information.
*/
/*
** usymtab.h
*/

# ifndef USYMTAB_H
# define USYMTAB_H

/*@constant null usymtab GLOBAL_ENV; @*/ 
# define GLOBAL_ENV usymtab_undefined

typedef enum { 
  US_GLOBAL, 
  US_NORMAL, 
  US_TBRANCH, US_FBRANCH, 
  US_CBRANCH, US_SWITCH
} uskind;

typedef struct { int level; int index; } *refentry;
typedef /*@only@*/ refentry o_refentry;
typedef o_refentry *refTable;

struct s_usymtab
{
  uskind   kind;
  int      nentries;
  int      nspace;
  int      lexlevel;
  bool     mustBreak;
  exitkind exitCode;
  /*@reldef@*/ /*@only@*/ o_uentry  *entries;
  /*@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;
} ; 

/*
** rep invariant:
**
** (left as exercise to reader)  ;) 
*/

extern void usymtab_printTypes (void) 
  /*@globals internalState@*/
  /*@modifies g_warningstream@*/ ;

extern void usymtab_setMustBreak (void) /*@modifies internalState@*/ ;

extern bool usymtab_inGlobalScope (void) /*@globals internalState@*/ ;
extern bool usymtab_inFunctionScope (void) /*@globals internalState@*/ ;
extern bool usymtab_inFileScope (void) /*@globals internalState@*/ ;
extern void usymtab_checkFinalScope (bool p_isReturn) 
  /*@globals internalState@*/ 
  /*@modifies *g_warningstream@*/ ;

extern void usymtab_allUsed (void)
   /*@globals internalState@*/ 
   /*@modifies *g_warningstream@*/ ;

extern void usymtab_allDefined (void)
   /*@globals internalState@*/
   /*@modifies *g_warningstream@*/ ;

extern void usymtab_prepareDump (void)
   /*@modifies internalState@*/ ;

extern void usymtab_dump (FILE *p_fout)
   /*@globals internalState@*/
   /*@modifies *p_fout@*/ ;


extern void usymtab_load (FILE *p_f) /*@modifies p_f, internalState@*/ ;

extern /*@exposed@*/ /*@dependent@*/ uentry 
  usymtab_getRefQuiet (int p_level, usymId p_index)
  /*@globals internalState@*/ ;

extern void usymtab_printLocal (void) 
  /*@globals internalState@*/ 
  /*@modifies stdout@*/ ;

extern /*@exposed@*/ /*@dependent@*/ uentry usymtab_getParam (int p_paramno)
   /*@globals internalState@*/;
extern void usymtab_free (void) /*@modifies internalState@*/ ;
extern bool usymtab_inDeepScope (void) /*@globals 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)
   /*@globals internalState@*/ ;
extern /*@exposed@*/ uentry usymtab_lookupExposeGlob (cstring p_k)
   /*@globals internalState@*/ ;
extern /*@observer@*/ uentry usymtab_lookupUnionTag (cstring p_k)
   /*@globals internalState@*/ ;
extern /*@observer@*/ uentry usymtab_lookupStructTag (cstring p_k)
   /*@globals internalState@*/ ;
extern /*@observer@*/ uentry usymtab_lookupEither (cstring p_k)
   /*@globals internalState@*/ ;

extern ctype usymtab_lookupType (cstring p_k)
   /*@globals internalState@*/ ;

extern bool usymtab_isDefinitelyNull (sRef p_s)
   /*@globals internalState@*/ ;
extern bool usymtab_isDefinitelyNullDeep (sRef p_s)
   /*@globals internalState@*/ ;

extern usymId usymtab_supExposedTypeEntry (/*@only@*/ uentry p_e, bool p_dodef)
   /*@modifies internalState, p_e@*/ ;

extern ctype usymtab_supTypeEntry (/*@only@*/ uentry p_e)
   /*@modifies internalState, p_e@*/ ;

extern /*@exposed@*/ uentry usymtab_supReturnTypeEntry (/*@only@*/ uentry p_e)
   /*@modifies internalState@*/ ;

extern /*@observer@*/ uentry usymtab_lookupSafe (cstring p_k)
   /*@globals internalState@*/ ;

extern /*@observer@*/ uentry
  usymtab_lookupSafeScope (cstring p_k, int p_lexlevel)
     /*@globals internalState@*/ ;

extern /*@observer@*/ uentry usymtab_getGlobalEntry (usymId p_uid)
  /*@globals internalState@*/ ;

extern bool usymtab_exists (cstring p_k)
   /*@globals internalState@*/ ;

extern bool usymtab_existsVar (cstring p_k)
   /*@globals internalState@*/ ;

extern bool usymtab_existsGlob (cstring p_k)
   /*@globals internalState@*/ ;

extern bool usymtab_existsType (cstring p_k)
   /*@globals internalState@*/ ;

extern bool usymtab_existsEither (cstring p_k)
   /*@globals internalState@*/ ;

extern bool usymtab_existsTypeEither (cstring p_k)
   /*@globals internalState@*/ ;

extern usymId usymtab_getId (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@*/ ;

extern void usymtab_replaceEntry (/*@only@*/ uentry p_s)
  /*@modifies internalState, p_s@*/ ;

extern void usymtab_supEntrySref (/*@only@*/ uentry p_e)
  /*@modifies internalState, p_e@*/ ;

extern void usymtab_supGlobalEntry (/*@only@*/ uentry p_e)
  /*@modifies internalState@*/ ;

extern void usymtab_addGlobalEntry (/*@only@*/ uentry p_e) 
  /*@modifies internalState, p_e@*/ ;

extern /*@exposed@*/ uentry 
  usymtab_supEntryReturn (/*@only@*/ uentry p_e)
  /*@modifies internalState, p_e@*/ ;

extern usymId usymtab_addEntry (/*@only@*/ uentry p_e)
  /*@modifies internalState, p_e@*/ ;

extern ctype usymtab_lookupAbstractType (cstring p_k) 
     /*@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_existsUnionTag (cstring p_k) 
  /*@globals internalState@*/ ;
extern bool usymtab_existsStructTag (cstring p_k) 
  /*@globals internalState@*/ ;

/*@iter usymtab_entries (sef usymtab u, yield exposed uentry el); @*/
# define usymtab_entries(x, m_i)   \
    { int m_ind; \
      if (usymtab_isDefined (x)) \
        for (m_ind = 0; m_ind < (x)->nentries; m_ind++) \
	   { uentry m_i = (x)->entries[m_ind]; 

# define end_usymtab_entries }}

extern /*@unused@*/ void usymtab_displayAllUses (void)
   /*@globals internalState@*/ 
   /*@modifies *g_warningstream@*/ ;

extern /*@unused@*/ void usymtab_printOut (void)
   /*@globals internalState@*/ 
   /*@modifies *g_warningstream@*/ ;

extern /*@unused@*/ void usymtab_printAll (void)
   /*@globals internalState@*/ 
   /*@modifies *g_warningstream@*/ ;

extern void usymtab_enterScope (void) 
  /*@modifies internalState;@*/ ;
extern void usymtab_enterFunctionScope (uentry p_fcn) 
  /*@modifies internalState;@*/ ;
extern void usymtab_quietExitScope (fileloc p_loc)
  /*@modifies internalState;@*/ ;
extern void usymtab_exitScope (exprNode p_expr) /*@modifies internalState@*/ ;
extern void usymtab_addGuards (guardSet p_guards) /*@modifies internalState@*/ ;
extern void usymtab_setExitCode (exitkind p_ex) /*@modifies internalState@*/ ;
extern void usymtab_exitFile (void) /*@modifies internalState@*/ ;
extern void usymtab_enterFile (void) /*@modifies internalState@*/ ;

extern /*@observer@*/ uentry usymtab_lookupEnumTag (cstring p_k)
  /*@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_structFieldsType (uentryList p_f)
   /*@globals internalState@*/ ;

extern ctype usymtab_unionFieldsType (uentryList p_f)
   /*@globals internalState@*/ ;

extern ctype usymtab_enumEnumNameListType (enumNameList p_f)
   /*@globals internalState@*/ ;

extern /*@exposed@*/ uentry usymtab_getTypeEntrySafe (typeId p_uid)
   /*@globals internalState@*/ ;

extern void usymtab_popOrBranch (exprNode p_pred, exprNode p_expr)
  /*@modifies internalState@*/ ;
extern void usymtab_popAndBranch (exprNode p_pred, exprNode p_expr)
  /*@modifies internalState@*/ ;

extern void usymtab_trueBranch (/*@only@*/ guardSet p_guards)
  /*@modifies internalState@*/ ;
extern void usymtab_altBranch (/*@only@*/ guardSet p_guards)
  /*@modifies internalState@*/ ;

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_popBranches (exprNode p_pred, exprNode p_tbranch, exprNode p_fbranch, 
		       bool p_isOpt, 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_warningstream@*/ ;
extern void usymtab_quietPlainExitScope (void) /*@modifies internalState@*/ ;
extern void usymtab_printComplete (void) /*@globals internalState@*/ /*@modifies *stdout@*/ ;

extern bool usymtab_existsGlobEither (cstring p_k) /*@globals internalState@*/ ;

extern bool usymtab_isBoolType (typeId p_uid) /*@globals internalState@*/ ;
extern /*@only@*/ cstring usymtab_getTypeEntryName (typeId p_uid)
  /*@globals internalState@*/ ;
extern /*@exposed@*/ uentry usymtab_getTypeEntry (typeId p_uid)
  /*@globals internalState@*/ ;

extern typeId
  usymtab_supAbstractTypeEntry (/*@only@*/ uentry p_e, bool p_dodef)
  /*@modifies internalState, p_e@*/ ;
extern ctype usymtab_supForwardTypeEntry (/*@only@*/ uentry p_e)
  /*@modifies internalState, p_e@*/ ;

extern /*@exposed@*/ uentry 
  usymtab_supGlobalEntryReturn (/*@only@*/ uentry p_e)
  /*@modifies internalState, p_e@*/ ;

extern /*@exposed@*/ uentry 
  usymtab_supEntrySrefReturn (/*@only@*/ uentry p_e)
  /*@modifies internalState, p_e@*/ ;

extern usymId usymtab_directParamNo (uentry p_ue)
  /*@globals internalState@*/ ;

extern bool usymtab_newCase (exprNode p_pred, exprNode p_last)
  /*@modifies internalState@*/ ;

extern void usymtab_switchBranch (exprNode p_s) 
  /*@modifies internalState@*/ ;

extern /*@only@*/ cstring usymtab_unparseStack (void)
  /*@globals internalState@*/ ;
extern void usymtab_exitSwitch (exprNode p_sw, bool p_allpaths)
  /*@modifies internalState@*/ ;

extern /*@observer@*/ uentry usymtab_lookupGlobSafe (cstring p_k)
  /*@globals internalState@*/ ;

extern /*@only@*/ sRefSet usymtab_aliasedBy (sRef p_s)
  /*@globals internalState@*/ ;

extern /*@only@*/ sRefSet usymtab_canAlias (sRef p_s)
  /*@globals internalState@*/ ;

extern void usymtab_clearAlias (sRef p_s)
  /*@modifies internalState, p_s@*/ ;

extern void usymtab_addMustAlias (/*@exposed@*/ sRef p_s, /*@exposed@*/ sRef p_al)
  /*@modifies internalState@*/ ;

extern void usymtab_addForceMustAlias (/*@exposed@*/ sRef p_s, /*@exposed@*/ sRef p_al)
  /*@modifies internalState@*/ ;

extern /*@only@*/ cstring usymtab_unparseAliases (void)
  /*@globals internalState@*/ ;

extern /*@exposed@*/ uentry
  usymtab_supReturnFileEntry (/*@only@*/ uentry p_e)
   /*@modifies internalState@*/ ;

extern bool usymtab_isAltDefinitelyNullDeep (sRef p_s)
   /*@globals internalState@*/ ;

extern bool usymtab_existsReal (cstring p_k)
   /*@globals internalState@*/ ;

extern /*@only@*/ sRefSet usymtab_allAliases (sRef p_s)
   /*@globals internalState@*/ ;

extern void usymtab_exportLocal (void)
   /*@modifies internalState@*/ ;

extern void usymtab_popCaseBranch (void)
     /*@modifies internalState@*/ ;

/* special scopes */

/*@constant int globScope;@*/
# define globScope 0  /* global variables */

/*@constant int fileScope;@*/
# define fileScope   1  /* file-level static variables */

/*@constant int paramsScope;@*/
# define paramsScope 2  /* function parameters */

/*@constant int functionScope;@*/
# define functionScope 3

extern /*@falsewhennull@*/ bool usymtab_isDefined (usymtab p_u) /*@*/ ;

/*@constant null usymtab usymtab_undefined; @*/
# define usymtab_undefined ((usymtab)NULL)
# define usymtab_isDefined(u) ((u) != usymtab_undefined)

extern void usymtab_checkDistinctName (uentry p_e, int p_scope)
  /*@globals internalState@*/
  /*@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@*/ ;

# ifdef DEBUGSPLINT
extern void usymtab_checkAllValid (void) /*@modifies g_errorstream@*/ ; 
# endif

# else
# error "Multiple include"
# endif
Commit	Line	Data
885824d3	1	/*
c0de361f	2	** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2003.
885824d3	3	** See ../LICENSE for license information.
	4	*/
	5	/*
	6	** usymtab.h
	7	*/
	8
	9	# ifndef USYMTAB_H
	10	# define USYMTAB_H
	11
	12	/@constant null usymtab GLOBAL_ENV; @/
	13	# define GLOBAL_ENV usymtab_undefined
	14
	15	typedef enum {
	16	US_GLOBAL,
	17	US_NORMAL,
	18	US_TBRANCH, US_FBRANCH,
	19	US_CBRANCH, US_SWITCH
	20	} uskind;
	21
28bf4b0b	22	typedef struct { int level; int index; } *refentry;
885824d3	23	typedef /@only@/ refentry o_refentry;
	24	typedef o_refentry *refTable;
	25
28bf4b0b	26	struct s_usymtab
885824d3	27	{
	28	uskind kind;
	29	int nentries;
	30	int nspace;
	31	int lexlevel;
	32	bool mustBreak;
	33	exitkind exitCode;
	34	/@reldef@/ /@only@/ o_uentry *entries;
28bf4b0b	35	/@null@/ /@only@/ cstringTable htable; /* for the global environment */
885824d3	36	/@null@/ /@only@/ refTable reftable; /* for branched environments */
	37	/@only@/ guardSet guards; /* guarded references (not null) */
	38	aliasTable aliases;
	39	/@owned@/ usymtab env;
	40	} ;
	41
	42	/*
	43	** rep invariant:
	44	**
	45	** (left as exercise to reader) ;)
	46	*/
	47
	48	extern void usymtab_printTypes (void)
	49	/@globals internalState@/
80489f0a	50	/@modifies g_warningstream@/ ;
885824d3	51
	52	extern void usymtab_setMustBreak (void) /@modifies internalState@/ ;
	53
	54	extern bool usymtab_inGlobalScope (void) /@globals internalState@/ ;
	55	extern bool usymtab_inFunctionScope (void) /@globals internalState@/ ;
	56	extern bool usymtab_inFileScope (void) /@globals internalState@/ ;
	57	extern void usymtab_checkFinalScope (bool p_isReturn)
	58	/@globals internalState@/
80489f0a	59	/@modifies g_warningstream@*/ ;
885824d3	60
	61	extern void usymtab_allUsed (void)
	62	/@globals internalState@/
80489f0a	63	/@modifies g_warningstream@*/ ;
885824d3	64
	65	extern void usymtab_allDefined (void)
	66	/@globals internalState@/
80489f0a	67	/@modifies g_warningstream@*/ ;
885824d3	68
	69	extern void usymtab_prepareDump (void)
	70	/@modifies internalState@/ ;
	71
	72	extern void usymtab_dump (FILE *p_fout)
	73	/@globals internalState@/
	74	/@modifies p_fout@*/ ;
	75
	76
	77	extern void usymtab_load (FILE p_f) /@modifies p_f, internalState@*/ ;
	78
	79	extern /@exposed@/ /@dependent@/ uentry
	80	usymtab_getRefQuiet (int p_level, usymId p_index)
	81	/@globals internalState@/ ;
	82
	83	extern void usymtab_printLocal (void)
	84	/@globals internalState@/
	85	/@modifies stdout@/ ;
	86
	87	extern /@exposed@/ /@dependent@/ uentry usymtab_getParam (int p_paramno)
	88	/@globals internalState@/;
	89	extern void usymtab_free (void) /@modifies internalState@/ ;
	90	extern bool usymtab_inDeepScope (void) /@globals internalState@/ ;
	91
	92	extern /@exposed@/ uentry usymtab_lookupExpose (cstring p_k)
	93	/@globals internalState@/ ;
28bf4b0b	94
885824d3	95	extern /@observer@/ uentry usymtab_lookup (cstring p_k)
885824d3	96	/@globals internalState@/ ;
28bf4b0b	97
885824d3	98	# define usymtab_lookup(s) (usymtab_lookupExpose (s))
	99
	100	extern /@observer@/ uentry usymtab_lookupGlob (cstring p_k)
	101	/@globals internalState@/ ;
	102	extern /@exposed@/ uentry usymtab_lookupExposeGlob (cstring p_k)
	103	/@globals internalState@/ ;
	104	extern /@observer@/ uentry usymtab_lookupUnionTag (cstring p_k)
	105	/@globals internalState@/ ;
	106	extern /@observer@/ uentry usymtab_lookupStructTag (cstring p_k)
	107	/@globals internalState@/ ;
	108	extern /@observer@/ uentry usymtab_lookupEither (cstring p_k)
	109	/@globals internalState@/ ;
	110
885824d3	111	extern ctype usymtab_lookupType (cstring p_k)
885824d3	112	/@globals internalState@/ ;
885824d3	113
28bf4b0b	114	extern bool usymtab_isDefinitelyNull (sRef p_s)
885824d3	115	/@globals internalState@/ ;
28bf4b0b	116	extern bool usymtab_isDefinitelyNullDeep (sRef p_s)
885824d3	117	/@globals internalState@/ ;
885824d3	118
885824d3	119	extern usymId usymtab_supExposedTypeEntry (/@only@/ uentry p_e, bool p_dodef)
885824d3	120	/@modifies internalState, p_e@/ ;
885824d3	121
	122	extern ctype usymtab_supTypeEntry (/@only@/ uentry p_e)
	123	/@modifies internalState, p_e@/ ;
	124
	125	extern /@exposed@/ uentry usymtab_supReturnTypeEntry (/@only@/ uentry p_e)
	126	/@modifies internalState@/ ;
	127
	128	extern /@observer@/ uentry usymtab_lookupSafe (cstring p_k)
	129	/@globals internalState@/ ;
	130
909cf5eb	131	extern /@observer@/ uentry
	132	usymtab_lookupSafeScope (cstring p_k, int p_lexlevel)
	133	/@globals internalState@/ ;
	134
885824d3	135	extern /@observer@/ uentry usymtab_getGlobalEntry (usymId p_uid)
	136	/@globals internalState@/ ;
	137
	138	extern bool usymtab_exists (cstring p_k)
	139	/@globals internalState@/ ;
	140
885824d3	141	extern bool usymtab_existsVar (cstring p_k)
885824d3	142	/@globals internalState@/ ;
885824d3	143
	144	extern bool usymtab_existsGlob (cstring p_k)
	145	/@globals internalState@/ ;
	146
	147	extern bool usymtab_existsType (cstring p_k)
	148	/@globals internalState@/ ;
	149
885824d3	150	extern bool usymtab_existsEither (cstring p_k)
885824d3	151	/@globals internalState@/ ;
885824d3	152
	153	extern bool usymtab_existsTypeEither (cstring p_k)
	154	/@globals internalState@/ ;
	155
	156	extern usymId usymtab_getId (cstring p_k) /@globals internalState@/ ;
b73d1009	157	extern typeId usymtab_getTypeId (cstring p_k) /@globals internalState@/ ;
885824d3	158
	159	extern void usymtab_supEntry (/@only@/ uentry p_e)
	160	/@modifies internalState, p_e@/ ;
	161
885824d3	162	extern void usymtab_replaceEntry (/@only@/ uentry p_s)
885824d3	163	/@modifies internalState, p_s@/ ;
885824d3	164
	165	extern void usymtab_supEntrySref (/@only@/ uentry p_e)
	166	/@modifies internalState, p_e@/ ;
	167
	168	extern void usymtab_supGlobalEntry (/@only@/ uentry p_e)
	169	/@modifies internalState@/ ;
	170
	171	extern void usymtab_addGlobalEntry (/@only@/ uentry p_e)
	172	/@modifies internalState, p_e@/ ;
	173
	174	extern /@exposed@/ uentry
	175	usymtab_supEntryReturn (/@only@/ uentry p_e)
	176	/@modifies internalState, p_e@/ ;
	177
	178	extern usymId usymtab_addEntry (/@only@/ uentry p_e)
	179	/@modifies internalState, p_e@/ ;
	180
	181	extern ctype usymtab_lookupAbstractType (cstring p_k)
28bf4b0b	182	/@globals internalState@/ /@modifies nothing@/ ;
28bf4b0b	183
b73d1009	184	extern bool usymtab_matchForwardStruct (typeId p_u1, typeId p_u2)
28bf4b0b	185	/@globals internalState@/ ;
885824d3	186
	187	extern bool usymtab_existsEnumTag (cstring p_k)
	188	/@globals internalState@/ ;
	189	extern bool usymtab_existsUnionTag (cstring p_k)
	190	/@globals internalState@/ ;
	191	extern bool usymtab_existsStructTag (cstring p_k)
	192	/@globals internalState@/ ;
	193
885824d3	194	/@iter usymtab_entries (sef usymtab u, yield exposed uentry el); @/
	195	# define usymtab_entries(x, m_i) \
	196	{ int m_ind; \
	197	if (usymtab_isDefined (x)) \
	198	for (m_ind = 0; m_ind < (x)->nentries; m_ind++) \
	199	{ uentry m_i = (x)->entries[m_ind];
	200
	201	# define end_usymtab_entries }}
	202
	203	extern /@unused@/ void usymtab_displayAllUses (void)
	204	/@globals internalState@/
80489f0a	205	/@modifies g_warningstream@*/ ;
885824d3	206
	207	extern /@unused@/ void usymtab_printOut (void)
	208	/@globals internalState@/
80489f0a	209	/@modifies g_warningstream@*/ ;
885824d3	210
	211	extern /@unused@/ void usymtab_printAll (void)
	212	/@globals internalState@/
80489f0a	213	/@modifies g_warningstream@*/ ;
885824d3	214
	215	extern void usymtab_enterScope (void)
	216	/@modifies internalState;@/ ;
	217	extern void usymtab_enterFunctionScope (uentry p_fcn)
	218	/@modifies internalState;@/ ;
	219	extern void usymtab_quietExitScope (fileloc p_loc)
	220	/@modifies internalState;@/ ;
	221	extern void usymtab_exitScope (exprNode p_expr) /@modifies internalState@/ ;
	222	extern void usymtab_addGuards (guardSet p_guards) /@modifies internalState@/ ;
	223	extern void usymtab_setExitCode (exitkind p_ex) /@modifies internalState@/ ;
	224	extern void usymtab_exitFile (void) /@modifies internalState@/ ;
	225	extern void usymtab_enterFile (void) /@modifies internalState@/ ;
	226
	227	extern /@observer@/ uentry usymtab_lookupEnumTag (cstring p_k)
	228	/@globals internalState@/ ;
	229
	230	extern usymId usymtab_convertId (usymId p_uid) /@globals internalState@/ ;
b73d1009	231	extern typeId usymtab_convertTypeId (typeId p_uid) /@globals internalState@/ ;
885824d3	232	extern void usymtab_initMod (void) /@modifies internalState@/ ;
6fcd0b1e	233	extern void usymtab_destroyMod (void) /@modifies internalState@/ ;
885824d3	234	extern void usymtab_initBool (void) /@modifies internalState@/ ;
28bf4b0b	235	extern void usymtab_initGlobalMarker (void) /@modifies internalState@/ ;
885824d3	236
	237	extern void usymtab_exportHeader (void)
	238	/@modifies internalState@/ ;
	239
	240	extern ctype usymtab_structFieldsType (uentryList p_f)
	241	/@globals internalState@/ ;
	242
	243	extern ctype usymtab_unionFieldsType (uentryList p_f)
	244	/@globals internalState@/ ;
	245
	246	extern ctype usymtab_enumEnumNameListType (enumNameList p_f)
	247	/@globals internalState@/ ;
	248
28bf4b0b	249	extern /@exposed@/ uentry usymtab_getTypeEntrySafe (typeId p_uid)
885824d3	250	/@globals internalState@/ ;
	251
	252	extern void usymtab_popOrBranch (exprNode p_pred, exprNode p_expr)
	253	/@modifies internalState@/ ;
	254	extern void usymtab_popAndBranch (exprNode p_pred, exprNode p_expr)
	255	/@modifies internalState@/ ;
	256
	257	extern void usymtab_trueBranch (/@only@/ guardSet p_guards)
	258	/@modifies internalState@/ ;
	259	extern void usymtab_altBranch (/@only@/ guardSet p_guards)
	260	/@modifies internalState@/ ;
	261
	262	extern void usymtab_popTrueBranch (exprNode p_pred, exprNode p_expr, clause p_cl)
	263	/@modifies internalState@/ ;
28bf4b0b	264
885824d3	265	extern void
	266	usymtab_popTrueExecBranch (exprNode p_pred, exprNode p_expr, clause p_cl)
	267	/@modifies internalState@/ ;
	268
	269	extern void
	270	usymtab_popBranches (exprNode p_pred, exprNode p_tbranch, exprNode p_fbranch,
	271	bool p_isOpt, clause p_cl)
	272	/@modifies internalState@/ ;
	273
	274	extern void usymtab_unguard (sRef p_s) /@modifies internalState@/ ;
	275	extern bool usymtab_isGuarded (sRef p_s) /@globals internalState@/ ;
80489f0a	276	extern void usymtab_printGuards (void) /@globals internalState@/ /@modifies g_warningstream@*/ ;
885824d3	277	extern void usymtab_quietPlainExitScope (void) /@modifies internalState@/ ;
	278	extern void usymtab_printComplete (void) /@globals internalState@/ /@modifies stdout@*/ ;
	279
885824d3	280	extern bool usymtab_existsGlobEither (cstring p_k) /@globals internalState@/ ;
885824d3	281
28bf4b0b	282	extern bool usymtab_isBoolType (typeId p_uid) /@globals internalState@/ ;
28bf4b0b	283	extern /@only@/ cstring usymtab_getTypeEntryName (typeId p_uid)
885824d3	284	/@globals internalState@/ ;
28bf4b0b	285	extern /@exposed@/ uentry usymtab_getTypeEntry (typeId p_uid)
885824d3	286	/@globals internalState@/ ;
885824d3	287
28bf4b0b	288	extern typeId
885824d3	289	usymtab_supAbstractTypeEntry (/@only@/ uentry p_e, bool p_dodef)
	290	/@modifies internalState, p_e@/ ;
	291	extern ctype usymtab_supForwardTypeEntry (/@only@/ uentry p_e)
	292	/@modifies internalState, p_e@/ ;
	293
	294	extern /@exposed@/ uentry
	295	usymtab_supGlobalEntryReturn (/@only@/ uentry p_e)
	296	/@modifies internalState, p_e@/ ;
	297
	298	extern /@exposed@/ uentry
	299	usymtab_supEntrySrefReturn (/@only@/ uentry p_e)
	300	/@modifies internalState, p_e@/ ;
	301
b73d1009	302	extern usymId usymtab_directParamNo (uentry p_ue)
885824d3	303	/@globals internalState@/ ;
	304
	305	extern bool usymtab_newCase (exprNode p_pred, exprNode p_last)
	306	/@modifies internalState@/ ;
	307
	308	extern void usymtab_switchBranch (exprNode p_s)
	309	/@modifies internalState@/ ;
	310
	311	extern /@only@/ cstring usymtab_unparseStack (void)
	312	/@globals internalState@/ ;
	313	extern void usymtab_exitSwitch (exprNode p_sw, bool p_allpaths)
	314	/@modifies internalState@/ ;
	315
	316	extern /@observer@/ uentry usymtab_lookupGlobSafe (cstring p_k)
	317	/@globals internalState@/ ;
	318
	319	extern /@only@/ sRefSet usymtab_aliasedBy (sRef p_s)
	320	/@globals internalState@/ ;
	321
	322	extern /@only@/ sRefSet usymtab_canAlias (sRef p_s)
	323	/@globals internalState@/ ;
	324
	325	extern void usymtab_clearAlias (sRef p_s)
	326	/@modifies internalState, p_s@/ ;
	327
28bf4b0b	328	extern void usymtab_addMustAlias (/@exposed@/ sRef p_s, /@exposed@/ sRef p_al)
885824d3	329	/@modifies internalState@/ ;
885824d3	330
28bf4b0b	331	extern void usymtab_addForceMustAlias (/@exposed@/ sRef p_s, /@exposed@/ sRef p_al)
885824d3	332	/@modifies internalState@/ ;
	333
	334	extern /@only@/ cstring usymtab_unparseAliases (void)
	335	/@globals internalState@/ ;
	336
	337	extern /@exposed@/ uentry
	338	usymtab_supReturnFileEntry (/@only@/ uentry p_e)
	339	/@modifies internalState@/ ;
	340
28bf4b0b	341	extern bool usymtab_isAltDefinitelyNullDeep (sRef p_s)
885824d3	342	/@globals internalState@/ ;
	343
	344	extern bool usymtab_existsReal (cstring p_k)
	345	/@globals internalState@/ ;
	346
	347	extern /@only@/ sRefSet usymtab_allAliases (sRef p_s)
	348	/@globals internalState@/ ;
	349
	350	extern void usymtab_exportLocal (void)
	351	/@modifies internalState@/ ;
	352
	353	extern void usymtab_popCaseBranch (void)
	354	/@modifies internalState@/ ;
	355
	356	/* special scopes */
	357
	358	/@constant int globScope;@/
	359	# define globScope 0 /* global variables */
	360
	361	/@constant int fileScope;@/
	362	# define fileScope 1 /* file-level static variables */
	363
	364	/@constant int paramsScope;@/
	365	# define paramsScope 2 /* function parameters */
	366
	367	/@constant int functionScope;@/
	368	# define functionScope 3
	369
0e41eb0e	370	extern /@falsewhennull@/ bool usymtab_isDefined (usymtab p_u) /@/ ;
885824d3	371
	372	/@constant null usymtab usymtab_undefined; @/
	373	# define usymtab_undefined ((usymtab)NULL)
	374	# define usymtab_isDefined(u) ((u) != usymtab_undefined)
	375
	376	extern void usymtab_checkDistinctName (uentry p_e, int p_scope)
	377	/@globals internalState@/
80489f0a	378	/@modifies g_warningstream, p_e@*/ ;
885824d3	379
28bf4b0b	380	extern /@exposed@/ sRef usymtab_lookupGlobalMarker (void) /@globals internalState@/ ;
393e573f	381	extern void usymtab_addReallyForceMustAlias (/@exposed@/ sRef p_s, /@exposed@/ sRef p_al) /@modifies internalState@/ ;
28bf4b0b	382	extern int usymtab_getCurrentDepth (void) /@globals internalState@/ ;
28bf4b0b	383
6483a926	384	# ifdef DEBUGSPLINT
	385	extern void usymtab_checkAllValid (void) /@modifies g_errorstream@/ ;
	386	# endif
	387
885824d3	388	# else
	389	# error "Multiple include"
	390	# endif
	391
	392
	393