[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_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
	131	extern /@observer@/ uentry usymtab_getGlobalEntry (usymId p_uid)
	132	/@globals internalState@/ ;
	133
	134	extern bool usymtab_exists (cstring p_k)
	135	/@globals internalState@/ ;
	136
885824d3	137	extern bool usymtab_existsVar (cstring p_k)
885824d3	138	/@globals internalState@/ ;
885824d3	139
	140	extern bool usymtab_existsGlob (cstring p_k)
	141	/@globals internalState@/ ;
	142
	143	extern bool usymtab_existsType (cstring p_k)
	144	/@globals internalState@/ ;
	145
885824d3	146	extern bool usymtab_existsEither (cstring p_k)
885824d3	147	/@globals internalState@/ ;
885824d3	148
	149	extern bool usymtab_existsTypeEither (cstring p_k)
	150	/@globals internalState@/ ;
	151
	152	extern usymId usymtab_getId (cstring p_k) /@globals internalState@/ ;
b73d1009	153	extern typeId usymtab_getTypeId (cstring p_k) /@globals internalState@/ ;
885824d3	154
	155	extern void usymtab_supEntry (/@only@/ uentry p_e)
	156	/@modifies internalState, p_e@/ ;
	157
885824d3	158	extern void usymtab_replaceEntry (/@only@/ uentry p_s)
885824d3	159	/@modifies internalState, p_s@/ ;
885824d3	160
	161	extern void usymtab_supEntrySref (/@only@/ uentry p_e)
	162	/@modifies internalState, p_e@/ ;
	163
	164	extern void usymtab_supGlobalEntry (/@only@/ uentry p_e)
	165	/@modifies internalState@/ ;
	166
	167	extern void usymtab_addGlobalEntry (/@only@/ uentry p_e)
	168	/@modifies internalState, p_e@/ ;
	169
	170	extern /@exposed@/ uentry
	171	usymtab_supEntryReturn (/@only@/ uentry p_e)
	172	/@modifies internalState, p_e@/ ;
	173
	174	extern usymId usymtab_addEntry (/@only@/ uentry p_e)
	175	/@modifies internalState, p_e@/ ;
	176
	177	extern ctype usymtab_lookupAbstractType (cstring p_k)
28bf4b0b	178	/@globals internalState@/ /@modifies nothing@/ ;
28bf4b0b	179
b73d1009	180	extern bool usymtab_matchForwardStruct (typeId p_u1, typeId p_u2)
28bf4b0b	181	/@globals internalState@/ ;
885824d3	182
	183	extern bool usymtab_existsEnumTag (cstring p_k)
	184	/@globals internalState@/ ;
	185	extern bool usymtab_existsUnionTag (cstring p_k)
	186	/@globals internalState@/ ;
	187	extern bool usymtab_existsStructTag (cstring p_k)
	188	/@globals internalState@/ ;
	189
885824d3	190	/@iter usymtab_entries (sef usymtab u, yield exposed uentry el); @/
	191	# define usymtab_entries(x, m_i) \
	192	{ int m_ind; \
	193	if (usymtab_isDefined (x)) \
	194	for (m_ind = 0; m_ind < (x)->nentries; m_ind++) \
	195	{ uentry m_i = (x)->entries[m_ind];
	196
	197	# define end_usymtab_entries }}
	198
	199	extern /@unused@/ void usymtab_displayAllUses (void)
	200	/@globals internalState@/
80489f0a	201	/@modifies g_warningstream@*/ ;
885824d3	202
	203	extern /@unused@/ void usymtab_printOut (void)
	204	/@globals internalState@/
80489f0a	205	/@modifies g_warningstream@*/ ;
885824d3	206
	207	extern /@unused@/ void usymtab_printAll (void)
	208	/@globals internalState@/
80489f0a	209	/@modifies g_warningstream@*/ ;
885824d3	210
	211	extern void usymtab_enterScope (void)
	212	/@modifies internalState;@/ ;
	213	extern void usymtab_enterFunctionScope (uentry p_fcn)
	214	/@modifies internalState;@/ ;
	215	extern void usymtab_quietExitScope (fileloc p_loc)
	216	/@modifies internalState;@/ ;
	217	extern void usymtab_exitScope (exprNode p_expr) /@modifies internalState@/ ;
	218	extern void usymtab_addGuards (guardSet p_guards) /@modifies internalState@/ ;
	219	extern void usymtab_setExitCode (exitkind p_ex) /@modifies internalState@/ ;
	220	extern void usymtab_exitFile (void) /@modifies internalState@/ ;
	221	extern void usymtab_enterFile (void) /@modifies internalState@/ ;
	222
	223	extern /@observer@/ uentry usymtab_lookupEnumTag (cstring p_k)
	224	/@globals internalState@/ ;
	225
	226	extern usymId usymtab_convertId (usymId p_uid) /@globals internalState@/ ;
b73d1009	227	extern typeId usymtab_convertTypeId (typeId p_uid) /@globals internalState@/ ;
885824d3	228	extern void usymtab_initMod (void) /@modifies internalState@/ ;
6fcd0b1e	229	extern void usymtab_destroyMod (void) /@modifies internalState@/ ;
885824d3	230	extern void usymtab_initBool (void) /@modifies internalState@/ ;
28bf4b0b	231	extern void usymtab_initGlobalMarker (void) /@modifies internalState@/ ;
885824d3	232
	233	extern void usymtab_exportHeader (void)
	234	/@modifies internalState@/ ;
	235
	236	extern ctype usymtab_structFieldsType (uentryList p_f)
	237	/@globals internalState@/ ;
	238
	239	extern ctype usymtab_unionFieldsType (uentryList p_f)
	240	/@globals internalState@/ ;
	241
	242	extern ctype usymtab_enumEnumNameListType (enumNameList p_f)
	243	/@globals internalState@/ ;
	244
28bf4b0b	245	extern /@exposed@/ uentry usymtab_getTypeEntrySafe (typeId p_uid)
885824d3	246	/@globals internalState@/ ;
	247
	248	extern void usymtab_popOrBranch (exprNode p_pred, exprNode p_expr)
	249	/@modifies internalState@/ ;
	250	extern void usymtab_popAndBranch (exprNode p_pred, exprNode p_expr)
	251	/@modifies internalState@/ ;
	252
	253	extern void usymtab_trueBranch (/@only@/ guardSet p_guards)
	254	/@modifies internalState@/ ;
	255	extern void usymtab_altBranch (/@only@/ guardSet p_guards)
	256	/@modifies internalState@/ ;
	257
	258	extern void usymtab_popTrueBranch (exprNode p_pred, exprNode p_expr, clause p_cl)
	259	/@modifies internalState@/ ;
28bf4b0b	260
885824d3	261	extern void
	262	usymtab_popTrueExecBranch (exprNode p_pred, exprNode p_expr, clause p_cl)
	263	/@modifies internalState@/ ;
	264
	265	extern void
	266	usymtab_popBranches (exprNode p_pred, exprNode p_tbranch, exprNode p_fbranch,
	267	bool p_isOpt, clause p_cl)
	268	/@modifies internalState@/ ;
	269
	270	extern void usymtab_unguard (sRef p_s) /@modifies internalState@/ ;
	271	extern bool usymtab_isGuarded (sRef p_s) /@globals internalState@/ ;
80489f0a	272	extern void usymtab_printGuards (void) /@globals internalState@/ /@modifies g_warningstream@*/ ;
885824d3	273	extern void usymtab_quietPlainExitScope (void) /@modifies internalState@/ ;
	274	extern void usymtab_printComplete (void) /@globals internalState@/ /@modifies stdout@*/ ;
	275
885824d3	276	extern bool usymtab_existsGlobEither (cstring p_k) /@globals internalState@/ ;
885824d3	277
28bf4b0b	278	extern bool usymtab_isBoolType (typeId p_uid) /@globals internalState@/ ;
28bf4b0b	279	extern /@only@/ cstring usymtab_getTypeEntryName (typeId p_uid)
885824d3	280	/@globals internalState@/ ;
28bf4b0b	281	extern /@exposed@/ uentry usymtab_getTypeEntry (typeId p_uid)
885824d3	282	/@globals internalState@/ ;
885824d3	283
28bf4b0b	284	extern typeId
885824d3	285	usymtab_supAbstractTypeEntry (/@only@/ uentry p_e, bool p_dodef)
	286	/@modifies internalState, p_e@/ ;
	287	extern ctype usymtab_supForwardTypeEntry (/@only@/ uentry p_e)
	288	/@modifies internalState, p_e@/ ;
	289
	290	extern /@exposed@/ uentry
	291	usymtab_supGlobalEntryReturn (/@only@/ uentry p_e)
	292	/@modifies internalState, p_e@/ ;
	293
	294	extern /@exposed@/ uentry
	295	usymtab_supEntrySrefReturn (/@only@/ uentry p_e)
	296	/@modifies internalState, p_e@/ ;
	297
b73d1009	298	extern usymId usymtab_directParamNo (uentry p_ue)
885824d3	299	/@globals internalState@/ ;
	300
	301	extern bool usymtab_newCase (exprNode p_pred, exprNode p_last)
	302	/@modifies internalState@/ ;
	303
	304	extern void usymtab_switchBranch (exprNode p_s)
	305	/@modifies internalState@/ ;
	306
	307	extern /@only@/ cstring usymtab_unparseStack (void)
	308	/@globals internalState@/ ;
	309	extern void usymtab_exitSwitch (exprNode p_sw, bool p_allpaths)
	310	/@modifies internalState@/ ;
	311
	312	extern /@observer@/ uentry usymtab_lookupGlobSafe (cstring p_k)
	313	/@globals internalState@/ ;
	314
	315	extern /@only@/ sRefSet usymtab_aliasedBy (sRef p_s)
	316	/@globals internalState@/ ;
	317
	318	extern /@only@/ sRefSet usymtab_canAlias (sRef p_s)
	319	/@globals internalState@/ ;
	320
	321	extern void usymtab_clearAlias (sRef p_s)
	322	/@modifies internalState, p_s@/ ;
	323
28bf4b0b	324	extern void usymtab_addMustAlias (/@exposed@/ sRef p_s, /@exposed@/ sRef p_al)
885824d3	325	/@modifies internalState@/ ;
885824d3	326
28bf4b0b	327	extern void usymtab_addForceMustAlias (/@exposed@/ sRef p_s, /@exposed@/ sRef p_al)
885824d3	328	/@modifies internalState@/ ;
	329
	330	extern /@only@/ cstring usymtab_unparseAliases (void)
	331	/@globals internalState@/ ;
	332
	333	extern /@exposed@/ uentry
	334	usymtab_supReturnFileEntry (/@only@/ uentry p_e)
	335	/@modifies internalState@/ ;
	336
28bf4b0b	337	extern bool usymtab_isAltDefinitelyNullDeep (sRef p_s)
885824d3	338	/@globals internalState@/ ;
	339
	340	extern bool usymtab_existsReal (cstring p_k)
	341	/@globals internalState@/ ;
	342
	343	extern /@only@/ sRefSet usymtab_allAliases (sRef p_s)
	344	/@globals internalState@/ ;
	345
	346	extern void usymtab_exportLocal (void)
	347	/@modifies internalState@/ ;
	348
	349	extern void usymtab_popCaseBranch (void)
	350	/@modifies internalState@/ ;
	351
	352	/* special scopes */
	353
	354	/@constant int globScope;@/
	355	# define globScope 0 /* global variables */
	356
	357	/@constant int fileScope;@/
	358	# define fileScope 1 /* file-level static variables */
	359
	360	/@constant int paramsScope;@/
	361	# define paramsScope 2 /* function parameters */
	362
	363	/@constant int functionScope;@/
	364	# define functionScope 3
	365
0e41eb0e	366	extern /@falsewhennull@/ bool usymtab_isDefined (usymtab p_u) /@/ ;
885824d3	367
	368	/@constant null usymtab usymtab_undefined; @/
	369	# define usymtab_undefined ((usymtab)NULL)
	370	# define usymtab_isDefined(u) ((u) != usymtab_undefined)
	371
	372	extern void usymtab_checkDistinctName (uentry p_e, int p_scope)
	373	/@globals internalState@/
80489f0a	374	/@modifies g_warningstream, p_e@*/ ;
885824d3	375
28bf4b0b	376	extern /@exposed@/ sRef usymtab_lookupGlobalMarker (void) /@globals internalState@/ ;
393e573f	377	extern void usymtab_addReallyForceMustAlias (/@exposed@/ sRef p_s, /@exposed@/ sRef p_al) /@modifies internalState@/ ;
28bf4b0b	378	extern int usymtab_getCurrentDepth (void) /@globals internalState@/ ;
28bf4b0b	379
6483a926	380	# ifdef DEBUGSPLINT
	381	extern void usymtab_checkAllValid (void) /@modifies g_errorstream@/ ;
	382	# endif
	383
885824d3	384	# else
	385	# error "Multiple include"
	386	# endif
	387
	388
	389