]> 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
Periodic commit
[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
a0a162cd 11#include "environmentTable.h"
885824d3 12
13/*@constant null usymtab GLOBAL_ENV; @*/
14# define GLOBAL_ENV usymtab_undefined
15
16typedef enum {
17 US_GLOBAL,
18 US_NORMAL,
19 US_TBRANCH, US_FBRANCH,
20 US_CBRANCH, US_SWITCH
21} uskind;
22
23typedef struct _refentry { int level; int index; } *refentry;
24typedef /*@only@*/ refentry o_refentry;
25typedef o_refentry *refTable;
26
27struct _usymtab
28{
29 uskind kind;
30 int nentries;
31 int nspace;
32 int lexlevel;
33 bool mustBreak;
34 exitkind exitCode;
35 /*@reldef@*/ /*@only@*/ o_uentry *entries;
36 /*@null@*/ /*@only@*/ hashTable htable; /* for the global environment */
37 /*@null@*/ /*@only@*/ refTable reftable; /* for branched environments */
38 /*@only@*/ guardSet guards; /* guarded references (not null) */
39 aliasTable aliases;
40 /*@owned@*/ usymtab env;
a0a162cd 41 environmentTable environment;
885824d3 42} ;
43
44/*
45** rep invariant:
46**
47** (left as exercise to reader) ;)
48*/
49
50extern void usymtab_printTypes (void)
51 /*@globals internalState@*/
52 /*@modifies g_msgstream@*/ ;
53
54extern void usymtab_setMustBreak (void) /*@modifies internalState@*/ ;
55
56extern bool usymtab_inGlobalScope (void) /*@globals internalState@*/ ;
57extern bool usymtab_inFunctionScope (void) /*@globals internalState@*/ ;
58extern bool usymtab_inFileScope (void) /*@globals internalState@*/ ;
59extern void usymtab_checkFinalScope (bool p_isReturn)
60 /*@globals internalState@*/
61 /*@modifies *g_msgstream@*/ ;
62
63extern void usymtab_allUsed (void)
64 /*@globals internalState@*/
65 /*@modifies *g_msgstream@*/ ;
66
67extern void usymtab_allDefined (void)
68 /*@globals internalState@*/
69 /*@modifies *g_msgstream@*/ ;
70
71extern void usymtab_prepareDump (void)
72 /*@modifies internalState@*/ ;
73
74extern void usymtab_dump (FILE *p_fout)
75 /*@globals internalState@*/
76 /*@modifies *p_fout@*/ ;
77
78
79extern void usymtab_load (FILE *p_f) /*@modifies p_f, internalState@*/ ;
80
81extern /*@exposed@*/ /*@dependent@*/ uentry
82 usymtab_getRefQuiet (int p_level, usymId p_index)
83 /*@globals internalState@*/ ;
84
85extern void usymtab_printLocal (void)
86 /*@globals internalState@*/
87 /*@modifies stdout@*/ ;
88
89extern /*@exposed@*/ /*@dependent@*/ uentry usymtab_getParam (int p_paramno)
90 /*@globals internalState@*/;
91extern void usymtab_free (void) /*@modifies internalState@*/ ;
92extern bool usymtab_inDeepScope (void) /*@globals internalState@*/ ;
93
94extern /*@exposed@*/ uentry usymtab_lookupExpose (cstring p_k)
95 /*@globals internalState@*/ ;
96extern /*@observer@*/ uentry usymtab_lookup (cstring p_k)
97 /*@globals internalState@*/ ;
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
111# ifndef NOLCL
112extern ctype usymtab_lookupType (cstring p_k)
113 /*@globals internalState@*/ ;
114# endif
115
116extern bool usymtab_isProbableNull (sRef p_s)
117 /*@globals internalState@*/ ;
118extern bool usymtab_isProbableDeepNull (sRef p_s)
119 /*@globals internalState@*/ ;
120
121# ifndef NOLCL
122extern usymId usymtab_supExposedTypeEntry (/*@only@*/ uentry p_e, bool p_dodef)
123 /*@modifies internalState, p_e@*/ ;
124# endif
125
126extern ctype usymtab_supTypeEntry (/*@only@*/ uentry p_e)
127 /*@modifies internalState, p_e@*/ ;
128
129extern /*@exposed@*/ uentry usymtab_supReturnTypeEntry (/*@only@*/ uentry p_e)
130 /*@modifies internalState@*/ ;
131
132extern /*@observer@*/ uentry usymtab_lookupSafe (cstring p_k)
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
141# ifndef NOLCL
142extern bool usymtab_existsVar (cstring p_k)
143 /*@globals internalState@*/ ;
144# endif
145
146extern bool usymtab_existsGlob (cstring p_k)
147 /*@globals internalState@*/ ;
148
149extern bool usymtab_existsType (cstring p_k)
150 /*@globals internalState@*/ ;
151
152# ifndef NOLCL
153extern bool usymtab_existsEither (cstring p_k)
154 /*@globals internalState@*/ ;
155# endif
156
157extern bool usymtab_existsTypeEither (cstring p_k)
158 /*@globals internalState@*/ ;
159
160extern usymId usymtab_getId (cstring p_k) /*@globals internalState@*/ ;
161extern usymId usymtab_getTypeId (cstring p_k) /*@globals internalState@*/ ;
162
163extern void usymtab_supEntry (/*@only@*/ uentry p_e)
164 /*@modifies internalState, p_e@*/ ;
165
166# ifndef NOLCL
167extern void usymtab_replaceEntry (/*@only@*/ uentry p_s)
168 /*@modifies internalState, p_s@*/ ;
169# endif
170
171extern void usymtab_supEntrySref (/*@only@*/ uentry p_e)
172 /*@modifies internalState, p_e@*/ ;
173
174extern void usymtab_supGlobalEntry (/*@only@*/ uentry p_e)
175 /*@modifies internalState@*/ ;
176
177extern void usymtab_addGlobalEntry (/*@only@*/ uentry p_e)
178 /*@modifies internalState, p_e@*/ ;
179
180extern /*@exposed@*/ uentry
181 usymtab_supEntryReturn (/*@only@*/ uentry p_e)
182 /*@modifies internalState, p_e@*/ ;
183
184extern usymId usymtab_addEntry (/*@only@*/ uentry p_e)
185 /*@modifies internalState, p_e@*/ ;
186
187extern ctype usymtab_lookupAbstractType (cstring p_k)
188 /*@globals internalState@*/ ;
189extern bool usymtab_matchForwardStruct (usymId p_u1, usymId p_u2)
190 /*@globals internalState@*/ ;
191
192extern bool usymtab_existsEnumTag (cstring p_k)
193 /*@globals internalState@*/ ;
194extern bool usymtab_existsUnionTag (cstring p_k)
195 /*@globals internalState@*/ ;
196extern bool usymtab_existsStructTag (cstring p_k)
197 /*@globals internalState@*/ ;
198
199extern usymId usymId_fromInt (int p_i) /*@*/ ;
200# define usymId_fromInt(i) ((usymId)(i))
201
202extern bool usymId_isInvalid (usymId p_u) /*@*/ ;
203# define usymId_isInvalid(u) ((u) == USYMIDINVALID)
204
205extern bool usymId_isValid (usymId p_u) /*@*/ ;
206# define usymId_isValid(u) ((u) != USYMIDINVALID)
207
208extern bool typeId_isInvalid (typeId p_u) /*@*/ ;
209# define typeId_isInvalid(u) ((u) == typeId_invalid)
210
211extern bool typeId_isValid (typeId p_u) /*@*/ ;
212# define typeId_isValid(u) ((u) != typeId_invalid)
213
214extern bool typeId_equal (typeId p_u1, typeId p_u2) /*@*/ ;
215# define typeId_equal(u1,u2) ((u1) == (u2))
216
217extern typeId typeId_fromInt (int p_i);
218# define typeId_fromInt(i) ((typeId)(i))
219
220/*@iter usymtab_entries (sef usymtab u, yield exposed uentry el); @*/
221# define usymtab_entries(x, m_i) \
222 { int m_ind; \
223 if (usymtab_isDefined (x)) \
224 for (m_ind = 0; m_ind < (x)->nentries; m_ind++) \
225 { uentry m_i = (x)->entries[m_ind];
226
227# define end_usymtab_entries }}
228
229extern /*@unused@*/ void usymtab_displayAllUses (void)
230 /*@globals internalState@*/
231 /*@modifies *g_msgstream@*/ ;
232
233extern /*@unused@*/ void usymtab_printOut (void)
234 /*@globals internalState@*/
235 /*@modifies *g_msgstream@*/ ;
236
237extern /*@unused@*/ void usymtab_printAll (void)
238 /*@globals internalState@*/
239 /*@modifies *g_msgstream@*/ ;
240
241extern void usymtab_enterScope (void)
242 /*@modifies internalState;@*/ ;
243extern void usymtab_enterFunctionScope (uentry p_fcn)
244 /*@modifies internalState;@*/ ;
245extern void usymtab_quietExitScope (fileloc p_loc)
246 /*@modifies internalState;@*/ ;
247extern void usymtab_exitScope (exprNode p_expr) /*@modifies internalState@*/ ;
248extern void usymtab_addGuards (guardSet p_guards) /*@modifies internalState@*/ ;
249extern void usymtab_setExitCode (exitkind p_ex) /*@modifies internalState@*/ ;
250extern void usymtab_exitFile (void) /*@modifies internalState@*/ ;
251extern void usymtab_enterFile (void) /*@modifies internalState@*/ ;
252
253extern /*@observer@*/ uentry usymtab_lookupEnumTag (cstring p_k)
254 /*@globals internalState@*/ ;
255
256extern usymId usymtab_convertId (usymId p_uid) /*@globals internalState@*/ ;
257extern void usymtab_initMod (void) /*@modifies internalState@*/ ;
258extern void usymtab_initBool (void) /*@modifies internalState@*/ ;
259
260extern void usymtab_exportHeader (void)
261 /*@modifies internalState@*/ ;
262
263extern ctype usymtab_structFieldsType (uentryList p_f)
264 /*@globals internalState@*/ ;
265
266extern ctype usymtab_unionFieldsType (uentryList p_f)
267 /*@globals internalState@*/ ;
268
269extern ctype usymtab_enumEnumNameListType (enumNameList p_f)
270 /*@globals internalState@*/ ;
271
272extern /*@exposed@*/ uentry usymtab_getTypeEntrySafe (usymId p_uid)
273 /*@globals internalState@*/ ;
274
275extern void usymtab_popOrBranch (exprNode p_pred, exprNode p_expr)
276 /*@modifies internalState@*/ ;
277extern void usymtab_popAndBranch (exprNode p_pred, exprNode p_expr)
278 /*@modifies internalState@*/ ;
279
280extern void usymtab_trueBranch (/*@only@*/ guardSet p_guards)
281 /*@modifies internalState@*/ ;
282extern void usymtab_altBranch (/*@only@*/ guardSet p_guards)
283 /*@modifies internalState@*/ ;
284
285extern void usymtab_popTrueBranch (exprNode p_pred, exprNode p_expr, clause p_cl)
286 /*@modifies internalState@*/ ;
287extern void
288 usymtab_popTrueExecBranch (exprNode p_pred, exprNode p_expr, clause p_cl)
289 /*@modifies internalState@*/ ;
290
291extern void
292 usymtab_popBranches (exprNode p_pred, exprNode p_tbranch, exprNode p_fbranch,
293 bool p_isOpt, clause p_cl)
294 /*@modifies internalState@*/ ;
295
296extern void usymtab_unguard (sRef p_s) /*@modifies internalState@*/ ;
297extern bool usymtab_isGuarded (sRef p_s) /*@globals internalState@*/ ;
298extern void usymtab_printGuards (void) /*@globals internalState@*/ /*@modifies *g_msgstream@*/ ;
299extern void usymtab_quietPlainExitScope (void) /*@modifies internalState@*/ ;
300extern void usymtab_printComplete (void) /*@globals internalState@*/ /*@modifies *stdout@*/ ;
301
302# ifndef NOLCL
303extern bool usymtab_existsGlobEither (cstring p_k) /*@globals internalState@*/ ;
304# endif
305
306extern bool usymtab_isBoolType (usymId p_uid) /*@globals internalState@*/ ;
307extern /*@only@*/ cstring
308 usymtab_getTypeEntryName (usymId p_uid)
309 /*@globals internalState@*/ ;
310extern /*@exposed@*/ uentry usymtab_getTypeEntry (usymId p_uid)
311 /*@globals internalState@*/ ;
312
313extern usymId
314 usymtab_supAbstractTypeEntry (/*@only@*/ uentry p_e, bool p_dodef)
315 /*@modifies internalState, p_e@*/ ;
316extern ctype usymtab_supForwardTypeEntry (/*@only@*/ uentry p_e)
317 /*@modifies internalState, p_e@*/ ;
318
319extern /*@exposed@*/ uentry
320 usymtab_supGlobalEntryReturn (/*@only@*/ uentry p_e)
321 /*@modifies internalState, p_e@*/ ;
322
323extern /*@exposed@*/ uentry
324 usymtab_supEntrySrefReturn (/*@only@*/ uentry p_e)
325 /*@modifies internalState, p_e@*/ ;
326
327extern int uentry_directParamNo (uentry p_ue)
328 /*@globals internalState@*/ ;
329
330extern bool usymtab_newCase (exprNode p_pred, exprNode p_last)
331 /*@modifies internalState@*/ ;
332
333extern void usymtab_switchBranch (exprNode p_s)
334 /*@modifies internalState@*/ ;
335
336extern /*@only@*/ cstring usymtab_unparseStack (void)
337 /*@globals internalState@*/ ;
338extern void usymtab_exitSwitch (exprNode p_sw, bool p_allpaths)
339 /*@modifies internalState@*/ ;
340
341extern /*@observer@*/ uentry usymtab_lookupGlobSafe (cstring p_k)
342 /*@globals internalState@*/ ;
343
344extern /*@only@*/ sRefSet usymtab_aliasedBy (sRef p_s)
345 /*@globals internalState@*/ ;
346
347extern /*@only@*/ sRefSet usymtab_canAlias (sRef p_s)
348 /*@globals internalState@*/ ;
349
350extern void usymtab_clearAlias (sRef p_s)
351 /*@modifies internalState, p_s@*/ ;
352
353extern void usymtab_addMustAlias (sRef p_s, sRef p_al)
354 /*@modifies internalState@*/ ;
355
356extern void usymtab_addForceMustAlias (sRef p_s, sRef p_al)
357 /*@modifies internalState@*/ ;
358
359extern /*@only@*/ cstring usymtab_unparseAliases (void)
360 /*@globals internalState@*/ ;
361
362extern /*@exposed@*/ uentry
363 usymtab_supReturnFileEntry (/*@only@*/ uentry p_e)
364 /*@modifies internalState@*/ ;
365
366extern bool usymtab_isAltProbablyDeepNull (sRef p_s)
367 /*@globals internalState@*/ ;
368
369extern bool usymtab_existsReal (cstring p_k)
370 /*@globals internalState@*/ ;
371
372extern /*@only@*/ sRefSet usymtab_allAliases (sRef p_s)
373 /*@globals internalState@*/ ;
374
375extern void usymtab_exportLocal (void)
376 /*@modifies internalState@*/ ;
377
378extern void usymtab_popCaseBranch (void)
379 /*@modifies internalState@*/ ;
380
381/* special scopes */
382
383/*@constant int globScope;@*/
384# define globScope 0 /* global variables */
385
386/*@constant int fileScope;@*/
387# define fileScope 1 /* file-level static variables */
388
389/*@constant int paramsScope;@*/
390# define paramsScope 2 /* function parameters */
391
392/*@constant int functionScope;@*/
393# define functionScope 3
394
395extern /*@falsenull@*/ bool usymtab_isDefined (usymtab p_u) /*@*/ ;
396
397/*@constant null usymtab usymtab_undefined; @*/
398# define usymtab_undefined ((usymtab)NULL)
399# define usymtab_isDefined(u) ((u) != usymtab_undefined)
400
401extern void usymtab_checkDistinctName (uentry p_e, int p_scope)
402 /*@globals internalState@*/
403 /*@modifies *g_msgstream, p_e@*/ ;
404
4cccc6ad 405
406 /*DRL add 9/4/00 */
407extern
408extern void usymtab_testInRange (sRef p_s, int p_index) /*@modifies internalState;@*/;
409extern void usymtab_postopVar (sRef p_sr) /*@modifies internalState;@*/ ;
410
411
885824d3 412# else
413# error "Multiple include"
414# endif
415
416
417
git-cvsimport mirror of splint
This page took 0.129594 seconds and 5 git commands to generate.