]> andersk Git - splint.git/blame - src/Headers/usymtab.h
andersk / splint.git / blame
? search:
summary | shortlog | log | commit | commitdiff | tree
blob | blame (incremental) | history | HEAD
Initial revision
[splint.git] / src / Headers / usymtab.h
CommitLineData
885824d3 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
15typedef enum {
16 US_GLOBAL,
17 US_NORMAL,
18 US_TBRANCH, US_FBRANCH,
19 US_CBRANCH, US_SWITCH
20} uskind;
21
22typedef struct _refentry { int level; int index; } *refentry;
23typedef /*@only@*/ refentry o_refentry;
24typedef o_refentry *refTable;
25
26struct _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
48extern void usymtab_printTypes (void)
49 /*@globals internalState@*/
50 /*@modifies g_msgstream@*/ ;
51
52extern void usymtab_setMustBreak (void) /*@modifies internalState@*/ ;
53
54extern bool usymtab_inGlobalScope (void) /*@globals internalState@*/ ;
55extern bool usymtab_inFunctionScope (void) /*@globals internalState@*/ ;
56extern bool usymtab_inFileScope (void) /*@globals internalState@*/ ;
57extern void usymtab_checkFinalScope (bool p_isReturn)
58 /*@globals internalState@*/
59 /*@modifies *g_msgstream@*/ ;
60
61extern void usymtab_allUsed (void)
62 /*@globals internalState@*/
63 /*@modifies *g_msgstream@*/ ;
64
65extern void usymtab_allDefined (void)
66 /*@globals internalState@*/
67 /*@modifies *g_msgstream@*/ ;
68
69extern void usymtab_prepareDump (void)
70 /*@modifies internalState@*/ ;
71
72extern void usymtab_dump (FILE *p_fout)
73 /*@globals internalState@*/
74 /*@modifies *p_fout@*/ ;
75
76
77extern void usymtab_load (FILE *p_f) /*@modifies p_f, internalState@*/ ;
78
79extern /*@exposed@*/ /*@dependent@*/ uentry
80 usymtab_getRefQuiet (int p_level, usymId p_index)
81 /*@globals internalState@*/ ;
82
83extern void usymtab_printLocal (void)
84 /*@globals internalState@*/
85 /*@modifies stdout@*/ ;
86
87extern /*@exposed@*/ /*@dependent@*/ uentry usymtab_getParam (int p_paramno)
88 /*@globals internalState@*/;
89extern void usymtab_free (void) /*@modifies internalState@*/ ;
90extern bool usymtab_inDeepScope (void) /*@globals internalState@*/ ;
91
92extern /*@exposed@*/ uentry usymtab_lookupExpose (cstring p_k)
93 /*@globals internalState@*/ ;
94extern /*@observer@*/ uentry usymtab_lookup (cstring p_k)
95 /*@globals internalState@*/ ;
96# define usymtab_lookup(s) (usymtab_lookupExpose (s))
97
98extern /*@observer@*/ uentry usymtab_lookupGlob (cstring p_k)
99 /*@globals internalState@*/ ;
100extern /*@exposed@*/ uentry usymtab_lookupExposeGlob (cstring p_k)
101 /*@globals internalState@*/ ;
102extern /*@observer@*/ uentry usymtab_lookupUnionTag (cstring p_k)
103 /*@globals internalState@*/ ;
104extern /*@observer@*/ uentry usymtab_lookupStructTag (cstring p_k)
105 /*@globals internalState@*/ ;
106extern /*@observer@*/ uentry usymtab_lookupEither (cstring p_k)
107 /*@globals internalState@*/ ;
108
109# ifndef NOLCL
110extern ctype usymtab_lookupType (cstring p_k)
111 /*@globals internalState@*/ ;
112# endif
113
114extern bool usymtab_isProbableNull (sRef p_s)
115 /*@globals internalState@*/ ;
116extern bool usymtab_isProbableDeepNull (sRef p_s)
117 /*@globals internalState@*/ ;
118
119# ifndef NOLCL
120extern usymId usymtab_supExposedTypeEntry (/*@only@*/ uentry p_e, bool p_dodef)
121 /*@modifies internalState, p_e@*/ ;
122# endif
123
124extern ctype usymtab_supTypeEntry (/*@only@*/ uentry p_e)
125 /*@modifies internalState, p_e@*/ ;
126
127extern /*@exposed@*/ uentry usymtab_supReturnTypeEntry (/*@only@*/ uentry p_e)
128 /*@modifies internalState@*/ ;
129
130extern /*@observer@*/ uentry usymtab_lookupSafe (cstring p_k)
131 /*@globals internalState@*/ ;
132
133extern /*@observer@*/ uentry usymtab_getGlobalEntry (usymId p_uid)
134 /*@globals internalState@*/ ;
135
136extern bool usymtab_exists (cstring p_k)
137 /*@globals internalState@*/ ;
138
139# ifndef NOLCL
140extern bool usymtab_existsVar (cstring p_k)
141 /*@globals internalState@*/ ;
142# endif
143
144extern bool usymtab_existsGlob (cstring p_k)
145 /*@globals internalState@*/ ;
146
147extern bool usymtab_existsType (cstring p_k)
148 /*@globals internalState@*/ ;
149
150# ifndef NOLCL
151extern bool usymtab_existsEither (cstring p_k)
152 /*@globals internalState@*/ ;
153# endif
154
155extern bool usymtab_existsTypeEither (cstring p_k)
156 /*@globals internalState@*/ ;
157
158extern usymId usymtab_getId (cstring p_k) /*@globals internalState@*/ ;
159extern usymId usymtab_getTypeId (cstring p_k) /*@globals internalState@*/ ;
160
161extern void usymtab_supEntry (/*@only@*/ uentry p_e)
162 /*@modifies internalState, p_e@*/ ;
163
164# ifndef NOLCL
165extern void usymtab_replaceEntry (/*@only@*/ uentry p_s)
166 /*@modifies internalState, p_s@*/ ;
167# endif
168
169extern void usymtab_supEntrySref (/*@only@*/ uentry p_e)
170 /*@modifies internalState, p_e@*/ ;
171
172extern void usymtab_supGlobalEntry (/*@only@*/ uentry p_e)
173 /*@modifies internalState@*/ ;
174
175extern void usymtab_addGlobalEntry (/*@only@*/ uentry p_e)
176 /*@modifies internalState, p_e@*/ ;
177
178extern /*@exposed@*/ uentry
179 usymtab_supEntryReturn (/*@only@*/ uentry p_e)
180 /*@modifies internalState, p_e@*/ ;
181
182extern usymId usymtab_addEntry (/*@only@*/ uentry p_e)
183 /*@modifies internalState, p_e@*/ ;
184
185extern ctype usymtab_lookupAbstractType (cstring p_k)
186 /*@globals internalState@*/ ;
187extern bool usymtab_matchForwardStruct (usymId p_u1, usymId p_u2)
188 /*@globals internalState@*/ ;
189
190extern bool usymtab_existsEnumTag (cstring p_k)
191 /*@globals internalState@*/ ;
192extern bool usymtab_existsUnionTag (cstring p_k)
193 /*@globals internalState@*/ ;
194extern bool usymtab_existsStructTag (cstring p_k)
195 /*@globals internalState@*/ ;
196
197extern usymId usymId_fromInt (int p_i) /*@*/ ;
198# define usymId_fromInt(i) ((usymId)(i))
199
200extern bool usymId_isInvalid (usymId p_u) /*@*/ ;
201# define usymId_isInvalid(u) ((u) == USYMIDINVALID)
202
203extern bool usymId_isValid (usymId p_u) /*@*/ ;
204# define usymId_isValid(u) ((u) != USYMIDINVALID)
205
206extern bool typeId_isInvalid (typeId p_u) /*@*/ ;
207# define typeId_isInvalid(u) ((u) == typeId_invalid)
208
209extern bool typeId_isValid (typeId p_u) /*@*/ ;
210# define typeId_isValid(u) ((u) != typeId_invalid)
211
212extern bool typeId_equal (typeId p_u1, typeId p_u2) /*@*/ ;
213# define typeId_equal(u1,u2) ((u1) == (u2))
214
215extern 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
227extern /*@unused@*/ void usymtab_displayAllUses (void)
228 /*@globals internalState@*/
229 /*@modifies *g_msgstream@*/ ;
230
231extern /*@unused@*/ void usymtab_printOut (void)
232 /*@globals internalState@*/
233 /*@modifies *g_msgstream@*/ ;
234
235extern /*@unused@*/ void usymtab_printAll (void)
236 /*@globals internalState@*/
237 /*@modifies *g_msgstream@*/ ;
238
239extern void usymtab_enterScope (void)
240 /*@modifies internalState;@*/ ;
241extern void usymtab_enterFunctionScope (uentry p_fcn)
242 /*@modifies internalState;@*/ ;
243extern void usymtab_quietExitScope (fileloc p_loc)
244 /*@modifies internalState;@*/ ;
245extern void usymtab_exitScope (exprNode p_expr) /*@modifies internalState@*/ ;
246extern void usymtab_addGuards (guardSet p_guards) /*@modifies internalState@*/ ;
247extern void usymtab_setExitCode (exitkind p_ex) /*@modifies internalState@*/ ;
248extern void usymtab_exitFile (void) /*@modifies internalState@*/ ;
249extern void usymtab_enterFile (void) /*@modifies internalState@*/ ;
250
251extern /*@observer@*/ uentry usymtab_lookupEnumTag (cstring p_k)
252 /*@globals internalState@*/ ;
253
254extern usymId usymtab_convertId (usymId p_uid) /*@globals internalState@*/ ;
255extern void usymtab_initMod (void) /*@modifies internalState@*/ ;
256extern void usymtab_initBool (void) /*@modifies internalState@*/ ;
257
258extern void usymtab_exportHeader (void)
259 /*@modifies internalState@*/ ;
260
261extern ctype usymtab_structFieldsType (uentryList p_f)
262 /*@globals internalState@*/ ;
263
264extern ctype usymtab_unionFieldsType (uentryList p_f)
265 /*@globals internalState@*/ ;
266
267extern ctype usymtab_enumEnumNameListType (enumNameList p_f)
268 /*@globals internalState@*/ ;
269
270extern /*@exposed@*/ uentry usymtab_getTypeEntrySafe (usymId p_uid)
271 /*@globals internalState@*/ ;
272
273extern void usymtab_popOrBranch (exprNode p_pred, exprNode p_expr)
274 /*@modifies internalState@*/ ;
275extern void usymtab_popAndBranch (exprNode p_pred, exprNode p_expr)
276 /*@modifies internalState@*/ ;
277
278extern void usymtab_trueBranch (/*@only@*/ guardSet p_guards)
279 /*@modifies internalState@*/ ;
280extern void usymtab_altBranch (/*@only@*/ guardSet p_guards)
281 /*@modifies internalState@*/ ;
282
283extern void usymtab_popTrueBranch (exprNode p_pred, exprNode p_expr, clause p_cl)
284 /*@modifies internalState@*/ ;
285extern void
286 usymtab_popTrueExecBranch (exprNode p_pred, exprNode p_expr, clause p_cl)
287 /*@modifies internalState@*/ ;
288
289extern void
290 usymtab_popBranches (exprNode p_pred, exprNode p_tbranch, exprNode p_fbranch,
291 bool p_isOpt, clause p_cl)
292 /*@modifies internalState@*/ ;
293
294extern void usymtab_unguard (sRef p_s) /*@modifies internalState@*/ ;
295extern bool usymtab_isGuarded (sRef p_s) /*@globals internalState@*/ ;
296extern void usymtab_printGuards (void) /*@globals internalState@*/ /*@modifies *g_msgstream@*/ ;
297extern void usymtab_quietPlainExitScope (void) /*@modifies internalState@*/ ;
298extern void usymtab_printComplete (void) /*@globals internalState@*/ /*@modifies *stdout@*/ ;
299
300# ifndef NOLCL
301extern bool usymtab_existsGlobEither (cstring p_k) /*@globals internalState@*/ ;
302# endif
303
304extern bool usymtab_isBoolType (usymId p_uid) /*@globals internalState@*/ ;
305extern /*@only@*/ cstring
306 usymtab_getTypeEntryName (usymId p_uid)
307 /*@globals internalState@*/ ;
308extern /*@exposed@*/ uentry usymtab_getTypeEntry (usymId p_uid)
309 /*@globals internalState@*/ ;
310
311extern usymId
312 usymtab_supAbstractTypeEntry (/*@only@*/ uentry p_e, bool p_dodef)
313 /*@modifies internalState, p_e@*/ ;
314extern ctype usymtab_supForwardTypeEntry (/*@only@*/ uentry p_e)
315 /*@modifies internalState, p_e@*/ ;
316
317extern /*@exposed@*/ uentry
318 usymtab_supGlobalEntryReturn (/*@only@*/ uentry p_e)
319 /*@modifies internalState, p_e@*/ ;
320
321extern /*@exposed@*/ uentry
322 usymtab_supEntrySrefReturn (/*@only@*/ uentry p_e)
323 /*@modifies internalState, p_e@*/ ;
324
325extern int uentry_directParamNo (uentry p_ue)
326 /*@globals internalState@*/ ;
327
328extern bool usymtab_newCase (exprNode p_pred, exprNode p_last)
329 /*@modifies internalState@*/ ;
330
331extern void usymtab_switchBranch (exprNode p_s)
332 /*@modifies internalState@*/ ;
333
334extern /*@only@*/ cstring usymtab_unparseStack (void)
335 /*@globals internalState@*/ ;
336extern void usymtab_exitSwitch (exprNode p_sw, bool p_allpaths)
337 /*@modifies internalState@*/ ;
338
339extern /*@observer@*/ uentry usymtab_lookupGlobSafe (cstring p_k)
340 /*@globals internalState@*/ ;
341
342extern /*@only@*/ sRefSet usymtab_aliasedBy (sRef p_s)
343 /*@globals internalState@*/ ;
344
345extern /*@only@*/ sRefSet usymtab_canAlias (sRef p_s)
346 /*@globals internalState@*/ ;
347
348extern void usymtab_clearAlias (sRef p_s)
349 /*@modifies internalState, p_s@*/ ;
350
351extern void usymtab_addMustAlias (sRef p_s, sRef p_al)
352 /*@modifies internalState@*/ ;
353
354extern void usymtab_addForceMustAlias (sRef p_s, sRef p_al)
355 /*@modifies internalState@*/ ;
356
357extern /*@only@*/ cstring usymtab_unparseAliases (void)
358 /*@globals internalState@*/ ;
359
360extern /*@exposed@*/ uentry
361 usymtab_supReturnFileEntry (/*@only@*/ uentry p_e)
362 /*@modifies internalState@*/ ;
363
364extern bool usymtab_isAltProbablyDeepNull (sRef p_s)
365 /*@globals internalState@*/ ;
366
367extern bool usymtab_existsReal (cstring p_k)
368 /*@globals internalState@*/ ;
369
370extern /*@only@*/ sRefSet usymtab_allAliases (sRef p_s)
371 /*@globals internalState@*/ ;
372
373extern void usymtab_exportLocal (void)
374 /*@modifies internalState@*/ ;
375
376extern 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
393extern /*@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
399extern 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
git-cvsimport mirror of splint
This page took 0.114783 seconds and 5 git commands to generate.