]> andersk Git - splint.git/blame - src/Headers/usymtab-branch.h
andersk / splint.git / blame
? search:
summary | shortlog | log | commit | commitdiff | tree
blob | blame (incremental) | history | HEAD
Merged code tree with Dave Evans's version. Many changes to numberous to list....
[splint.git] / src / Headers / usymtab-branch.h
CommitLineData
28bf4b0b 1/*
2** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2001.
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 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
36struct _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
64extern void usymtab_printTypes (void)
65 /*@globals internalState@*/
66 /*@modifies g_msgstream@*/ ;
67
68extern void usymtab_setMustBreak (void) /*@modifies internalState@*/ ;
69
70extern bool usymtab_inGlobalScope (void) /*@globals internalState@*/ ;
71extern bool usymtab_inFunctionScope (void) /*@globals internalState@*/ ;
72extern bool usymtab_inFileScope (void) /*@globals internalState@*/ ;
73extern void usymtab_checkFinalScope (bool p_isReturn)
74 /*@globals internalState@*/
75 /*@modifies *g_msgstream@*/ ;
76
77extern void usymtab_allUsed (void)
78 /*@globals internalState@*/
79 /*@modifies *g_msgstream@*/ ;
80
81extern void usymtab_allDefined (void)
82 /*@globals internalState@*/
83 /*@modifies *g_msgstream@*/ ;
84
85extern void usymtab_prepareDump (void)
86 /*@modifies internalState@*/ ;
87
88extern void usymtab_dump (FILE *p_fout)
89 /*@globals internalState@*/
90 /*@modifies *p_fout@*/ ;
91
92
93extern void usymtab_load (FILE *p_f) /*@modifies p_f, internalState@*/ ;
94
95extern /*@exposed@*/ /*@dependent@*/ uentry
96 usymtab_getRefQuiet (int p_level, usymId p_index)
97 /*@globals internalState@*/ ;
98
99extern void usymtab_printLocal (void)
100 /*@globals internalState@*/
101 /*@modifies stdout@*/ ;
102
103extern /*@exposed@*/ /*@dependent@*/ uentry usymtab_getParam (int p_paramno)
104 /*@globals internalState@*/;
105extern void usymtab_free (void) /*@modifies internalState@*/ ;
106extern bool usymtab_inDeepScope (void) /*@globals internalState@*/ ;
107
108extern /*@exposed@*/ uentry usymtab_lookupExpose (cstring p_k)
109 /*@globals internalState@*/ ;
110
111extern /*@observer@*/ uentry usymtab_lookup (cstring p_k)
112 /*@globals internalState@*/ ;
113
114# define usymtab_lookup(s) (usymtab_lookupExpose (s))
115
116extern /*@observer@*/ uentry usymtab_lookupGlob (cstring p_k)
117 /*@globals internalState@*/ ;
118extern /*@exposed@*/ uentry usymtab_lookupExposeGlob (cstring p_k)
119 /*@globals internalState@*/ ;
120extern /*@observer@*/ uentry usymtab_lookupUnionTag (cstring p_k)
121 /*@globals internalState@*/ ;
122extern /*@observer@*/ uentry usymtab_lookupStructTag (cstring p_k)
123 /*@globals internalState@*/ ;
124extern /*@observer@*/ uentry usymtab_lookupEither (cstring p_k)
125 /*@globals internalState@*/ ;
126
127# ifndef NOLCL
128extern ctype usymtab_lookupType (cstring p_k)
129 /*@globals internalState@*/ ;
130# endif
131
132extern bool usymtab_isDefinitelyNull (sRef p_s)
133 /*@globals internalState@*/ ;
134extern bool usymtab_isDefinitelyNullDeep (sRef p_s)
135 /*@globals internalState@*/ ;
136
137# ifndef NOLCL
138extern usymId usymtab_supExposedTypeEntry (/*@only@*/ uentry p_e, bool p_dodef)
139 /*@modifies internalState, p_e@*/ ;
140# endif
141
142extern ctype usymtab_supTypeEntry (/*@only@*/ uentry p_e)
143 /*@modifies internalState, p_e@*/ ;
144
145extern /*@exposed@*/ uentry usymtab_supReturnTypeEntry (/*@only@*/ uentry p_e)
146 /*@modifies internalState@*/ ;
147
148extern /*@observer@*/ uentry usymtab_lookupSafe (cstring p_k)
149 /*@globals internalState@*/ ;
150
151extern /*@observer@*/ uentry usymtab_getGlobalEntry (usymId p_uid)
152 /*@globals internalState@*/ ;
153
154extern bool usymtab_exists (cstring p_k)
155 /*@globals internalState@*/ ;
156
157# ifndef NOLCL
158extern bool usymtab_existsVar (cstring p_k)
159 /*@globals internalState@*/ ;
160# endif
161
162extern bool usymtab_existsGlob (cstring p_k)
163 /*@globals internalState@*/ ;
164
165extern bool usymtab_existsType (cstring p_k)
166 /*@globals internalState@*/ ;
167
168# ifndef NOLCL
169extern bool usymtab_existsEither (cstring p_k)
170 /*@globals internalState@*/ ;
171# endif
172
173extern bool usymtab_existsTypeEither (cstring p_k)
174 /*@globals internalState@*/ ;
175
176extern usymId usymtab_getId (cstring p_k) /*@globals internalState@*/ ;
177extern usymId usymtab_getTypeId (cstring p_k) /*@globals internalState@*/ ;
178
179extern void usymtab_supEntry (/*@only@*/ uentry p_e)
180 /*@modifies internalState, p_e@*/ ;
181
182# ifndef NOLCL
183extern void usymtab_replaceEntry (/*@only@*/ uentry p_s)
184 /*@modifies internalState, p_s@*/ ;
185# endif
186
187extern void usymtab_supEntrySref (/*@only@*/ uentry p_e)
188 /*@modifies internalState, p_e@*/ ;
189
190extern void usymtab_supGlobalEntry (/*@only@*/ uentry p_e)
191 /*@modifies internalState@*/ ;
192
193extern void usymtab_addGlobalEntry (/*@only@*/ uentry p_e)
194 /*@modifies internalState, p_e@*/ ;
195
196extern /*@exposed@*/ uentry
197 usymtab_supEntryReturn (/*@only@*/ uentry p_e)
198 /*@modifies internalState, p_e@*/ ;
199
200extern usymId usymtab_addEntry (/*@only@*/ uentry p_e)
201 /*@modifies internalState, p_e@*/ ;
202
203extern ctype usymtab_lookupAbstractType (cstring p_k)
204 /*@globals internalState@*/ /*@modifies nothing@*/ ;
205
206extern bool usymtab_matchForwardStruct (usymId p_u1, usymId p_u2)
207 /*@globals internalState@*/ ;
208
209extern bool usymtab_existsEnumTag (cstring p_k)
210 /*@globals internalState@*/ ;
211extern bool usymtab_existsUnionTag (cstring p_k)
212 /*@globals internalState@*/ ;
213extern bool usymtab_existsStructTag (cstring p_k)
214 /*@globals internalState@*/ ;
215
216extern usymId usymId_fromInt (int p_i) /*@*/ ;
217# define usymId_fromInt(i) ((usymId)(i))
218
219extern bool usymId_isInvalid (usymId p_u) /*@*/ ;
220# define usymId_isInvalid(u) ((u) == USYMIDINVALID)
221
222extern bool usymId_isValid (usymId p_u) /*@*/ ;
223# define usymId_isValid(u) ((u) != USYMIDINVALID)
224
225extern bool typeId_isInvalid (typeId p_u) /*@*/ ;
226# define typeId_isInvalid(u) ((u) == typeId_invalid)
227
228extern bool typeId_isValid (typeId p_u) /*@*/ ;
229# define typeId_isValid(u) ((u) != typeId_invalid)
230
231extern bool typeId_equal (typeId p_u1, typeId p_u2) /*@*/ ;
232# define typeId_equal(u1,u2) ((u1) == (u2))
233
234extern typeId typeId_fromInt (int p_i);
235# define typeId_fromInt(i) ((typeId)(i))
236
237/*@iter usymtab_entries (sef usymtab u, yield exposed uentry el); @*/
238# define usymtab_entries(x, m_i) \
239 { int m_ind; \
240 if (usymtab_isDefined (x)) \
241 for (m_ind = 0; m_ind < (x)->nentries; m_ind++) \
242 { uentry m_i = (x)->entries[m_ind];
243
244# define end_usymtab_entries }}
245
246extern /*@unused@*/ void usymtab_displayAllUses (void)
247 /*@globals internalState@*/
248 /*@modifies *g_msgstream@*/ ;
249
250extern /*@unused@*/ void usymtab_printOut (void)
251 /*@globals internalState@*/
252 /*@modifies *g_msgstream@*/ ;
253
254extern /*@unused@*/ void usymtab_printAll (void)
255 /*@globals internalState@*/
256 /*@modifies *g_msgstream@*/ ;
257
258extern void usymtab_enterScope (void)
259 /*@modifies internalState;@*/ ;
260extern void usymtab_enterFunctionScope (uentry p_fcn)
261 /*@modifies internalState;@*/ ;
262extern void usymtab_quietExitScope (fileloc p_loc)
263 /*@modifies internalState;@*/ ;
264extern void usymtab_exitScope (exprNode p_expr) /*@modifies internalState@*/ ;
265extern void usymtab_addGuards (guardSet p_guards) /*@modifies internalState@*/ ;
266extern void usymtab_setExitCode (exitkind p_ex) /*@modifies internalState@*/ ;
267extern void usymtab_exitFile (void) /*@modifies internalState@*/ ;
268extern void usymtab_enterFile (void) /*@modifies internalState@*/ ;
269
270extern /*@observer@*/ uentry usymtab_lookupEnumTag (cstring p_k)
271 /*@globals internalState@*/ ;
272
273extern usymId usymtab_convertId (usymId p_uid) /*@globals internalState@*/ ;
274extern void usymtab_initMod (void) /*@modifies internalState@*/ ;
275extern void usymtab_initBool (void) /*@modifies internalState@*/ ;
276extern void usymtab_initGlobalMarker (void) /*@modifies internalState@*/ ;
277
278extern void usymtab_exportHeader (void)
279 /*@modifies internalState@*/ ;
280
281extern ctype usymtab_structFieldsType (uentryList p_f)
282 /*@globals internalState@*/ ;
283
284extern ctype usymtab_unionFieldsType (uentryList p_f)
285 /*@globals internalState@*/ ;
286
287extern ctype usymtab_enumEnumNameListType (enumNameList p_f)
288 /*@globals internalState@*/ ;
289
290extern /*@exposed@*/ uentry usymtab_getTypeEntrySafe (usymId p_uid)
291 /*@globals internalState@*/ ;
292
293extern void usymtab_popOrBranch (exprNode p_pred, exprNode p_expr)
294 /*@modifies internalState@*/ ;
295extern void usymtab_popAndBranch (exprNode p_pred, exprNode p_expr)
296 /*@modifies internalState@*/ ;
297
298extern void usymtab_trueBranch (/*@only@*/ guardSet p_guards)
299 /*@modifies internalState@*/ ;
300extern void usymtab_altBranch (/*@only@*/ guardSet p_guards)
301 /*@modifies internalState@*/ ;
302
303extern void usymtab_popTrueBranch (exprNode p_pred, exprNode p_expr, clause p_cl)
304 /*@modifies internalState@*/ ;
305
306extern void
307 usymtab_popTrueExecBranch (exprNode p_pred, exprNode p_expr, clause p_cl)
308 /*@modifies internalState@*/ ;
309
310extern void
311 usymtab_popBranches (exprNode p_pred, exprNode p_tbranch, exprNode p_fbranch,
312 bool p_isOpt, clause p_cl)
313 /*@modifies internalState@*/ ;
314
315extern void usymtab_unguard (sRef p_s) /*@modifies internalState@*/ ;
316extern bool usymtab_isGuarded (sRef p_s) /*@globals internalState@*/ ;
317extern void usymtab_printGuards (void) /*@globals internalState@*/ /*@modifies *g_msgstream@*/ ;
318extern void usymtab_quietPlainExitScope (void) /*@modifies internalState@*/ ;
319extern void usymtab_printComplete (void) /*@globals internalState@*/ /*@modifies *stdout@*/ ;
320
321# ifndef NOLCL
322extern bool usymtab_existsGlobEither (cstring p_k) /*@globals internalState@*/ ;
323# endif
324
325extern bool usymtab_isBoolType (usymId p_uid) /*@globals internalState@*/ ;
326extern /*@only@*/ cstring
327 usymtab_getTypeEntryName (usymId p_uid)
328 /*@globals internalState@*/ ;
329extern /*@exposed@*/ uentry usymtab_getTypeEntry (usymId p_uid)
330 /*@globals internalState@*/ ;
331
332extern usymId
333 usymtab_supAbstractTypeEntry (/*@only@*/ uentry p_e, bool p_dodef)
334 /*@modifies internalState, p_e@*/ ;
335extern ctype usymtab_supForwardTypeEntry (/*@only@*/ uentry p_e)
336 /*@modifies internalState, p_e@*/ ;
337
338extern /*@exposed@*/ uentry
339 usymtab_supGlobalEntryReturn (/*@only@*/ uentry p_e)
340 /*@modifies internalState, p_e@*/ ;
341
342extern /*@exposed@*/ uentry
343 usymtab_supEntrySrefReturn (/*@only@*/ uentry p_e)
344 /*@modifies internalState, p_e@*/ ;
345
346extern int uentry_directParamNo (uentry p_ue)
347 /*@globals internalState@*/ ;
348
349extern bool usymtab_newCase (exprNode p_pred, exprNode p_last)
350 /*@modifies internalState@*/ ;
351
352extern void usymtab_switchBranch (exprNode p_s)
353 /*@modifies internalState@*/ ;
354
355extern /*@only@*/ cstring usymtab_unparseStack (void)
356 /*@globals internalState@*/ ;
357extern void usymtab_exitSwitch (exprNode p_sw, bool p_allpaths)
358 /*@modifies internalState@*/ ;
359
360extern /*@observer@*/ uentry usymtab_lookupGlobSafe (cstring p_k)
361 /*@globals internalState@*/ ;
362
363extern /*@only@*/ sRefSet usymtab_aliasedBy (sRef p_s)
364 /*@globals internalState@*/ ;
365
366extern /*@only@*/ sRefSet usymtab_canAlias (sRef p_s)
367 /*@globals internalState@*/ ;
368
369extern void usymtab_clearAlias (sRef p_s)
370 /*@modifies internalState, p_s@*/ ;
371
372extern void usymtab_addMustAlias (/*@exposed@*/ sRef p_s, /*@exposed@*/ sRef p_al)
373 /*@modifies internalState@*/ ;
374
375extern void usymtab_addForceMustAlias (/*@exposed@*/ sRef p_s, /*@exposed@*/ sRef p_al)
376 /*@modifies internalState@*/ ;
377
378extern /*@only@*/ cstring usymtab_unparseAliases (void)
379 /*@globals internalState@*/ ;
380
381extern /*@exposed@*/ uentry
382 usymtab_supReturnFileEntry (/*@only@*/ uentry p_e)
383 /*@modifies internalState@*/ ;
384
385extern bool usymtab_isAltDefinitelyNullDeep (sRef p_s)
386 /*@globals internalState@*/ ;
387
388extern bool usymtab_existsReal (cstring p_k)
389 /*@globals internalState@*/ ;
390
391extern /*@only@*/ sRefSet usymtab_allAliases (sRef p_s)
392 /*@globals internalState@*/ ;
393
394extern void usymtab_exportLocal (void)
395 /*@modifies internalState@*/ ;
396
397extern void usymtab_popCaseBranch (void)
398 /*@modifies internalState@*/ ;
399
400/* special scopes */
401
402/*@constant int invalidScope;@*/
403# define invalidScope -1 /* invalid scope */
404
405/*@constant int globScope;@*/
406# define globScope 0 /* global variables */
407
408/*@constant int fileScope;@*/
409# define fileScope 1 /* file-level static variables */
410
411/*@constant int paramsScope;@*/
412# define paramsScope 2 /* function parameters */
413
414/*@constant int functionScope;@*/
415# define functionScope 3
416
417extern /*@falsenull@*/ bool usymtab_isDefined (usymtab p_u) /*@*/ ;
418
419/*@constant null usymtab usymtab_undefined; @*/
420# define usymtab_undefined ((usymtab)NULL)
421# define usymtab_isDefined(u) ((u) != usymtab_undefined)
422
423extern void usymtab_checkDistinctName (uentry p_e, int p_scope)
424 /*@globals internalState@*/
425 /*@modifies *g_msgstream, p_e@*/ ;
426
427extern /*@exposed@*/ sRef usymtab_lookupGlobalMarker (void) /*@globals internalState@*/ ;
428
429extern int usymtab_getCurrentDepth (void) /*@globals internalState@*/ ;
430
431# else
432# error "Multiple include"
433# endif
434
435
436
git-cvsimport mirror of splint
This page took 0.10973 seconds and 5 git commands to generate.