]>
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) |
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) |
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) |
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) |
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) |
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 |