]> andersk Git - splint.git/blob - src/Headers/usymtab.h
Initial revision
[splint.git] / src / Headers / usymtab.h
1 /*
2 ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2000.
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 _refentry { int level; int index; } *refentry;
23 typedef /*@only@*/ refentry o_refentry;
24 typedef o_refentry *refTable;
25
26 struct _usymtab
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;
35   /*@null@*/ /*@only@*/ hashTable htable;   /* for the global environment */
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@*/
50   /*@modifies g_msgstream@*/ ;
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@*/ 
59   /*@modifies *g_msgstream@*/ ;
60
61 extern void usymtab_allUsed (void)
62    /*@globals internalState@*/ 
63    /*@modifies *g_msgstream@*/ ;
64
65 extern void usymtab_allDefined (void)
66    /*@globals internalState@*/
67    /*@modifies *g_msgstream@*/ ;
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@*/ ;
94 extern /*@observer@*/ uentry usymtab_lookup (cstring p_k)
95    /*@globals internalState@*/ ;
96 # define usymtab_lookup(s) (usymtab_lookupExpose (s))
97
98 extern /*@observer@*/ uentry usymtab_lookupGlob (cstring p_k)
99    /*@globals internalState@*/ ;
100 extern /*@exposed@*/ uentry usymtab_lookupExposeGlob (cstring p_k)
101    /*@globals internalState@*/ ;
102 extern /*@observer@*/ uentry usymtab_lookupUnionTag (cstring p_k)
103    /*@globals internalState@*/ ;
104 extern /*@observer@*/ uentry usymtab_lookupStructTag (cstring p_k)
105    /*@globals internalState@*/ ;
106 extern /*@observer@*/ uentry usymtab_lookupEither (cstring p_k)
107    /*@globals internalState@*/ ;
108
109 # ifndef NOLCL
110 extern ctype usymtab_lookupType (cstring p_k)
111    /*@globals internalState@*/ ;
112 # endif
113
114 extern bool usymtab_isProbableNull (sRef p_s)
115    /*@globals internalState@*/ ;
116 extern bool usymtab_isProbableDeepNull (sRef p_s)
117    /*@globals internalState@*/ ;
118
119 # ifndef NOLCL
120 extern usymId usymtab_supExposedTypeEntry (/*@only@*/ uentry p_e, bool p_dodef)
121    /*@modifies internalState, p_e@*/ ;
122 # endif
123
124 extern ctype usymtab_supTypeEntry (/*@only@*/ uentry p_e)
125    /*@modifies internalState, p_e@*/ ;
126
127 extern /*@exposed@*/ uentry usymtab_supReturnTypeEntry (/*@only@*/ uentry p_e)
128    /*@modifies internalState@*/ ;
129
130 extern /*@observer@*/ uentry usymtab_lookupSafe (cstring p_k)
131    /*@globals internalState@*/ ;
132
133 extern /*@observer@*/ uentry usymtab_getGlobalEntry (usymId p_uid)
134   /*@globals internalState@*/ ;
135
136 extern bool usymtab_exists (cstring p_k)
137    /*@globals internalState@*/ ;
138
139 # ifndef NOLCL
140 extern bool usymtab_existsVar (cstring p_k)
141    /*@globals internalState@*/ ;
142 # endif
143
144 extern bool usymtab_existsGlob (cstring p_k)
145    /*@globals internalState@*/ ;
146
147 extern bool usymtab_existsType (cstring p_k)
148    /*@globals internalState@*/ ;
149
150 # ifndef NOLCL
151 extern bool usymtab_existsEither (cstring p_k)
152    /*@globals internalState@*/ ;
153 # endif
154
155 extern bool usymtab_existsTypeEither (cstring p_k)
156    /*@globals internalState@*/ ;
157
158 extern usymId usymtab_getId (cstring p_k) /*@globals internalState@*/ ;
159 extern usymId usymtab_getTypeId (cstring p_k) /*@globals internalState@*/ ;
160
161 extern void usymtab_supEntry (/*@only@*/ uentry p_e)
162   /*@modifies internalState, p_e@*/ ;
163
164 # ifndef NOLCL
165 extern void usymtab_replaceEntry (/*@only@*/ uentry p_s)
166   /*@modifies internalState, p_s@*/ ;
167 # endif
168
169 extern void usymtab_supEntrySref (/*@only@*/ uentry p_e)
170   /*@modifies internalState, p_e@*/ ;
171
172 extern void usymtab_supGlobalEntry (/*@only@*/ uentry p_e)
173   /*@modifies internalState@*/ ;
174
175 extern void usymtab_addGlobalEntry (/*@only@*/ uentry p_e) 
176   /*@modifies internalState, p_e@*/ ;
177
178 extern /*@exposed@*/ uentry 
179   usymtab_supEntryReturn (/*@only@*/ uentry p_e)
180   /*@modifies internalState, p_e@*/ ;
181
182 extern usymId usymtab_addEntry (/*@only@*/ uentry p_e)
183   /*@modifies internalState, p_e@*/ ;
184
185 extern ctype usymtab_lookupAbstractType (cstring p_k) 
186   /*@globals internalState@*/ ;
187 extern bool usymtab_matchForwardStruct (usymId p_u1, usymId p_u2)
188   /*@globals internalState@*/ ;
189
190 extern bool usymtab_existsEnumTag (cstring p_k)
191   /*@globals internalState@*/ ;
192 extern bool usymtab_existsUnionTag (cstring p_k) 
193   /*@globals internalState@*/ ;
194 extern bool usymtab_existsStructTag (cstring p_k) 
195   /*@globals internalState@*/ ;
196
197 extern usymId usymId_fromInt (int p_i) /*@*/ ;
198 # define usymId_fromInt(i)   ((usymId)(i))
199
200 extern bool usymId_isInvalid (usymId p_u) /*@*/ ;
201 # define usymId_isInvalid(u) ((u) == USYMIDINVALID)
202
203 extern bool usymId_isValid (usymId p_u) /*@*/ ;
204 # define usymId_isValid(u)   ((u) != USYMIDINVALID)
205
206 extern bool typeId_isInvalid (typeId p_u) /*@*/ ;
207 # define typeId_isInvalid(u) ((u) == typeId_invalid)
208
209 extern bool typeId_isValid (typeId p_u) /*@*/ ;
210 # define typeId_isValid(u)   ((u) != typeId_invalid)
211
212 extern bool typeId_equal (typeId p_u1, typeId p_u2) /*@*/ ;
213 # define typeId_equal(u1,u2) ((u1) == (u2))
214
215 extern typeId typeId_fromInt (int p_i);
216 # define typeId_fromInt(i)   ((typeId)(i))
217
218 /*@iter usymtab_entries (sef usymtab u, yield exposed uentry el); @*/
219 # define usymtab_entries(x, m_i)   \
220     { int m_ind; \
221       if (usymtab_isDefined (x)) \
222         for (m_ind = 0; m_ind < (x)->nentries; m_ind++) \
223            { uentry m_i = (x)->entries[m_ind]; 
224
225 # define end_usymtab_entries }}
226
227 extern /*@unused@*/ void usymtab_displayAllUses (void)
228    /*@globals internalState@*/ 
229    /*@modifies *g_msgstream@*/ ;
230
231 extern /*@unused@*/ void usymtab_printOut (void)
232    /*@globals internalState@*/ 
233    /*@modifies *g_msgstream@*/ ;
234
235 extern /*@unused@*/ void usymtab_printAll (void)
236    /*@globals internalState@*/ 
237    /*@modifies *g_msgstream@*/ ;
238
239 extern void usymtab_enterScope (void) 
240   /*@modifies internalState;@*/ ;
241 extern void usymtab_enterFunctionScope (uentry p_fcn) 
242   /*@modifies internalState;@*/ ;
243 extern void usymtab_quietExitScope (fileloc p_loc)
244   /*@modifies internalState;@*/ ;
245 extern void usymtab_exitScope (exprNode p_expr) /*@modifies internalState@*/ ;
246 extern void usymtab_addGuards (guardSet p_guards) /*@modifies internalState@*/ ;
247 extern void usymtab_setExitCode (exitkind p_ex) /*@modifies internalState@*/ ;
248 extern void usymtab_exitFile (void) /*@modifies internalState@*/ ;
249 extern void usymtab_enterFile (void) /*@modifies internalState@*/ ;
250
251 extern /*@observer@*/ uentry usymtab_lookupEnumTag (cstring p_k)
252   /*@globals internalState@*/ ; 
253
254 extern usymId usymtab_convertId (usymId p_uid) /*@globals internalState@*/ ;
255 extern void usymtab_initMod (void) /*@modifies internalState@*/ ;
256 extern void usymtab_initBool (void) /*@modifies internalState@*/ ;
257
258 extern void usymtab_exportHeader (void)
259    /*@modifies internalState@*/ ;
260
261 extern ctype usymtab_structFieldsType (uentryList p_f)
262    /*@globals internalState@*/ ;
263
264 extern ctype usymtab_unionFieldsType (uentryList p_f)
265    /*@globals internalState@*/ ;
266
267 extern ctype usymtab_enumEnumNameListType (enumNameList p_f)
268    /*@globals internalState@*/ ;
269
270 extern /*@exposed@*/ uentry usymtab_getTypeEntrySafe (usymId p_uid)
271    /*@globals internalState@*/ ;
272
273 extern void usymtab_popOrBranch (exprNode p_pred, exprNode p_expr)
274   /*@modifies internalState@*/ ;
275 extern void usymtab_popAndBranch (exprNode p_pred, exprNode p_expr)
276   /*@modifies internalState@*/ ;
277
278 extern void usymtab_trueBranch (/*@only@*/ guardSet p_guards)
279   /*@modifies internalState@*/ ;
280 extern void usymtab_altBranch (/*@only@*/ guardSet p_guards)
281   /*@modifies internalState@*/ ;
282
283 extern void usymtab_popTrueBranch (exprNode p_pred, exprNode p_expr, clause p_cl)
284   /*@modifies internalState@*/ ;
285 extern void
286   usymtab_popTrueExecBranch (exprNode p_pred, exprNode p_expr, clause p_cl)
287   /*@modifies internalState@*/ ;
288
289 extern void 
290   usymtab_popBranches (exprNode p_pred, exprNode p_tbranch, exprNode p_fbranch, 
291                        bool p_isOpt, clause p_cl)
292    /*@modifies internalState@*/ ;
293
294 extern void usymtab_unguard (sRef p_s) /*@modifies internalState@*/ ;
295 extern bool usymtab_isGuarded (sRef p_s) /*@globals internalState@*/ ;
296 extern void usymtab_printGuards (void) /*@globals internalState@*/ /*@modifies *g_msgstream@*/ ;
297 extern void usymtab_quietPlainExitScope (void) /*@modifies internalState@*/ ;
298 extern void usymtab_printComplete (void) /*@globals internalState@*/ /*@modifies *stdout@*/ ;
299
300 # ifndef NOLCL
301 extern bool usymtab_existsGlobEither (cstring p_k) /*@globals internalState@*/ ;
302 # endif
303
304 extern bool usymtab_isBoolType (usymId p_uid) /*@globals internalState@*/ ;
305 extern /*@only@*/ cstring 
306   usymtab_getTypeEntryName (usymId p_uid)
307   /*@globals internalState@*/ ;
308 extern /*@exposed@*/ uentry usymtab_getTypeEntry (usymId p_uid)
309   /*@globals internalState@*/ ;
310
311 extern usymId 
312   usymtab_supAbstractTypeEntry (/*@only@*/ uentry p_e, bool p_dodef)
313   /*@modifies internalState, p_e@*/ ;
314 extern ctype usymtab_supForwardTypeEntry (/*@only@*/ uentry p_e)
315   /*@modifies internalState, p_e@*/ ;
316
317 extern /*@exposed@*/ uentry 
318   usymtab_supGlobalEntryReturn (/*@only@*/ uentry p_e)
319   /*@modifies internalState, p_e@*/ ;
320
321 extern /*@exposed@*/ uentry 
322   usymtab_supEntrySrefReturn (/*@only@*/ uentry p_e)
323   /*@modifies internalState, p_e@*/ ;
324
325 extern int uentry_directParamNo (uentry p_ue)
326   /*@globals internalState@*/ ;
327
328 extern bool usymtab_newCase (exprNode p_pred, exprNode p_last)
329   /*@modifies internalState@*/ ;
330
331 extern void usymtab_switchBranch (exprNode p_s) 
332   /*@modifies internalState@*/ ;
333
334 extern /*@only@*/ cstring usymtab_unparseStack (void)
335   /*@globals internalState@*/ ;
336 extern void usymtab_exitSwitch (exprNode p_sw, bool p_allpaths)
337   /*@modifies internalState@*/ ;
338
339 extern /*@observer@*/ uentry usymtab_lookupGlobSafe (cstring p_k)
340   /*@globals internalState@*/ ;
341
342 extern /*@only@*/ sRefSet usymtab_aliasedBy (sRef p_s)
343   /*@globals internalState@*/ ;
344
345 extern /*@only@*/ sRefSet usymtab_canAlias (sRef p_s)
346   /*@globals internalState@*/ ;
347
348 extern void usymtab_clearAlias (sRef p_s)
349   /*@modifies internalState, p_s@*/ ;
350
351 extern void usymtab_addMustAlias (sRef p_s, sRef p_al)
352   /*@modifies internalState@*/ ;
353
354 extern void usymtab_addForceMustAlias (sRef p_s, sRef p_al)
355   /*@modifies internalState@*/ ;
356
357 extern /*@only@*/ cstring usymtab_unparseAliases (void)
358   /*@globals internalState@*/ ;
359
360 extern /*@exposed@*/ uentry
361   usymtab_supReturnFileEntry (/*@only@*/ uentry p_e)
362    /*@modifies internalState@*/ ;
363
364 extern bool usymtab_isAltProbablyDeepNull (sRef p_s)
365    /*@globals internalState@*/ ;
366
367 extern bool usymtab_existsReal (cstring p_k)
368    /*@globals internalState@*/ ;
369
370 extern /*@only@*/ sRefSet usymtab_allAliases (sRef p_s)
371    /*@globals internalState@*/ ;
372
373 extern void usymtab_exportLocal (void)
374    /*@modifies internalState@*/ ;
375
376 extern void usymtab_popCaseBranch (void)
377      /*@modifies internalState@*/ ;
378
379 /* special scopes */
380
381 /*@constant int globScope;@*/
382 # define globScope 0  /* global variables */
383
384 /*@constant int fileScope;@*/
385 # define fileScope   1  /* file-level static variables */
386
387 /*@constant int paramsScope;@*/
388 # define paramsScope 2  /* function parameters */
389
390 /*@constant int functionScope;@*/
391 # define functionScope 3
392
393 extern /*@falsenull@*/ bool usymtab_isDefined (usymtab p_u) /*@*/ ;
394
395 /*@constant null usymtab usymtab_undefined; @*/
396 # define usymtab_undefined ((usymtab)NULL)
397 # define usymtab_isDefined(u) ((u) != usymtab_undefined)
398
399 extern void usymtab_checkDistinctName (uentry p_e, int p_scope)
400   /*@globals internalState@*/
401   /*@modifies *g_msgstream, p_e@*/ ;
402
403 # else
404 # error "Multiple include"
405 # endif
406
407
408
This page took 0.1261 seconds and 5 git commands to generate.