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