[splint.git] / src / Headers / usymtab-branch.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 s_usentry
{
  /*@only@*/ uentry entry;
  bool istrace;

  /* 
  ** Trace entries have a level and index that identify the original entry. 
  ** Not used for normal entries.
  */

  int level; 
  int index; 
} usentry;

struct _usymtab
{
  uskind   kind;
  int      nentries;
  int      nspace;
  int      lexlevel;
  bool     mustBreak;
  exitkind exitCode;
  /*@reldef@*/ /*@only@*/ usentry *entries;
  
  /* Optional.  Used for the global environment to speed lookups. */
  /*@null@*/ /*@only@*/ cstringTable htable;   

  /* Guarded references - these references are not null along this path. */
  /*@i32 This seems unnecessary - the trace entries should cover it...? */
  /*@only@*/ guardSet guards;   

  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_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 (usymId 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 (usymId p_uid) /*@globals internalState@*/ ;
extern /*@only@*/ cstring 
  usymtab_getTypeEntryName (usymId p_uid)
  /*@globals internalState@*/ ;
extern /*@exposed@*/ uentry usymtab_getTypeEntry (usymId p_uid)
  /*@globals internalState@*/ ;

extern usymId 
  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 invalidScope;@*/
# define invalidScope -1  /* invalid scope */

/*@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 int usymtab_getCurrentDepth (void) /*@globals internalState@*/ ;

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