2 ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2001.
3 ** See ../LICENSE for license information.
12 /*@constant null usymtab GLOBAL_ENV; @*/
13 # define GLOBAL_ENV usymtab_undefined
18 US_TBRANCH, US_FBRANCH,
22 typedef struct s_usentry
24 /*@only@*/ uentry entry;
28 ** Trace entries have a level and index that identify the original entry.
29 ** Not used for normal entries.
44 /*@reldef@*/ /*@only@*/ usentry *entries;
46 /* Optional. Used for the global environment to speed lookups. */
47 /*@null@*/ /*@only@*/ cstringTable htable;
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;
55 /*@owned@*/ usymtab env;
61 ** (left as exercise to reader) ;)
64 extern void usymtab_printTypes (void)
65 /*@globals internalState@*/
66 /*@modifies g_msgstream@*/ ;
68 extern void usymtab_setMustBreak (void) /*@modifies internalState@*/ ;
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@*/
75 /*@modifies *g_msgstream@*/ ;
77 extern void usymtab_allUsed (void)
78 /*@globals internalState@*/
79 /*@modifies *g_msgstream@*/ ;
81 extern void usymtab_allDefined (void)
82 /*@globals internalState@*/
83 /*@modifies *g_msgstream@*/ ;
85 extern void usymtab_prepareDump (void)
86 /*@modifies internalState@*/ ;
88 extern void usymtab_dump (FILE *p_fout)
89 /*@globals internalState@*/
90 /*@modifies *p_fout@*/ ;
93 extern void usymtab_load (FILE *p_f) /*@modifies p_f, internalState@*/ ;
95 extern /*@exposed@*/ /*@dependent@*/ uentry
96 usymtab_getRefQuiet (int p_level, usymId p_index)
97 /*@globals internalState@*/ ;
99 extern void usymtab_printLocal (void)
100 /*@globals internalState@*/
101 /*@modifies stdout@*/ ;
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@*/ ;
108 extern /*@exposed@*/ uentry usymtab_lookupExpose (cstring p_k)
109 /*@globals internalState@*/ ;
111 extern /*@observer@*/ uentry usymtab_lookup (cstring p_k)
112 /*@globals internalState@*/ ;
114 # define usymtab_lookup(s) (usymtab_lookupExpose (s))
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@*/ ;
128 extern ctype usymtab_lookupType (cstring p_k)
129 /*@globals internalState@*/ ;
132 extern bool usymtab_isDefinitelyNull (sRef p_s)
133 /*@globals internalState@*/ ;
134 extern bool usymtab_isDefinitelyNullDeep (sRef p_s)
135 /*@globals internalState@*/ ;
138 extern usymId usymtab_supExposedTypeEntry (/*@only@*/ uentry p_e, bool p_dodef)
139 /*@modifies internalState, p_e@*/ ;
142 extern ctype usymtab_supTypeEntry (/*@only@*/ uentry p_e)
143 /*@modifies internalState, p_e@*/ ;
145 extern /*@exposed@*/ uentry usymtab_supReturnTypeEntry (/*@only@*/ uentry p_e)
146 /*@modifies internalState@*/ ;
148 extern /*@observer@*/ uentry usymtab_lookupSafe (cstring p_k)
149 /*@globals internalState@*/ ;
151 extern /*@observer@*/ uentry usymtab_getGlobalEntry (usymId p_uid)
152 /*@globals internalState@*/ ;
154 extern bool usymtab_exists (cstring p_k)
155 /*@globals internalState@*/ ;
158 extern bool usymtab_existsVar (cstring p_k)
159 /*@globals internalState@*/ ;
162 extern bool usymtab_existsGlob (cstring p_k)
163 /*@globals internalState@*/ ;
165 extern bool usymtab_existsType (cstring p_k)
166 /*@globals internalState@*/ ;
169 extern bool usymtab_existsEither (cstring p_k)
170 /*@globals internalState@*/ ;
173 extern bool usymtab_existsTypeEither (cstring p_k)
174 /*@globals internalState@*/ ;
176 extern usymId usymtab_getId (cstring p_k) /*@globals internalState@*/ ;
177 extern usymId usymtab_getTypeId (cstring p_k) /*@globals internalState@*/ ;
179 extern void usymtab_supEntry (/*@only@*/ uentry p_e)
180 /*@modifies internalState, p_e@*/ ;
183 extern void usymtab_replaceEntry (/*@only@*/ uentry p_s)
184 /*@modifies internalState, p_s@*/ ;
187 extern void usymtab_supEntrySref (/*@only@*/ uentry p_e)
188 /*@modifies internalState, p_e@*/ ;
190 extern void usymtab_supGlobalEntry (/*@only@*/ uentry p_e)
191 /*@modifies internalState@*/ ;
193 extern void usymtab_addGlobalEntry (/*@only@*/ uentry p_e)
194 /*@modifies internalState, p_e@*/ ;
196 extern /*@exposed@*/ uentry
197 usymtab_supEntryReturn (/*@only@*/ uentry p_e)
198 /*@modifies internalState, p_e@*/ ;
200 extern usymId usymtab_addEntry (/*@only@*/ uentry p_e)
201 /*@modifies internalState, p_e@*/ ;
203 extern ctype usymtab_lookupAbstractType (cstring p_k)
204 /*@globals internalState@*/ /*@modifies nothing@*/ ;
206 extern bool usymtab_matchForwardStruct (usymId p_u1, usymId p_u2)
207 /*@globals internalState@*/ ;
209 extern bool usymtab_existsEnumTag (cstring p_k)
210 /*@globals internalState@*/ ;
211 extern bool usymtab_existsUnionTag (cstring p_k)
212 /*@globals internalState@*/ ;
213 extern bool usymtab_existsStructTag (cstring p_k)
214 /*@globals internalState@*/ ;
216 extern usymId usymId_fromInt (int p_i) /*@*/ ;
217 # define usymId_fromInt(i) ((usymId)(i))
219 extern bool usymId_isInvalid (usymId p_u) /*@*/ ;
220 # define usymId_isInvalid(u) ((u) == USYMIDINVALID)
222 extern bool usymId_isValid (usymId p_u) /*@*/ ;
223 # define usymId_isValid(u) ((u) != USYMIDINVALID)
225 extern bool typeId_isInvalid (typeId p_u) /*@*/ ;
226 # define typeId_isInvalid(u) ((u) == typeId_invalid)
228 extern bool typeId_isValid (typeId p_u) /*@*/ ;
229 # define typeId_isValid(u) ((u) != typeId_invalid)
231 extern bool typeId_equal (typeId p_u1, typeId p_u2) /*@*/ ;
232 # define typeId_equal(u1,u2) ((u1) == (u2))
234 extern typeId typeId_fromInt (int p_i);
235 # define typeId_fromInt(i) ((typeId)(i))
237 /*@iter usymtab_entries (sef usymtab u, yield exposed uentry el); @*/
238 # define usymtab_entries(x, m_i) \
240 if (usymtab_isDefined (x)) \
241 for (m_ind = 0; m_ind < (x)->nentries; m_ind++) \
242 { uentry m_i = (x)->entries[m_ind];
244 # define end_usymtab_entries }}
246 extern /*@unused@*/ void usymtab_displayAllUses (void)
247 /*@globals internalState@*/
248 /*@modifies *g_msgstream@*/ ;
250 extern /*@unused@*/ void usymtab_printOut (void)
251 /*@globals internalState@*/
252 /*@modifies *g_msgstream@*/ ;
254 extern /*@unused@*/ void usymtab_printAll (void)
255 /*@globals internalState@*/
256 /*@modifies *g_msgstream@*/ ;
258 extern void usymtab_enterScope (void)
259 /*@modifies internalState;@*/ ;
260 extern void usymtab_enterFunctionScope (uentry p_fcn)
261 /*@modifies internalState;@*/ ;
262 extern void usymtab_quietExitScope (fileloc p_loc)
263 /*@modifies internalState;@*/ ;
264 extern void usymtab_exitScope (exprNode p_expr) /*@modifies internalState@*/ ;
265 extern void usymtab_addGuards (guardSet p_guards) /*@modifies internalState@*/ ;
266 extern void usymtab_setExitCode (exitkind p_ex) /*@modifies internalState@*/ ;
267 extern void usymtab_exitFile (void) /*@modifies internalState@*/ ;
268 extern void usymtab_enterFile (void) /*@modifies internalState@*/ ;
270 extern /*@observer@*/ uentry usymtab_lookupEnumTag (cstring p_k)
271 /*@globals internalState@*/ ;
273 extern usymId usymtab_convertId (usymId p_uid) /*@globals internalState@*/ ;
274 extern void usymtab_initMod (void) /*@modifies internalState@*/ ;
275 extern void usymtab_initBool (void) /*@modifies internalState@*/ ;
276 extern void usymtab_initGlobalMarker (void) /*@modifies internalState@*/ ;
278 extern void usymtab_exportHeader (void)
279 /*@modifies internalState@*/ ;
281 extern ctype usymtab_structFieldsType (uentryList p_f)
282 /*@globals internalState@*/ ;
284 extern ctype usymtab_unionFieldsType (uentryList p_f)
285 /*@globals internalState@*/ ;
287 extern ctype usymtab_enumEnumNameListType (enumNameList p_f)
288 /*@globals internalState@*/ ;
290 extern /*@exposed@*/ uentry usymtab_getTypeEntrySafe (usymId p_uid)
291 /*@globals internalState@*/ ;
293 extern void usymtab_popOrBranch (exprNode p_pred, exprNode p_expr)
294 /*@modifies internalState@*/ ;
295 extern void usymtab_popAndBranch (exprNode p_pred, exprNode p_expr)
296 /*@modifies internalState@*/ ;
298 extern void usymtab_trueBranch (/*@only@*/ guardSet p_guards)
299 /*@modifies internalState@*/ ;
300 extern void usymtab_altBranch (/*@only@*/ guardSet p_guards)
301 /*@modifies internalState@*/ ;
303 extern void usymtab_popTrueBranch (exprNode p_pred, exprNode p_expr, clause p_cl)
304 /*@modifies internalState@*/ ;
307 usymtab_popTrueExecBranch (exprNode p_pred, exprNode p_expr, clause p_cl)
308 /*@modifies internalState@*/ ;
311 usymtab_popBranches (exprNode p_pred, exprNode p_tbranch, exprNode p_fbranch,
312 bool p_isOpt, clause p_cl)
313 /*@modifies internalState@*/ ;
315 extern void usymtab_unguard (sRef p_s) /*@modifies internalState@*/ ;
316 extern bool usymtab_isGuarded (sRef p_s) /*@globals internalState@*/ ;
317 extern void usymtab_printGuards (void) /*@globals internalState@*/ /*@modifies *g_msgstream@*/ ;
318 extern void usymtab_quietPlainExitScope (void) /*@modifies internalState@*/ ;
319 extern void usymtab_printComplete (void) /*@globals internalState@*/ /*@modifies *stdout@*/ ;
322 extern bool usymtab_existsGlobEither (cstring p_k) /*@globals internalState@*/ ;
325 extern bool usymtab_isBoolType (usymId p_uid) /*@globals internalState@*/ ;
326 extern /*@only@*/ cstring
327 usymtab_getTypeEntryName (usymId p_uid)
328 /*@globals internalState@*/ ;
329 extern /*@exposed@*/ uentry usymtab_getTypeEntry (usymId p_uid)
330 /*@globals internalState@*/ ;
333 usymtab_supAbstractTypeEntry (/*@only@*/ uentry p_e, bool p_dodef)
334 /*@modifies internalState, p_e@*/ ;
335 extern ctype usymtab_supForwardTypeEntry (/*@only@*/ uentry p_e)
336 /*@modifies internalState, p_e@*/ ;
338 extern /*@exposed@*/ uentry
339 usymtab_supGlobalEntryReturn (/*@only@*/ uentry p_e)
340 /*@modifies internalState, p_e@*/ ;
342 extern /*@exposed@*/ uentry
343 usymtab_supEntrySrefReturn (/*@only@*/ uentry p_e)
344 /*@modifies internalState, p_e@*/ ;
346 extern int uentry_directParamNo (uentry p_ue)
347 /*@globals internalState@*/ ;
349 extern bool usymtab_newCase (exprNode p_pred, exprNode p_last)
350 /*@modifies internalState@*/ ;
352 extern void usymtab_switchBranch (exprNode p_s)
353 /*@modifies internalState@*/ ;
355 extern /*@only@*/ cstring usymtab_unparseStack (void)
356 /*@globals internalState@*/ ;
357 extern void usymtab_exitSwitch (exprNode p_sw, bool p_allpaths)
358 /*@modifies internalState@*/ ;
360 extern /*@observer@*/ uentry usymtab_lookupGlobSafe (cstring p_k)
361 /*@globals internalState@*/ ;
363 extern /*@only@*/ sRefSet usymtab_aliasedBy (sRef p_s)
364 /*@globals internalState@*/ ;
366 extern /*@only@*/ sRefSet usymtab_canAlias (sRef p_s)
367 /*@globals internalState@*/ ;
369 extern void usymtab_clearAlias (sRef p_s)
370 /*@modifies internalState, p_s@*/ ;
372 extern void usymtab_addMustAlias (/*@exposed@*/ sRef p_s, /*@exposed@*/ sRef p_al)
373 /*@modifies internalState@*/ ;
375 extern void usymtab_addForceMustAlias (/*@exposed@*/ sRef p_s, /*@exposed@*/ sRef p_al)
376 /*@modifies internalState@*/ ;
378 extern /*@only@*/ cstring usymtab_unparseAliases (void)
379 /*@globals internalState@*/ ;
381 extern /*@exposed@*/ uentry
382 usymtab_supReturnFileEntry (/*@only@*/ uentry p_e)
383 /*@modifies internalState@*/ ;
385 extern bool usymtab_isAltDefinitelyNullDeep (sRef p_s)
386 /*@globals internalState@*/ ;
388 extern bool usymtab_existsReal (cstring p_k)
389 /*@globals internalState@*/ ;
391 extern /*@only@*/ sRefSet usymtab_allAliases (sRef p_s)
392 /*@globals internalState@*/ ;
394 extern void usymtab_exportLocal (void)
395 /*@modifies internalState@*/ ;
397 extern void usymtab_popCaseBranch (void)
398 /*@modifies internalState@*/ ;
402 /*@constant int invalidScope;@*/
403 # define invalidScope -1 /* invalid scope */
405 /*@constant int globScope;@*/
406 # define globScope 0 /* global variables */
408 /*@constant int fileScope;@*/
409 # define fileScope 1 /* file-level static variables */
411 /*@constant int paramsScope;@*/
412 # define paramsScope 2 /* function parameters */
414 /*@constant int functionScope;@*/
415 # define functionScope 3
417 extern /*@falsenull@*/ bool usymtab_isDefined (usymtab p_u) /*@*/ ;
419 /*@constant null usymtab usymtab_undefined; @*/
420 # define usymtab_undefined ((usymtab)NULL)
421 # define usymtab_isDefined(u) ((u) != usymtab_undefined)
423 extern void usymtab_checkDistinctName (uentry p_e, int p_scope)
424 /*@globals internalState@*/
425 /*@modifies *g_msgstream, p_e@*/ ;
427 extern /*@exposed@*/ sRef usymtab_lookupGlobalMarker (void) /*@globals internalState@*/ ;
429 extern int usymtab_getCurrentDepth (void) /*@globals internalState@*/ ;
432 # error "Multiple include"