2 ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2003.
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 { int level; int index; } *refentry;
23 typedef /*@only@*/ refentry o_refentry;
24 typedef o_refentry *refTable;
34 /*@reldef@*/ /*@only@*/ o_uentry *entries;
35 /*@null@*/ /*@only@*/ cstringTable htable; /* for the global environment */
36 /*@null@*/ /*@only@*/ refTable reftable; /* for branched environments */
37 /*@only@*/ guardSet guards; /* guarded references (not null) */
39 /*@owned@*/ usymtab env;
45 ** (left as exercise to reader) ;)
48 extern void usymtab_printTypes (void)
49 /*@globals internalState@*/
50 /*@modifies g_warningstream@*/ ;
52 extern void usymtab_setMustBreak (void) /*@modifies internalState@*/ ;
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@*/
59 /*@modifies *g_warningstream@*/ ;
61 extern void usymtab_allUsed (void)
62 /*@globals internalState@*/
63 /*@modifies *g_warningstream@*/ ;
65 extern void usymtab_allDefined (void)
66 /*@globals internalState@*/
67 /*@modifies *g_warningstream@*/ ;
69 extern void usymtab_prepareDump (void)
70 /*@modifies internalState@*/ ;
72 extern void usymtab_dump (FILE *p_fout)
73 /*@globals internalState@*/
74 /*@modifies *p_fout@*/ ;
77 extern void usymtab_load (FILE *p_f) /*@modifies p_f, internalState@*/ ;
79 extern /*@exposed@*/ /*@dependent@*/ uentry
80 usymtab_getRefQuiet (int p_level, usymId p_index)
81 /*@globals internalState@*/ ;
83 extern void usymtab_printLocal (void)
84 /*@globals internalState@*/
85 /*@modifies stdout@*/ ;
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@*/ ;
92 extern /*@exposed@*/ uentry usymtab_lookupExpose (cstring p_k)
93 /*@globals internalState@*/ ;
95 extern /*@observer@*/ uentry usymtab_lookup (cstring p_k)
96 /*@globals internalState@*/ ;
98 # define usymtab_lookup(s) (usymtab_lookupExpose (s))
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@*/ ;
111 extern ctype usymtab_lookupType (cstring p_k)
112 /*@globals internalState@*/ ;
114 extern bool usymtab_isDefinitelyNull (sRef p_s)
115 /*@globals internalState@*/ ;
116 extern bool usymtab_isDefinitelyNullDeep (sRef p_s)
117 /*@globals internalState@*/ ;
119 extern usymId usymtab_supExposedTypeEntry (/*@only@*/ uentry p_e, bool p_dodef)
120 /*@modifies internalState, p_e@*/ ;
122 extern ctype usymtab_supTypeEntry (/*@only@*/ uentry p_e)
123 /*@modifies internalState, p_e@*/ ;
125 extern /*@exposed@*/ uentry usymtab_supReturnTypeEntry (/*@only@*/ uentry p_e)
126 /*@modifies internalState@*/ ;
128 extern /*@observer@*/ uentry usymtab_lookupSafe (cstring p_k)
129 /*@globals internalState@*/ ;
131 extern /*@observer@*/ uentry usymtab_getGlobalEntry (usymId p_uid)
132 /*@globals internalState@*/ ;
134 extern bool usymtab_exists (cstring p_k)
135 /*@globals internalState@*/ ;
137 extern bool usymtab_existsVar (cstring p_k)
138 /*@globals internalState@*/ ;
140 extern bool usymtab_existsGlob (cstring p_k)
141 /*@globals internalState@*/ ;
143 extern bool usymtab_existsType (cstring p_k)
144 /*@globals internalState@*/ ;
146 extern bool usymtab_existsEither (cstring p_k)
147 /*@globals internalState@*/ ;
149 extern bool usymtab_existsTypeEither (cstring p_k)
150 /*@globals internalState@*/ ;
152 extern usymId usymtab_getId (cstring p_k) /*@globals internalState@*/ ;
153 extern typeId usymtab_getTypeId (cstring p_k) /*@globals internalState@*/ ;
155 extern void usymtab_supEntry (/*@only@*/ uentry p_e)
156 /*@modifies internalState, p_e@*/ ;
158 extern void usymtab_replaceEntry (/*@only@*/ uentry p_s)
159 /*@modifies internalState, p_s@*/ ;
161 extern void usymtab_supEntrySref (/*@only@*/ uentry p_e)
162 /*@modifies internalState, p_e@*/ ;
164 extern void usymtab_supGlobalEntry (/*@only@*/ uentry p_e)
165 /*@modifies internalState@*/ ;
167 extern void usymtab_addGlobalEntry (/*@only@*/ uentry p_e)
168 /*@modifies internalState, p_e@*/ ;
170 extern /*@exposed@*/ uentry
171 usymtab_supEntryReturn (/*@only@*/ uentry p_e)
172 /*@modifies internalState, p_e@*/ ;
174 extern usymId usymtab_addEntry (/*@only@*/ uentry p_e)
175 /*@modifies internalState, p_e@*/ ;
177 extern ctype usymtab_lookupAbstractType (cstring p_k)
178 /*@globals internalState@*/ /*@modifies nothing@*/ ;
180 extern bool usymtab_matchForwardStruct (typeId p_u1, typeId p_u2)
181 /*@globals internalState@*/ ;
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@*/ ;
190 /*@iter usymtab_entries (sef usymtab u, yield exposed uentry el); @*/
191 # define usymtab_entries(x, m_i) \
193 if (usymtab_isDefined (x)) \
194 for (m_ind = 0; m_ind < (x)->nentries; m_ind++) \
195 { uentry m_i = (x)->entries[m_ind];
197 # define end_usymtab_entries }}
199 extern /*@unused@*/ void usymtab_displayAllUses (void)
200 /*@globals internalState@*/
201 /*@modifies *g_warningstream@*/ ;
203 extern /*@unused@*/ void usymtab_printOut (void)
204 /*@globals internalState@*/
205 /*@modifies *g_warningstream@*/ ;
207 extern /*@unused@*/ void usymtab_printAll (void)
208 /*@globals internalState@*/
209 /*@modifies *g_warningstream@*/ ;
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@*/ ;
223 extern /*@observer@*/ uentry usymtab_lookupEnumTag (cstring p_k)
224 /*@globals internalState@*/ ;
226 extern usymId usymtab_convertId (usymId p_uid) /*@globals internalState@*/ ;
227 extern typeId usymtab_convertTypeId (typeId p_uid) /*@globals internalState@*/ ;
228 extern void usymtab_initMod (void) /*@modifies internalState@*/ ;
229 extern void usymtab_destroyMod (void) /*@modifies internalState@*/ ;
230 extern void usymtab_initBool (void) /*@modifies internalState@*/ ;
231 extern void usymtab_initGlobalMarker (void) /*@modifies internalState@*/ ;
233 extern void usymtab_exportHeader (void)
234 /*@modifies internalState@*/ ;
236 extern ctype usymtab_structFieldsType (uentryList p_f)
237 /*@globals internalState@*/ ;
239 extern ctype usymtab_unionFieldsType (uentryList p_f)
240 /*@globals internalState@*/ ;
242 extern ctype usymtab_enumEnumNameListType (enumNameList p_f)
243 /*@globals internalState@*/ ;
245 extern /*@exposed@*/ uentry usymtab_getTypeEntrySafe (typeId p_uid)
246 /*@globals internalState@*/ ;
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@*/ ;
253 extern void usymtab_trueBranch (/*@only@*/ guardSet p_guards)
254 /*@modifies internalState@*/ ;
255 extern void usymtab_altBranch (/*@only@*/ guardSet p_guards)
256 /*@modifies internalState@*/ ;
258 extern void usymtab_popTrueBranch (exprNode p_pred, exprNode p_expr, clause p_cl)
259 /*@modifies internalState@*/ ;
262 usymtab_popTrueExecBranch (exprNode p_pred, exprNode p_expr, clause p_cl)
263 /*@modifies internalState@*/ ;
266 usymtab_popBranches (exprNode p_pred, exprNode p_tbranch, exprNode p_fbranch,
267 bool p_isOpt, clause p_cl)
268 /*@modifies internalState@*/ ;
270 extern void usymtab_unguard (sRef p_s) /*@modifies internalState@*/ ;
271 extern bool usymtab_isGuarded (sRef p_s) /*@globals internalState@*/ ;
272 extern void usymtab_printGuards (void) /*@globals internalState@*/ /*@modifies *g_warningstream@*/ ;
273 extern void usymtab_quietPlainExitScope (void) /*@modifies internalState@*/ ;
274 extern void usymtab_printComplete (void) /*@globals internalState@*/ /*@modifies *stdout@*/ ;
276 extern bool usymtab_existsGlobEither (cstring p_k) /*@globals internalState@*/ ;
278 extern bool usymtab_isBoolType (typeId p_uid) /*@globals internalState@*/ ;
279 extern /*@only@*/ cstring usymtab_getTypeEntryName (typeId p_uid)
280 /*@globals internalState@*/ ;
281 extern /*@exposed@*/ uentry usymtab_getTypeEntry (typeId p_uid)
282 /*@globals internalState@*/ ;
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@*/ ;
290 extern /*@exposed@*/ uentry
291 usymtab_supGlobalEntryReturn (/*@only@*/ uentry p_e)
292 /*@modifies internalState, p_e@*/ ;
294 extern /*@exposed@*/ uentry
295 usymtab_supEntrySrefReturn (/*@only@*/ uentry p_e)
296 /*@modifies internalState, p_e@*/ ;
298 extern usymId usymtab_directParamNo (uentry p_ue)
299 /*@globals internalState@*/ ;
301 extern bool usymtab_newCase (exprNode p_pred, exprNode p_last)
302 /*@modifies internalState@*/ ;
304 extern void usymtab_switchBranch (exprNode p_s)
305 /*@modifies internalState@*/ ;
307 extern /*@only@*/ cstring usymtab_unparseStack (void)
308 /*@globals internalState@*/ ;
309 extern void usymtab_exitSwitch (exprNode p_sw, bool p_allpaths)
310 /*@modifies internalState@*/ ;
312 extern /*@observer@*/ uentry usymtab_lookupGlobSafe (cstring p_k)
313 /*@globals internalState@*/ ;
315 extern /*@only@*/ sRefSet usymtab_aliasedBy (sRef p_s)
316 /*@globals internalState@*/ ;
318 extern /*@only@*/ sRefSet usymtab_canAlias (sRef p_s)
319 /*@globals internalState@*/ ;
321 extern void usymtab_clearAlias (sRef p_s)
322 /*@modifies internalState, p_s@*/ ;
324 extern void usymtab_addMustAlias (/*@exposed@*/ sRef p_s, /*@exposed@*/ sRef p_al)
325 /*@modifies internalState@*/ ;
327 extern void usymtab_addForceMustAlias (/*@exposed@*/ sRef p_s, /*@exposed@*/ sRef p_al)
328 /*@modifies internalState@*/ ;
330 extern /*@only@*/ cstring usymtab_unparseAliases (void)
331 /*@globals internalState@*/ ;
333 extern /*@exposed@*/ uentry
334 usymtab_supReturnFileEntry (/*@only@*/ uentry p_e)
335 /*@modifies internalState@*/ ;
337 extern bool usymtab_isAltDefinitelyNullDeep (sRef p_s)
338 /*@globals internalState@*/ ;
340 extern bool usymtab_existsReal (cstring p_k)
341 /*@globals internalState@*/ ;
343 extern /*@only@*/ sRefSet usymtab_allAliases (sRef p_s)
344 /*@globals internalState@*/ ;
346 extern void usymtab_exportLocal (void)
347 /*@modifies internalState@*/ ;
349 extern void usymtab_popCaseBranch (void)
350 /*@modifies internalState@*/ ;
354 /*@constant int globScope;@*/
355 # define globScope 0 /* global variables */
357 /*@constant int fileScope;@*/
358 # define fileScope 1 /* file-level static variables */
360 /*@constant int paramsScope;@*/
361 # define paramsScope 2 /* function parameters */
363 /*@constant int functionScope;@*/
364 # define functionScope 3
366 extern /*@falsewhennull@*/ bool usymtab_isDefined (usymtab p_u) /*@*/ ;
368 /*@constant null usymtab usymtab_undefined; @*/
369 # define usymtab_undefined ((usymtab)NULL)
370 # define usymtab_isDefined(u) ((u) != usymtab_undefined)
372 extern void usymtab_checkDistinctName (uentry p_e, int p_scope)
373 /*@globals internalState@*/
374 /*@modifies *g_warningstream, p_e@*/ ;
376 extern /*@exposed@*/ sRef usymtab_lookupGlobalMarker (void) /*@globals internalState@*/ ;
377 extern void usymtab_addReallyForceMustAlias (/*@exposed@*/ sRef p_s, /*@exposed@*/ sRef p_al) /*@modifies internalState@*/ ;
378 extern int usymtab_getCurrentDepth (void) /*@globals internalState@*/ ;
381 extern void usymtab_checkAllValid (void) /*@modifies g_errorstream@*/ ;
385 # error "Multiple include"