]> 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
Added manual files
[splint.git] / src / Headers / usymtab.h
CommitLineData
885824d3 1/*
28bf4b0b 2** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2001.
885824d3 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
28bf4b0b 22typedef struct { int level; int index; } *refentry;
885824d3 23typedef /*@only@*/ refentry o_refentry;
24typedef o_refentry *refTable;
25
28bf4b0b 26struct s_usymtab
885824d3 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;
28bf4b0b 35 /*@null@*/ /*@only@*/ cstringTable htable; /* for the global environment */
885824d3 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@*/ ;
28bf4b0b 94
885824d3 95extern /*@observer@*/ uentry usymtab_lookup (cstring p_k)
96 /*@globals internalState@*/ ;
28bf4b0b 97
885824d3 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
28bf4b0b 116extern bool usymtab_isDefinitelyNull (sRef p_s)
885824d3 117 /*@globals internalState@*/ ;
28bf4b0b 118extern bool usymtab_isDefinitelyNullDeep (sRef p_s)
885824d3 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)
28bf4b0b 188 /*@globals internalState@*/ /*@modifies nothing@*/ ;
189
885824d3 190extern bool usymtab_matchForwardStruct (usymId p_u1, usymId p_u2)
28bf4b0b 191 /*@globals internalState@*/ ;
885824d3 192
193extern bool usymtab_existsEnumTag (cstring p_k)
194 /*@globals internalState@*/ ;
195extern bool usymtab_existsUnionTag (cstring p_k)
196 /*@globals internalState@*/ ;
197extern bool usymtab_existsStructTag (cstring p_k)
198 /*@globals internalState@*/ ;
199
200extern usymId usymId_fromInt (int p_i) /*@*/ ;
201# define usymId_fromInt(i) ((usymId)(i))
202
203extern bool usymId_isInvalid (usymId p_u) /*@*/ ;
204# define usymId_isInvalid(u) ((u) == USYMIDINVALID)
205
206extern bool usymId_isValid (usymId p_u) /*@*/ ;
207# define usymId_isValid(u) ((u) != USYMIDINVALID)
208
209extern bool typeId_isInvalid (typeId p_u) /*@*/ ;
210# define typeId_isInvalid(u) ((u) == typeId_invalid)
211
212extern bool typeId_isValid (typeId p_u) /*@*/ ;
213# define typeId_isValid(u) ((u) != typeId_invalid)
214
215extern bool typeId_equal (typeId p_u1, typeId p_u2) /*@*/ ;
216# define typeId_equal(u1,u2) ((u1) == (u2))
217
218extern typeId typeId_fromInt (int p_i);
219# define typeId_fromInt(i) ((typeId)(i))
220
221/*@iter usymtab_entries (sef usymtab u, yield exposed uentry el); @*/
222# define usymtab_entries(x, m_i) \
223 { int m_ind; \
224 if (usymtab_isDefined (x)) \
225 for (m_ind = 0; m_ind < (x)->nentries; m_ind++) \
226 { uentry m_i = (x)->entries[m_ind];
227
228# define end_usymtab_entries }}
229
230extern /*@unused@*/ void usymtab_displayAllUses (void)
231 /*@globals internalState@*/
232 /*@modifies *g_msgstream@*/ ;
233
234extern /*@unused@*/ void usymtab_printOut (void)
235 /*@globals internalState@*/
236 /*@modifies *g_msgstream@*/ ;
237
238extern /*@unused@*/ void usymtab_printAll (void)
239 /*@globals internalState@*/
240 /*@modifies *g_msgstream@*/ ;
241
242extern void usymtab_enterScope (void)
243 /*@modifies internalState;@*/ ;
244extern void usymtab_enterFunctionScope (uentry p_fcn)
245 /*@modifies internalState;@*/ ;
246extern void usymtab_quietExitScope (fileloc p_loc)
247 /*@modifies internalState;@*/ ;
248extern void usymtab_exitScope (exprNode p_expr) /*@modifies internalState@*/ ;
249extern void usymtab_addGuards (guardSet p_guards) /*@modifies internalState@*/ ;
250extern void usymtab_setExitCode (exitkind p_ex) /*@modifies internalState@*/ ;
251extern void usymtab_exitFile (void) /*@modifies internalState@*/ ;
252extern void usymtab_enterFile (void) /*@modifies internalState@*/ ;
253
254extern /*@observer@*/ uentry usymtab_lookupEnumTag (cstring p_k)
255 /*@globals internalState@*/ ;
256
257extern usymId usymtab_convertId (usymId p_uid) /*@globals internalState@*/ ;
258extern void usymtab_initMod (void) /*@modifies internalState@*/ ;
259extern void usymtab_initBool (void) /*@modifies internalState@*/ ;
28bf4b0b 260extern void usymtab_initGlobalMarker (void) /*@modifies internalState@*/ ;
885824d3 261
262extern void usymtab_exportHeader (void)
263 /*@modifies internalState@*/ ;
264
265extern ctype usymtab_structFieldsType (uentryList p_f)
266 /*@globals internalState@*/ ;
267
268extern ctype usymtab_unionFieldsType (uentryList p_f)
269 /*@globals internalState@*/ ;
270
271extern ctype usymtab_enumEnumNameListType (enumNameList p_f)
272 /*@globals internalState@*/ ;
273
28bf4b0b 274extern /*@exposed@*/ uentry usymtab_getTypeEntrySafe (typeId p_uid)
885824d3 275 /*@globals internalState@*/ ;
276
277extern void usymtab_popOrBranch (exprNode p_pred, exprNode p_expr)
278 /*@modifies internalState@*/ ;
279extern void usymtab_popAndBranch (exprNode p_pred, exprNode p_expr)
280 /*@modifies internalState@*/ ;
281
282extern void usymtab_trueBranch (/*@only@*/ guardSet p_guards)
283 /*@modifies internalState@*/ ;
284extern void usymtab_altBranch (/*@only@*/ guardSet p_guards)
285 /*@modifies internalState@*/ ;
286
287extern void usymtab_popTrueBranch (exprNode p_pred, exprNode p_expr, clause p_cl)
288 /*@modifies internalState@*/ ;
28bf4b0b 289
885824d3 290extern void
291 usymtab_popTrueExecBranch (exprNode p_pred, exprNode p_expr, clause p_cl)
292 /*@modifies internalState@*/ ;
293
294extern void
295 usymtab_popBranches (exprNode p_pred, exprNode p_tbranch, exprNode p_fbranch,
296 bool p_isOpt, clause p_cl)
297 /*@modifies internalState@*/ ;
298
299extern void usymtab_unguard (sRef p_s) /*@modifies internalState@*/ ;
300extern bool usymtab_isGuarded (sRef p_s) /*@globals internalState@*/ ;
301extern void usymtab_printGuards (void) /*@globals internalState@*/ /*@modifies *g_msgstream@*/ ;
302extern void usymtab_quietPlainExitScope (void) /*@modifies internalState@*/ ;
303extern void usymtab_printComplete (void) /*@globals internalState@*/ /*@modifies *stdout@*/ ;
304
305# ifndef NOLCL
306extern bool usymtab_existsGlobEither (cstring p_k) /*@globals internalState@*/ ;
307# endif
308
28bf4b0b 309extern bool usymtab_isBoolType (typeId p_uid) /*@globals internalState@*/ ;
310extern /*@only@*/ cstring usymtab_getTypeEntryName (typeId p_uid)
885824d3 311 /*@globals internalState@*/ ;
28bf4b0b 312extern /*@exposed@*/ uentry usymtab_getTypeEntry (typeId p_uid)
885824d3 313 /*@globals internalState@*/ ;
314
28bf4b0b 315extern typeId
885824d3 316 usymtab_supAbstractTypeEntry (/*@only@*/ uentry p_e, bool p_dodef)
317 /*@modifies internalState, p_e@*/ ;
318extern ctype usymtab_supForwardTypeEntry (/*@only@*/ uentry p_e)
319 /*@modifies internalState, p_e@*/ ;
320
321extern /*@exposed@*/ uentry
322 usymtab_supGlobalEntryReturn (/*@only@*/ uentry p_e)
323 /*@modifies internalState, p_e@*/ ;
324
325extern /*@exposed@*/ uentry
326 usymtab_supEntrySrefReturn (/*@only@*/ uentry p_e)
327 /*@modifies internalState, p_e@*/ ;
328
329extern int uentry_directParamNo (uentry p_ue)
330 /*@globals internalState@*/ ;
331
332extern bool usymtab_newCase (exprNode p_pred, exprNode p_last)
333 /*@modifies internalState@*/ ;
334
335extern void usymtab_switchBranch (exprNode p_s)
336 /*@modifies internalState@*/ ;
337
338extern /*@only@*/ cstring usymtab_unparseStack (void)
339 /*@globals internalState@*/ ;
340extern void usymtab_exitSwitch (exprNode p_sw, bool p_allpaths)
341 /*@modifies internalState@*/ ;
342
343extern /*@observer@*/ uentry usymtab_lookupGlobSafe (cstring p_k)
344 /*@globals internalState@*/ ;
345
346extern /*@only@*/ sRefSet usymtab_aliasedBy (sRef p_s)
347 /*@globals internalState@*/ ;
348
349extern /*@only@*/ sRefSet usymtab_canAlias (sRef p_s)
350 /*@globals internalState@*/ ;
351
352extern void usymtab_clearAlias (sRef p_s)
353 /*@modifies internalState, p_s@*/ ;
354
28bf4b0b 355extern void usymtab_addMustAlias (/*@exposed@*/ sRef p_s, /*@exposed@*/ sRef p_al)
885824d3 356 /*@modifies internalState@*/ ;
357
28bf4b0b 358extern void usymtab_addForceMustAlias (/*@exposed@*/ sRef p_s, /*@exposed@*/ sRef p_al)
885824d3 359 /*@modifies internalState@*/ ;
360
361extern /*@only@*/ cstring usymtab_unparseAliases (void)
362 /*@globals internalState@*/ ;
363
364extern /*@exposed@*/ uentry
365 usymtab_supReturnFileEntry (/*@only@*/ uentry p_e)
366 /*@modifies internalState@*/ ;
367
28bf4b0b 368extern bool usymtab_isAltDefinitelyNullDeep (sRef p_s)
885824d3 369 /*@globals internalState@*/ ;
370
371extern bool usymtab_existsReal (cstring p_k)
372 /*@globals internalState@*/ ;
373
374extern /*@only@*/ sRefSet usymtab_allAliases (sRef p_s)
375 /*@globals internalState@*/ ;
376
377extern void usymtab_exportLocal (void)
378 /*@modifies internalState@*/ ;
379
380extern void usymtab_popCaseBranch (void)
381 /*@modifies internalState@*/ ;
382
383/* special scopes */
384
385/*@constant int globScope;@*/
386# define globScope 0 /* global variables */
387
388/*@constant int fileScope;@*/
389# define fileScope 1 /* file-level static variables */
390
391/*@constant int paramsScope;@*/
392# define paramsScope 2 /* function parameters */
393
394/*@constant int functionScope;@*/
395# define functionScope 3
396
397extern /*@falsenull@*/ bool usymtab_isDefined (usymtab p_u) /*@*/ ;
398
399/*@constant null usymtab usymtab_undefined; @*/
400# define usymtab_undefined ((usymtab)NULL)
401# define usymtab_isDefined(u) ((u) != usymtab_undefined)
402
403extern void usymtab_checkDistinctName (uentry p_e, int p_scope)
404 /*@globals internalState@*/
405 /*@modifies *g_msgstream, p_e@*/ ;
406
28bf4b0b 407extern /*@exposed@*/ sRef usymtab_lookupGlobalMarker (void) /*@globals internalState@*/ ;
408
409extern int usymtab_getCurrentDepth (void) /*@globals internalState@*/ ;
410
885824d3 411# else
412# error "Multiple include"
413# endif
414
415
416
git-cvsimport mirror of splint
This page took 0.322148 seconds and 5 git commands to generate.