[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 usymId 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 (usymId p_u1, usymId 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@*/ ;

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; \
      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 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 int uentry_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@/ ;
	153	extern usymId usymtab_getTypeId (cstring p_k) /@globals internalState@/ ;
	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
885824d3	180	extern bool usymtab_matchForwardStruct (usymId p_u1, usymId 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
	190	extern usymId usymId_fromInt (int p_i) /@/ ;
	191	# define usymId_fromInt(i) ((usymId)(i))
	192
	193	extern bool usymId_isInvalid (usymId p_u) /@/ ;
	194	# define usymId_isInvalid(u) ((u) == USYMIDINVALID)
	195
	196	extern bool usymId_isValid (usymId p_u) /@/ ;
	197	# define usymId_isValid(u) ((u) != USYMIDINVALID)
	198
	199	extern bool typeId_isInvalid (typeId p_u) /@/ ;
	200	# define typeId_isInvalid(u) ((u) == typeId_invalid)
	201
	202	extern bool typeId_isValid (typeId p_u) /@/ ;
	203	# define typeId_isValid(u) ((u) != typeId_invalid)
	204
	205	extern bool typeId_equal (typeId p_u1, typeId p_u2) /@/ ;
	206	# define typeId_equal(u1,u2) ((u1) == (u2))
	207
	208	extern typeId typeId_fromInt (int p_i);
	209	# define typeId_fromInt(i) ((typeId)(i))
	210
	211	/@iter usymtab_entries (sef usymtab u, yield exposed uentry el); @/
	212	# define usymtab_entries(x, m_i) \
	213	{ int m_ind; \
	214	if (usymtab_isDefined (x)) \
	215	for (m_ind = 0; m_ind < (x)->nentries; m_ind++) \
	216	{ uentry m_i = (x)->entries[m_ind];
	217
	218	# define end_usymtab_entries }}
	219
	220	extern /@unused@/ void usymtab_displayAllUses (void)
	221	/@globals internalState@/
80489f0a	222	/@modifies g_warningstream@*/ ;
885824d3	223
	224	extern /@unused@/ void usymtab_printOut (void)
	225	/@globals internalState@/
80489f0a	226	/@modifies g_warningstream@*/ ;
885824d3	227
	228	extern /@unused@/ void usymtab_printAll (void)
	229	/@globals internalState@/
80489f0a	230	/@modifies g_warningstream@*/ ;
885824d3	231
	232	extern void usymtab_enterScope (void)
	233	/@modifies internalState;@/ ;
	234	extern void usymtab_enterFunctionScope (uentry p_fcn)
	235	/@modifies internalState;@/ ;
	236	extern void usymtab_quietExitScope (fileloc p_loc)
	237	/@modifies internalState;@/ ;
	238	extern void usymtab_exitScope (exprNode p_expr) /@modifies internalState@/ ;
	239	extern void usymtab_addGuards (guardSet p_guards) /@modifies internalState@/ ;
	240	extern void usymtab_setExitCode (exitkind p_ex) /@modifies internalState@/ ;
	241	extern void usymtab_exitFile (void) /@modifies internalState@/ ;
	242	extern void usymtab_enterFile (void) /@modifies internalState@/ ;
	243
	244	extern /@observer@/ uentry usymtab_lookupEnumTag (cstring p_k)
	245	/@globals internalState@/ ;
	246
	247	extern usymId usymtab_convertId (usymId p_uid) /@globals internalState@/ ;
	248	extern void usymtab_initMod (void) /@modifies internalState@/ ;
6fcd0b1e	249	extern void usymtab_destroyMod (void) /@modifies internalState@/ ;
885824d3	250	extern void usymtab_initBool (void) /@modifies internalState@/ ;
28bf4b0b	251	extern void usymtab_initGlobalMarker (void) /@modifies internalState@/ ;
885824d3	252
	253	extern void usymtab_exportHeader (void)
	254	/@modifies internalState@/ ;
	255
	256	extern ctype usymtab_structFieldsType (uentryList p_f)
	257	/@globals internalState@/ ;
	258
	259	extern ctype usymtab_unionFieldsType (uentryList p_f)
	260	/@globals internalState@/ ;
	261
	262	extern ctype usymtab_enumEnumNameListType (enumNameList p_f)
	263	/@globals internalState@/ ;
	264
28bf4b0b	265	extern /@exposed@/ uentry usymtab_getTypeEntrySafe (typeId p_uid)
885824d3	266	/@globals internalState@/ ;
	267
	268	extern void usymtab_popOrBranch (exprNode p_pred, exprNode p_expr)
	269	/@modifies internalState@/ ;
	270	extern void usymtab_popAndBranch (exprNode p_pred, exprNode p_expr)
	271	/@modifies internalState@/ ;
	272
	273	extern void usymtab_trueBranch (/@only@/ guardSet p_guards)
	274	/@modifies internalState@/ ;
	275	extern void usymtab_altBranch (/@only@/ guardSet p_guards)
	276	/@modifies internalState@/ ;
	277
	278	extern void usymtab_popTrueBranch (exprNode p_pred, exprNode p_expr, clause p_cl)
	279	/@modifies internalState@/ ;
28bf4b0b	280
885824d3	281	extern void
	282	usymtab_popTrueExecBranch (exprNode p_pred, exprNode p_expr, clause p_cl)
	283	/@modifies internalState@/ ;
	284
	285	extern void
	286	usymtab_popBranches (exprNode p_pred, exprNode p_tbranch, exprNode p_fbranch,
	287	bool p_isOpt, clause p_cl)
	288	/@modifies internalState@/ ;
	289
	290	extern void usymtab_unguard (sRef p_s) /@modifies internalState@/ ;
	291	extern bool usymtab_isGuarded (sRef p_s) /@globals internalState@/ ;
80489f0a	292	extern void usymtab_printGuards (void) /@globals internalState@/ /@modifies g_warningstream@*/ ;
885824d3	293	extern void usymtab_quietPlainExitScope (void) /@modifies internalState@/ ;
	294	extern void usymtab_printComplete (void) /@globals internalState@/ /@modifies stdout@*/ ;
	295
885824d3	296	extern bool usymtab_existsGlobEither (cstring p_k) /@globals internalState@/ ;
885824d3	297
28bf4b0b	298	extern bool usymtab_isBoolType (typeId p_uid) /@globals internalState@/ ;
28bf4b0b	299	extern /@only@/ cstring usymtab_getTypeEntryName (typeId p_uid)
885824d3	300	/@globals internalState@/ ;
28bf4b0b	301	extern /@exposed@/ uentry usymtab_getTypeEntry (typeId p_uid)
885824d3	302	/@globals internalState@/ ;
885824d3	303
28bf4b0b	304	extern typeId
885824d3	305	usymtab_supAbstractTypeEntry (/@only@/ uentry p_e, bool p_dodef)
	306	/@modifies internalState, p_e@/ ;
	307	extern ctype usymtab_supForwardTypeEntry (/@only@/ uentry p_e)
	308	/@modifies internalState, p_e@/ ;
	309
	310	extern /@exposed@/ uentry
	311	usymtab_supGlobalEntryReturn (/@only@/ uentry p_e)
	312	/@modifies internalState, p_e@/ ;
	313
	314	extern /@exposed@/ uentry
	315	usymtab_supEntrySrefReturn (/@only@/ uentry p_e)
	316	/@modifies internalState, p_e@/ ;
	317
	318	extern int uentry_directParamNo (uentry p_ue)
	319	/@globals internalState@/ ;
	320
	321	extern bool usymtab_newCase (exprNode p_pred, exprNode p_last)
	322	/@modifies internalState@/ ;
	323
	324	extern void usymtab_switchBranch (exprNode p_s)
	325	/@modifies internalState@/ ;
	326
	327	extern /@only@/ cstring usymtab_unparseStack (void)
	328	/@globals internalState@/ ;
	329	extern void usymtab_exitSwitch (exprNode p_sw, bool p_allpaths)
	330	/@modifies internalState@/ ;
	331
	332	extern /@observer@/ uentry usymtab_lookupGlobSafe (cstring p_k)
	333	/@globals internalState@/ ;
	334
	335	extern /@only@/ sRefSet usymtab_aliasedBy (sRef p_s)
	336	/@globals internalState@/ ;
	337
	338	extern /@only@/ sRefSet usymtab_canAlias (sRef p_s)
	339	/@globals internalState@/ ;
	340
	341	extern void usymtab_clearAlias (sRef p_s)
	342	/@modifies internalState, p_s@/ ;
	343
28bf4b0b	344	extern void usymtab_addMustAlias (/@exposed@/ sRef p_s, /@exposed@/ sRef p_al)
885824d3	345	/@modifies internalState@/ ;
885824d3	346
28bf4b0b	347	extern void usymtab_addForceMustAlias (/@exposed@/ sRef p_s, /@exposed@/ sRef p_al)
885824d3	348	/@modifies internalState@/ ;
	349
	350	extern /@only@/ cstring usymtab_unparseAliases (void)
	351	/@globals internalState@/ ;
	352
	353	extern /@exposed@/ uentry
	354	usymtab_supReturnFileEntry (/@only@/ uentry p_e)
	355	/@modifies internalState@/ ;
	356
28bf4b0b	357	extern bool usymtab_isAltDefinitelyNullDeep (sRef p_s)
885824d3	358	/@globals internalState@/ ;
	359
	360	extern bool usymtab_existsReal (cstring p_k)
	361	/@globals internalState@/ ;
	362
	363	extern /@only@/ sRefSet usymtab_allAliases (sRef p_s)
	364	/@globals internalState@/ ;
	365
	366	extern void usymtab_exportLocal (void)
	367	/@modifies internalState@/ ;
	368
	369	extern void usymtab_popCaseBranch (void)
	370	/@modifies internalState@/ ;
	371
	372	/* special scopes */
	373
	374	/@constant int globScope;@/
	375	# define globScope 0 /* global variables */
	376
	377	/@constant int fileScope;@/
	378	# define fileScope 1 /* file-level static variables */
	379
	380	/@constant int paramsScope;@/
	381	# define paramsScope 2 /* function parameters */
	382
	383	/@constant int functionScope;@/
	384	# define functionScope 3
	385
0e41eb0e	386	extern /@falsewhennull@/ bool usymtab_isDefined (usymtab p_u) /@/ ;
885824d3	387
	388	/@constant null usymtab usymtab_undefined; @/
	389	# define usymtab_undefined ((usymtab)NULL)
	390	# define usymtab_isDefined(u) ((u) != usymtab_undefined)
	391
	392	extern void usymtab_checkDistinctName (uentry p_e, int p_scope)
	393	/@globals internalState@/
80489f0a	394	/@modifies g_warningstream, p_e@*/ ;
885824d3	395
28bf4b0b	396	extern /@exposed@/ sRef usymtab_lookupGlobalMarker (void) /@globals internalState@/ ;
393e573f	397	extern void usymtab_addReallyForceMustAlias (/@exposed@/ sRef p_s, /@exposed@/ sRef p_al) /@modifies internalState@/ ;
28bf4b0b	398	extern int usymtab_getCurrentDepth (void) /@globals internalState@/ ;
28bf4b0b	399
6483a926	400	# ifdef DEBUGSPLINT
	401	extern void usymtab_checkAllValid (void) /@modifies g_errorstream@/ ;
	402	# endif
	403
885824d3	404	# else
	405	# error "Multiple include"
	406	# endif
	407
	408
	409