]> andersk Git - splint.git/blame - src/Headers/uentry.h
andersk / splint.git / blame
? search:
summary | shortlog | log | commit | commitdiff | tree
blob | blame (incremental) | history | HEAD
Removed .lh .lcs .lcd files in test directory from distribution tar ball as suggested...
[splint.git] / src / Headers / uentry.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# ifndef UENTRY_H
6# define UENTRY_H
7# define CENTRY_H
8
9/*
10** universal symbol table entry
11** (combines old llentry, centry, and ttentry)
12*/
13
14/*
15** vkind --- need to fix value for consistency in dump files
16*/
17
28bf4b0b 18typedef struct
885824d3 19{
b9904f57 20 typeIdSet access;
5e211f69 21 bool macro;
885824d3 22} *ucinfo;
23
24typedef enum
25{
26 VKSPEC = 0, VKNORMAL,
27 VKPARAM, VKYIELDPARAM, VKREFYIELDPARAM,
28 VKRETPARAM, VKREFPARAM,
29 VKSEFPARAM, VKREFSEFPARAM,
30 VKSEFRETPARAM, VKREFSEFRETPARAM,
31 VKEXPMACRO
32} vkind;
33
34/*@constant vkind VKFIRST;@*/
35# define VKFIRST VKSPEC
36
37/*@constant vkind VKLAST;@*/
38# define VKLAST VKEXPMACRO
39
40typedef enum
41{
42 CH_UNKNOWN,
43 CH_UNCHECKED,
44 CH_CHECKED,
45 CH_CHECKMOD,
46 CH_CHECKEDSTRICT
47} chkind;
48
1ac6313d 49/* start modifications */
28bf4b0b 50typedef enum {
1ac6313d 51 BB_POSSIBLYNULLTERMINATED, /* buffer is possibly nullterm(can't decide statically) */
52 BB_NULLTERMINATED, /*buffer is known to be nullterminated */
53 BB_NOTNULLTERMINATED /* buffer is known to be not nullterm */
54} bbufstate;
55
abd7f895 56typedef /*@null@*/ struct s_bbufinfo {
1ac6313d 57 bbufstate bufstate; /* state of the buffer */
58 int size; /* size of the buffer allocated */
59 int len; /* len of the buffer VALID ONLY IF state is NULLTERM */
60} *bbufinfo ;
61
28bf4b0b 62typedef struct
885824d3 63{
64 vkind kind; /* kind (parameter, specified) */
65 chkind checked; /* how is it checked */
66 sstate defstate;
67 nstate nullstate;
1ac6313d 68 bbufinfo bufinfo; /* is valid only if the entry is a variable and (a pointer
69 or array) */
885824d3 70} *uvinfo ;
1ac6313d 71/* end modifications */
885824d3 72
28bf4b0b 73typedef struct
885824d3 74{
75 ynm abs;
76 ynm mut;
77 ctype type;
78} *udinfo ;
79
80/* information for specified functions */
81
82typedef enum
83{
84 SPC_NONE,
85 SPC_PRINTFLIKE,
86 SPC_SCANFLIKE,
87 SPC_MESSAGELIKE,
88 SPC_LAST
89} specCode;
90
28bf4b0b 91typedef struct
885824d3 92{
93 qual nullPred;
94 specCode specialCode;
95 exitkind exitCode;
96 typeIdSet access; /* access types */
97
98 /*@owned@*/ globSet globs; /* globals list */
99 /*@owned@*/ sRefSet mods; /* modifies */
100
28bf4b0b 101 stateClauseList specclauses;
885824d3 102
103 /*@dependent@*/ uentryList defparams;
104 bool hasGlobs BOOLBITS;
105 bool hasMods BOOLBITS;
93307a76 106
3814599d 107 functionConstraint preconditions;
108 functionConstraint postconditions;
93307a76 109
885824d3 110} *ufinfo ;
111
28bf4b0b 112typedef struct
885824d3 113{
114 typeIdSet access;
115 /*@owned@*/ globSet globs; /* globals list */
116 /*@owned@*/ sRefSet mods; /* modifies */
117} *uiinfo ;
118
28bf4b0b 119typedef struct
885824d3 120{
6fcd0b1e 121 typeIdSet access;
885824d3 122} *ueinfo ;
123
28bf4b0b 124typedef union
885824d3 125{
126 ucinfo uconst;
127 uvinfo var;
128 udinfo datatype;
129 ufinfo fcn;
130 uiinfo iter;
131 ueinfo enditer;
132} *uinfo ;
133
28bf4b0b 134struct s_uentry
885824d3 135{
136 ekind ukind;
137 cstring uname;
138 ctype utype;
139
140 fileloc whereSpecified;
141 fileloc whereDefined;
142 fileloc whereDeclared;
143
144 /* meaning of sref is different for:
145 ** variables current state
146 ** functions state of return value
147 ** types state of datatype
148 */
28bf4b0b 149
885824d3 150 /*@exposed@*/ /*@null@*/ sRef sref;
151
28bf4b0b 152 warnClause warn;
153
885824d3 154 /* Location list is complete only if showalluses is set. */
155 filelocList uses;
156
157 bool used BOOLBITS;
158 bool lset BOOLBITS; /* set in local table */
159 bool isPrivate BOOLBITS; /* specification only */
160 bool hasNameError BOOLBITS;
161
162 storageClassCode storageclass;
163 /*@relnull@*/ uinfo info; /* null for KELIPSMARKER, KINVALID */
164} ;
165
166/*
167** There is no uentry_isDefined to avoid confusion with
168** uentry_isCodeDefined (which was previously called
b7e84605 169** uentry_isDefined).
885824d3 170*/
171
0e41eb0e 172extern /*@nullwhentrue@*/ bool uentry_isUndefined (/*@special@*/ uentry p_e)
885824d3 173 /*@*/ ;
0e41eb0e 174extern /*@nullwhentrue@*/ bool uentry_isInvalid (/*@special@*/ uentry p_e)
885824d3 175 /*@*/ ;
0e41eb0e 176extern /*@falsewhennull@*/ bool uentry_isValid (/*@special@*/ uentry p_e)
885824d3 177 /*@*/ ;
178
179/*@constant null uentry uentry_undefined; @*/
180# define uentry_undefined ((uentry) NULL)
181
182# define uentry_isUndefined(e) ((e) == uentry_undefined)
183# define uentry_isValid(e) ((e) != uentry_undefined)
184# define uentry_isInvalid(e) ((e) == uentry_undefined)
185
186extern int uentry_compareStrict (uentry p_v1, uentry p_v2);
187
188/*@constant int PARAMUNKNOWN; @*/
189# define PARAMUNKNOWN -1
190
191extern bool uentry_isMaybeAbstract (uentry p_e) /*@*/ ;
192extern void uentry_setAbstract (uentry p_e) /*@modifies p_e@*/ ;
193extern void uentry_setConcrete (uentry p_e) /*@modifies p_e@*/ ;
194extern void uentry_setHasNameError (uentry p_ue) /*@modifies p_ue@*/ ;
195
0e41eb0e 196extern /*@falsewhennull@*/ bool uentry_isLset (/*@sef@*/ uentry p_e);
885824d3 197# define uentry_isLset(e) \
198 (uentry_isValid(e) && (e)->lset)
199
0e41eb0e 200extern /*@falsewhennull@*/ bool uentry_isUsed (/*@sef@*/ uentry p_e);
885824d3 201# define uentry_isUsed(e) (uentry_isValid(e) && (e)->used)
202
0e41eb0e 203extern /*@unused@*/ /*@falsewhennull@*/ bool
885824d3 204 uentry_isAbstractType (uentry p_e) /*@*/ ;
205# define uentry_isAbstractType(e) (uentry_isAbstractDatatype(e))
206
0e41eb0e 207extern /*@falsewhennull@*/ bool uentry_isConstant (/*@sef@*/ uentry p_e) /*@*/ ;
885824d3 208# define uentry_isConstant(e) \
209 (uentry_isValid(e) && ekind_isConst ((e)->ukind))
210
0e41eb0e 211extern /*@falsewhennull@*/ bool uentry_isEitherConstant (/*@sef@*/ uentry p_e) /*@*/ ;
885824d3 212# define uentry_isEitherConstant(e) \
213 (uentry_isValid(e) && (ekind_isConst ((e)->ukind) || ekind_isEnumConst ((e)->ukind)))
214
0e41eb0e 215extern /*@falsewhennull@*/ bool uentry_isEnumConstant (/*@sef@*/ uentry p_e) /*@*/ ;
885824d3 216# define uentry_isEnumConstant(e) \
217 (uentry_isValid(e) && ekind_isEnumConst ((e)->ukind))
218
0e41eb0e 219extern /*@falsewhennull@*/ bool uentry_isExternal (/*@sef@*/ uentry p_e) /*@*/ ;
885824d3 220# define uentry_isExternal(c) \
221 (uentry_isValid(c) && fileloc_isExternal (uentry_whereDefined (c)))
222
0e41eb0e 223extern /*@falsewhennull@*/ bool uentry_isExtern (/*@sef@*/ uentry p_e) /*@*/ ;
885824d3 224# define uentry_isExtern(c) \
225 (uentry_isValid(c) && (c)->storageclass == SCEXTERN)
226
227extern bool uentry_isForward (uentry p_e) /*@*/ ;
228
0e41eb0e 229extern /*@falsewhennull@*/ bool uentry_isFunction (/*@sef@*/ uentry p_e) /*@*/ ;
885824d3 230# define uentry_isFunction(e) \
231 (uentry_isValid(e) && ekind_isFunction ((e)->ukind))
232
0e41eb0e 233extern /*@falsewhennull@*/ bool uentry_isPriv (/*@sef@*/ uentry p_e) /*@*/ ;
885824d3 234# define uentry_isPriv(e) \
235 (uentry_isValid(e) && (e)->isPrivate)
236
0e41eb0e 237extern /*@falsewhennull@*/ bool uentry_isFileStatic (uentry p_ue) /*@*/ ;
238extern /*@falsewhennull@*/ bool uentry_isExported (uentry p_ue) /*@*/ ;
885824d3 239
0e41eb0e 240extern /*@falsewhennull@*/ bool uentry_isStatic (/*@sef@*/ uentry p_e) /*@*/ ;
885824d3 241# define uentry_isStatic(c) \
242 (uentry_isValid(c) && (c)->storageclass == SCSTATIC)
243
244extern void uentry_setLset (/*@sef@*/ uentry p_e);
245# define uentry_setLset(e) \
246 (uentry_isValid(e) ? (e)->lset = TRUE : TRUE)
247
248extern bool uentry_isSpecialFunction (uentry p_ue) /*@*/ ;
249extern bool uentry_isMessageLike (uentry p_ue) /*@*/ ;
250extern bool uentry_isScanfLike (uentry p_ue) /*@*/ ;
251extern bool uentry_isPrintfLike (uentry p_ue) /*@*/ ;
252
253extern void uentry_setMessageLike (uentry p_ue) /*@modifies p_ue@*/ ;
254extern void uentry_setScanfLike (uentry p_ue) /*@modifies p_ue@*/ ;
255extern void uentry_setPrintfLike (uentry p_ue) /*@modifies p_ue@*/ ;
256
80489f0a 257extern void uentry_checkName (uentry p_ue) /*@modifies g_warningstream, p_ue@*/ ;
885824d3 258
259extern bool uentry_sameObject (uentry p_e1, uentry p_e2);
260# define uentry_sameObject(e1,e2) ((e1) == (e2))
261
262extern void uentry_addAccessType (uentry p_ue, typeId p_tid) /*@modifies p_ue@*/ ;
263
264extern void uentry_showWhereAny (uentry p_spec)
80489f0a 265 /*@modifies g_warningstream@*/ ;
885824d3 266
267extern void uentry_checkParams (uentry p_ue);
268extern void uentry_mergeUses (uentry p_res, uentry p_other);
269extern void uentry_setExtern (uentry p_c);
270extern void uentry_setUsed (uentry p_e, fileloc p_loc);
271extern void uentry_setDefState (uentry p_ue, sstate p_defstate);
272
273extern void uentry_setNotUsed (/*@sef@*/ uentry p_e);
274# define uentry_setNotUsed(e) \
275 (uentry_isValid (e) ? (e)->used = FALSE : FALSE)
276
277extern bool uentry_wasUsed (/*@sef@*/ uentry p_e);
278# define uentry_wasUsed(e) \
279 (uentry_isValid (e) ? (e)->used : TRUE)
280
281extern void uentry_mergeConstantValue (uentry p_ue, /*@only@*/ multiVal p_m);
282
283extern /*@observer@*/ fileloc uentry_whereEarliest (uentry p_e) /*@*/ ;
284extern /*@observer@*/ cstring uentry_rawName (uentry p_e) /*@*/ ;
285extern /*@observer@*/ fileloc uentry_whereDeclared (uentry p_e) /*@*/ ;
286extern bool uentry_equiv (uentry p_p1, uentry p_p2) /*@*/ ;
0e41eb0e 287extern /*@falsewhennull@*/ bool uentry_hasName (uentry p_e) /*@*/ ;
288extern /*@falsewhennull@*/ bool uentry_hasRealName (uentry p_e) /*@*/ ;
289extern /*@falsewhennull@*/ bool uentry_isAbstractDatatype (uentry p_e) /*@*/ ;
290extern /*@falsewhennull@*/ bool uentry_isAnyTag (/*@special@*/ uentry p_ue)
885824d3 291 /*@uses p_ue->ukind@*/
292 /*@*/ ;
0e41eb0e 293extern /*@falsewhennull@*/ bool uentry_isDatatype (uentry p_e) /*@*/ ;
885824d3 294
0e41eb0e 295extern /*@falsewhennull@*/ bool uentry_isCodeDefined (uentry p_e) /*@*/ ;
885824d3 296
0e41eb0e 297extern /*@falsewhennull@*/ bool uentry_isDeclared (/*@special@*/ uentry p_e)
885824d3 298 /*@uses p_e->whereDeclared@*/ /*@*/ ;
299
300extern /*@observer@*/ cstring uentry_ekindName (uentry p_ue) /*@*/ ;
28bf4b0b 301extern /*@observer@*/ cstring uentry_ekindNameLC (uentry p_ue) /*@*/ ;
302
885824d3 303extern void uentry_showWhereDefined (uentry p_spec);
0e41eb0e 304extern /*@falsewhennull@*/ bool uentry_isEndIter (uentry p_e) /*@*/ ;
305extern /*@falsewhennull@*/ bool uentry_isEnumTag (/*@special@*/ uentry p_ue)
885824d3 306 /*@uses p_ue->ukind@*/ /*@*/ ;
0e41eb0e 307extern /*@falsewhennull@*/ bool uentry_isFakeTag (uentry p_e) /*@*/ ;
308extern /*@falsewhennull@*/ bool uentry_isIter (uentry p_e) /*@*/ ;
309extern /*@falsewhennull@*/ bool uentry_isMutableDatatype (uentry p_e) /*@*/ ;
310extern /*@falsewhennull@*/ bool uentry_isParam (uentry p_u) /*@*/ ;
311extern /*@falsewhennull@*/ bool uentry_isExpandedMacro (uentry p_u) /*@*/ ;
312extern /*@falsewhennull@*/ bool uentry_isSefParam (uentry p_u) /*@*/ ;
313extern /*@falsewhennull@*/ bool uentry_isAnyParam (/*@special@*/ uentry p_u)
885824d3 314 /*@uses p_u->ukind, p_u->info@*/
315 /*@*/ ;
316
0e41eb0e 317extern /*@falsewhennull@*/ bool uentry_isRealFunction (uentry p_e) /*@*/ ;
318extern /*@falsewhennull@*/ bool uentry_isSpecified (uentry p_e) /*@*/ ;
885824d3 319
0e41eb0e 320extern /*@falsewhennull@*/ bool uentry_isStructTag (/*@special@*/ uentry p_ue)
885824d3 321 /*@uses p_ue->ukind@*/ /*@*/ ;
0e41eb0e 322extern /*@falsewhennull@*/ bool uentry_isUnionTag (/*@special@*/ uentry p_ue)
885824d3 323 /*@uses p_ue->ukind@*/ /*@*/ ;
324
0e41eb0e 325extern /*@falsewhennull@*/ bool uentry_isVar (/*@special@*/ uentry p_e)
885824d3 326 /*@uses p_e->ukind@*/
327 /*@*/ ;
328
0e41eb0e 329extern /*@falsewhennull@*/ bool uentry_isVariable (/*@special@*/ uentry p_e)
885824d3 330 /*@uses p_e->ukind@*/
331 /*@*/ ;
332
333extern cstring uentry_dump (uentry p_v) ;
334extern cstring uentry_dumpParam (uentry p_v);
28bf4b0b 335
336extern /*@observer@*/ cstring uentry_observeRealName (uentry p_e) /*@*/ ;
337
885824d3 338extern cstring uentry_getName (/*@special@*/ uentry p_e)
339 /*@uses p_e->ukind, p_e->info, p_e->uname@*/
340 /*@*/ ;
341
342extern cstring uentry_unparse (uentry p_v) /*@*/ ;
343extern cstring uentry_unparseAbbrev (uentry p_v) /*@*/ ;
344extern cstring uentry_unparseFull (uentry p_v) /*@*/ ;
345extern void uentry_setMutable (uentry p_e) /*@modifies p_e@*/ ;
346extern ctype uentry_getAbstractType (uentry p_e) /*@*/ ;
347extern ctype uentry_getRealType (uentry p_e) /*@globals internalState@*/ ;
348extern ctype uentry_getType (uentry p_e) /*@*/ ;
349extern ekind uentry_getKind (uentry p_e) /*@*/ ;
350extern /*@observer@*/ fileloc uentry_whereDefined (uentry p_e) /*@*/ ;
351extern /*@observer@*/ fileloc uentry_whereSpecified (uentry p_e) /*@*/ ;
352extern int uentry_compare (uentry p_u1, uentry p_u2);
353extern /*@exposed@*/ sRef uentry_getSref (/*@temp@*/ uentry p_e) /*@*/ ;
354extern /*@observer@*/ sRefSet uentry_getMods (uentry p_l) /*@*/ ;
355extern typeIdSet uentry_accessType (uentry p_e) /*@*/ ;
356extern /*@observer@*/ fileloc uentry_whereEither (uentry p_e) /*@*/ ;
357extern /*@notnull@*/ uentry uentry_makeExpandedMacro (cstring p_s,
358 /*@temp@*/ fileloc p_f)
359 /*@*/ ;
360
80489f0a 361extern void uentry_checkMatchParam (uentry p_u1, uentry p_u2, int p_paramno, exprNode p_e) /*@modifies g_warningstream@*/ ;
885824d3 362
28bf4b0b 363extern /*@observer@*/ stateClauseList uentry_getStateClauseList (uentry p_ue) /*@*/ ;
885824d3 364
365extern void uentry_showWhereLastExtra (uentry p_spec, /*@only@*/ cstring p_extra)
80489f0a 366 /*@modifies g_warningstream@*/ ;
885824d3 367
885824d3 368extern void uentry_setRefCounted (uentry p_e);
369
370extern /*@notnull@*/ /*@only@*/ uentry uentry_makeUnnamedVariable (ctype p_t);
288cbc5c 371extern /*@falsewhennull@*/ bool uentry_isUnnamedVariable (uentry) /*@*/;
885824d3 372
373extern /*@notnull@*/ uentry
374 uentry_makeUnspecFunction (cstring p_n, ctype p_t, typeIdSet p_access,
375 /*@keep@*/ fileloc p_f);
376
377extern /*@notnull@*/ uentry
378 uentry_makePrivFunction2 (cstring p_n, ctype p_t,
379 typeIdSet p_access,
380 /*@only@*/ globSet p_globs,
381 /*@only@*/ sRefSet p_mods, /*@keep@*/ fileloc p_f);
382
383extern /*@notnull@*/ uentry
384 uentry_makeSpecEnumConstant (cstring p_n, ctype p_t, /*@keep@*/ fileloc p_loc) /*@*/ ;
385
386extern /*@notnull@*/ uentry
387 uentry_makeEnumTag (cstring p_n, ctype p_t, /*@only@*/ fileloc p_loc) /*@*/ ;
388
389extern /*@notnull@*/ uentry
390 uentry_makeTypeListFunction (cstring p_n, typeIdSet p_access, /*@only@*/ fileloc p_f)
391 /*@*/ ;
392
393extern /*@notnull@*/ uentry
394 uentry_makeSpecFunction (cstring p_n, ctype p_t,
395 typeIdSet p_access, /*@only@*/ globSet p_globs,
396 /*@only@*/ sRefSet p_mods, /*@keep@*/ fileloc p_f);
885824d3 397
398extern /*@notnull@*/ uentry
399 uentry_makeEnumConstant (cstring p_n, ctype p_t) /*@*/ ;
400
401extern /*@notnull@*/ uentry
402 uentry_makeEnumInitializedConstant (cstring p_n, ctype p_t, exprNode p_expr) /*@*/ ;
403
404extern /*@notnull@*/ /*@only@*/ uentry
405 uentry_makeConstant (/*@temp@*/ cstring p_n, ctype p_t, /*@keep@*/ fileloc p_f)
406 /*@*/ ;
5e211f69 407
408extern /*@only@*/ /*@notnull@*/ uentry
3e3ec469 409 uentry_makeConstantValue (/*@temp@*/ cstring p_n, ctype p_t, /*@keep@*/ fileloc p_f,
410 bool p_priv, /*@only@*/ multiVal p_val)
5e211f69 411 /*@*/ ;
412
413extern /*@notnull@*/ /*@only@*/ uentry
414 uentry_makeMacroConstant (/*@temp@*/ cstring p_n, ctype p_t, /*@keep@*/ fileloc p_f)
415 /*@*/ ;
416
885824d3 417extern /*@notnull@*/ /*@only@*/ uentry
28bf4b0b 418 uentry_makeDatatype (/*@temp@*/ cstring p_n, ctype p_t, ynm p_mut, ynm p_abstract,
885824d3 419 /*@only@*/ fileloc p_f) /*@*/ ;
420extern /*@notnull@*/ /*@only@*/ uentry
421 uentry_makeDatatypeAux (/*@temp@*/ cstring p_n, ctype p_t, ynm p_mut,
28bf4b0b 422 ynm p_abstract, /*@keep@*/ fileloc p_f, bool p_priv) /*@*/ ;
885824d3 423extern /*@notnull@*/ uentry uentry_makeElipsisMarker (void) /*@*/ ;
424
425extern void uentry_makeVarFunction (/*@temp@*/ uentry p_ue) /*@modifies p_ue@*/ ;
b072092f 426extern void uentry_makeConstantFunction (/*@temp@*/ uentry p_ue) /*@modifies p_ue@*/ ;
885824d3 427
428extern bool uentry_isElipsisMarker (/*@sef@*/ uentry p_u) /*@*/ ;
429# define uentry_isElipsisMarker(u) \
430 (uentry_isValid(u) && ekind_isElipsis ((u)->ukind))
431
432extern /*@notnull@*/ uentry
433 uentry_makeEndIter (cstring p_n, /*@only@*/ fileloc p_f) /*@*/ ;
434extern /*@notnull@*/ uentry
435 uentry_makeEnumTagLoc (cstring p_n, ctype p_t) /*@*/ ;
436extern /*@notnull@*/ uentry
437 uentry_makeForwardFunction (cstring p_n, typeId p_access, /*@temp@*/ fileloc p_f) /*@*/ ;
438
439extern /*@notnull@*/ uentry
440 uentry_makeFunction (cstring p_n, ctype p_t,
441 typeId p_access,
442 /*@only@*/ globSet p_globs, /*@only@*/ sRefSet p_mods,
28bf4b0b 443 /*@only@*/ warnClause p_warn,
885824d3 444 /*@only@*/ fileloc p_f);
445
446extern /*@notnull@*/ uentry
447 uentry_makeIter (cstring p_n, ctype p_ct, /*@only@*/ fileloc p_f) /*@*/ ;
448extern /*@notnull@*/ uentry
449 uentry_makeParam (idDecl p_t, int p_i) /*@*/ ;
450
451extern /*@notnull@*/ uentry
452 uentry_makeStructTag (cstring p_n, ctype p_t, /*@only@*/ fileloc p_loc);
453extern /*@notnull@*/ uentry
454 uentry_makeStructTagLoc (cstring p_n, ctype p_t);
455extern /*@notnull@*/ uentry
456 uentry_makeUnionTag (cstring p_n, ctype p_t, /*@only@*/ fileloc p_loc);
457extern /*@notnull@*/ uentry
458 uentry_makeUnionTagLoc (cstring p_n, ctype p_t);
459extern /*@notnull@*/ uentry
460 uentry_makeVariable (cstring p_n, ctype p_t, /*@keep@*/ fileloc p_f, bool p_isPriv);
461extern /*@notnull@*/ /*@only@*/ uentry
462 uentry_makeVariableLoc (cstring p_n, ctype p_t);
463
885824d3 464extern /*@notnull@*/ /*@only@*/
6970c11b 465 uentry uentry_makeVariableParam (cstring p_n, ctype p_t, fileloc p_loc);
885824d3 466
467extern /*@notnull@*/ /*@only@*/
6970c11b 468uentry uentry_makeVariableSrefParam (cstring p_n, ctype p_t, /*@only@*/ fileloc p_loc,
469 /*@exposed@*/ sRef p_s);
885824d3 470extern /*@notnull@*/ /*@only@*/
471 uentry uentry_makeIdFunction (idDecl p_id);
472extern /*@notnull@*/ /*@only@*/
473 uentry uentry_makeIdDatatype (idDecl p_id);
474extern /*@notnull@*/ /*@only@*/
28bf4b0b 475 uentry uentry_makeBoolDatatype (ynm p_abstract);
885824d3 476extern void uentry_mergeDefinition (uentry p_old, /*@only@*/ uentry p_unew);
477extern void uentry_mergeEntries (uentry p_spec, /*@only@*/ uentry p_def);
478extern uentry uentry_nameCopy (/*@only@*/ cstring p_name, uentry p_e);
479extern uentry uentry_undump (ekind p_kind, fileloc p_loc, char **p_s);
480extern /*@observer@*/ uentryList uentry_getParams (uentry p_l) /*@*/ ;
481extern void uentry_resetParams (uentry p_ue, /*@only@*/ uentryList p_pn)
482 /*@modifies p_ue@*/ ;
483extern /*@observer@*/ globSet uentry_getGlobs (uentry p_l) /*@*/ ;
484extern qual uentry_nullPred (uentry p_u);
485extern void uentry_free (/*@only@*/ /*@only@*/ uentry p_e);
486extern void uentry_setDatatype (uentry p_e, usymId p_uid);
487
488extern void uentry_setDefined (/*@special@*/ uentry p_e, fileloc p_f)
489 /*@uses p_e->whereDefined, p_e->ukind, p_e->uname, p_e->info@*/
490 /*@modifies p_e@*/ ;
491
492extern void uentry_checkDecl (void);
493extern void uentry_clearDecl (void);
494extern void uentry_setDeclared (uentry p_e, fileloc p_f);
495extern void uentry_setDeclaredOnly (uentry p_e, /*@only@*/ fileloc p_f);
496extern void uentry_setDeclaredForceOnly (uentry p_e, /*@only@*/ fileloc p_f);
497extern void uentry_setFunctionDefined (uentry p_e, fileloc p_loc);
498extern void uentry_setName (uentry p_e, /*@only@*/ cstring p_n);
499extern void uentry_setParam (uentry p_e);
500extern void uentry_setSref (uentry p_e, /*@exposed@*/ sRef p_s);
501extern void uentry_setStatic (uentry p_c);
502
503extern void uentry_setModifies (uentry p_ue, /*@owned@*/ sRefSet p_sr)
504 /*@modifies p_ue, p_sr@*/;
505
28bf4b0b 506extern bool uentry_hasWarning (uentry p_ue) /*@*/ ;
507
508extern void uentry_addWarning (uentry p_ue, /*@only@*/ warnClause p_warn)
509 /*@modifies p_ue*/;
510
511extern void uentry_setStateClauseList (uentry p_ue, /*@only@*/ stateClauseList p_clauses)
885824d3 512 /*@modifies p_ue@*/ ;
513
514extern void uentry_setType (uentry p_e, ctype p_t);
515
516extern /*@unused@*/ /*@observer@*/ cstring uentry_checkedName (uentry p_ue);
80489f0a 517extern void uentry_showWhereLastPlain (uentry p_spec) /*@modifies g_warningstream@*/ ;
885824d3 518
519extern void
520 uentry_showWhereSpecifiedExtra (uentry p_spec, /*@only@*/ cstring p_s)
80489f0a 521 /*@modifies g_warningstream@*/ ;
885824d3 522
80489f0a 523extern void uentry_showWhereSpecified (uentry p_spec) /*@modifies g_warningstream@*/ ;
524extern void uentry_showWhereLast (uentry p_spec) /*@modifies g_warningstream@*/ ;
525extern void uentry_showWhereDeclared (uentry p_spec) /*@modifies g_warningstream@*/ ;
885824d3 526
527extern /*@notnull@*/ /*@only@*/ uentry uentry_makeIdVariable (idDecl p_t) /*@*/ ;
528extern uentry uentry_copy (uentry p_e) /*@*/ ;
6fcd0b1e 529extern uentry uentry_copyNoSave (uentry p_e) /*@*/ ; /* for use for uentries that do not live beyond function exits */
885824d3 530extern void uentry_freeComplete (/*@only@*/ uentry p_e) ;
531extern void uentry_clearDefined (uentry p_e) /*@modifies p_e@*/;
532extern /*@observer@*/ cstring uentry_specDeclName (uentry p_u) /*@*/ ;
533
534extern void
535 uentry_mergeState (uentry p_res, uentry p_other, fileloc p_loc,
536 bool p_mustReturn, bool p_flip, bool p_opt,
537 clause p_cl) /*@modifies p_res, p_other@*/ ;
538
539extern void uentry_setState (uentry p_res, uentry p_other)
540 /*@modifies p_res, p_other@*/ ;
541
542extern void uentry_setRefParam (uentry p_e) /*@modifies p_e@*/ ;
543
544extern void uentry_setDeclaredForce (uentry p_e, fileloc p_f) /*@modifies p_e@*/;
545extern bool uentry_isNonLocal (uentry p_ue) /*@*/ ;
28bf4b0b 546extern bool uentry_isGlobalVariable (uentry p_ue) /*@*/;
547extern bool uentry_isVisibleExternally (uentry p_ue) /*@*/;
885824d3 548extern bool uentry_isRefParam (uentry p_u) /*@*/ ;
549extern bool uentry_hasGlobs (uentry p_ue) /*@*/ ;
550extern bool uentry_hasMods (uentry p_ue) /*@*/ ;
551
28bf4b0b 552extern bool uentry_hasStateClauseList (uentry p_ue) /*@*/ ;
ccf0a4a8 553extern bool uentry_hasConditions (uentry p_ue) /*@*/ ;
554
885824d3 555extern exitkind uentry_getExitCode (uentry p_ue) /*@*/ ;
556
557extern void uentry_checkYieldParam (uentry p_old, uentry p_unew);
558extern bool uentry_isOnly (uentry p_ue) /*@*/ ;
559extern bool uentry_isUnique (uentry p_ue) /*@*/ ;
560extern void uentry_reflectQualifiers (uentry p_ue, qualList p_q) /*@modifies p_ue@*/;
561extern bool uentry_isOut (uentry p_u) /*@*/ ;
562extern bool uentry_isPartial (uentry p_u) /*@*/ ;
563extern bool uentry_isStateSpecial (uentry p_u) /*@*/ ;
564extern bool uentry_possiblyNull (uentry p_u) /*@*/ ;
565extern ctype uentry_getForceRealType (uentry p_e) /*@globals internalState@*/ ;
566extern alkind uentry_getAliasKind (uentry p_u) /*@*/ ;
567extern exkind uentry_getExpKind (uentry p_u) /*@*/ ;
568extern /*@observer@*/ multiVal uentry_getConstantValue (uentry p_e) /*@*/ ;
569extern void uentry_fixupSref (uentry p_ue) /*@modifies p_ue@*/ ;
b87215ab 570extern void uentry_setGlobals (uentry p_ue, /*@only@*/ globSet p_globs) /*@modifies p_ue, p_globs@*/ ;
885824d3 571extern bool uentry_isYield (uentry p_ue) /*@*/ ;
572extern /*@notnull@*/ uentry uentry_makeIdConstant (idDecl p_t) /*@*/ ;
573extern /*@observer@*/ cstring uentry_getRealName (uentry p_e) /*@*/ ;
574extern int uentry_xcomparealpha (uentry *p_p1, uentry *p_p2) /*@*/ ;
575extern int uentry_xcompareuses (uentry *p_p1, uentry *p_p2) /*@*/ ;
576extern /*@observer@*/ cstring uentry_specOrDefName (uentry p_u) /*@*/ ;
577extern void uentry_copyState (uentry p_res, uentry p_other);
578extern bool uentry_sameKind (uentry p_u1, uentry p_u2);
6fcd0b1e 579extern /*@exposed@*/ sRef uentry_returnedRef (uentry p_u, exprNodeList p_args, fileloc p_loc);
885824d3 580extern bool uentry_isReturned (uentry p_u);
581extern bool uentry_isRefCountedDatatype (uentry p_e);
582extern sstate uentry_getDefState (uentry p_u);
583extern /*@unused@*/ void uentry_markFree (/*@owned@*/ uentry p_u);
584extern /*@dependent@*/ sRef uentry_getOrigSref (uentry p_e);
585extern void uentry_destroyMod (void) /*@modifies internalState@*/;
586extern void uentry_showDefSpecInfo (uentry p_ce, fileloc p_fwhere);
587extern void uentry_markOwned (/*@owned@*/ uentry p_u);
588
589extern /*@observer@*/ fileloc uentry_whereLast (uentry p_e) /*@*/ ;
590extern void uentry_setParamNo (uentry p_ue, int p_pno) /*@modifies p_ue@*/;
591
592extern /*@observer@*/ filelocList uentry_getUses (/*@sef@*/ uentry p_e) /*@*/ ;
593# define uentry_getUses(u) (uentry_isValid (u) ? (u)->uses : filelocList_undefined)
594
595extern bool uentry_isCheckedUnknown (uentry p_ue) /*@*/ ;
596extern bool uentry_isCheckedModify (uentry p_ue) /*@*/ ;
597extern bool uentry_isUnchecked (uentry p_ue) /*@*/ ;
598extern bool uentry_isChecked (uentry p_ue) /*@*/ ;
599extern bool uentry_isCheckMod (uentry p_ue) /*@*/ ;
600extern bool uentry_isCheckedStrict (uentry p_ue) /*@*/ ;
601extern void uentry_setUnchecked (uentry p_ue) /*@modifies p_ue@*/ ;
602extern void uentry_setChecked (uentry p_ue) /*@modifies p_ue@*/ ;
603extern void uentry_setCheckMod (uentry p_ue) /*@modifies p_ue@*/ ;
604extern void uentry_setCheckedStrict (uentry p_ue) /*@modifies p_ue@*/ ;
605
606extern bool uentry_hasAccessType (uentry p_e);
607
28bf4b0b 608/*@constant cstring GLOBAL_MARKER_NAME@*/
609# define GLOBAL_MARKER_NAME cstring_makeLiteralTemp ("#GM#")
1ac6313d 610
1ac6313d 611/* functions for making modification to null-term info */
b7b694d6 612extern void uentry_setNullTerminatedState (uentry p_e);
613extern void uentry_setPossiblyNullTerminatedState (uentry p_e);
614extern void uentry_setSize(uentry p_e, int p_size);
615extern void uentry_setLen(uentry p_e, int p_len);
1ac6313d 616
4cccc6ad 617/*@i66*/
618/*@-nullderef@*/
1ac6313d 619extern bool uentry_hasBufStateInfo (uentry p_ue);
620# define uentry_hasBufStateInfo(p_ue) \
621 (((p_ue)->info->var->bufinfo != NULL) ? TRUE : FALSE)
622
84c9ffbf 623/*@unused@*/ extern bool uentry_isNullTerminated(/*@sef@*/uentry p_ue);
1ac6313d 624# define uentry_isNullTerminated(p_ue) \
bb7c2085 625 ( uentry_hasBufStateInfo((p_ue ) ) ? ((p_ue)->info->var->bufinfo->bufstate \
1ac6313d 626 == BB_NULLTERMINATED) : FALSE)
627
84c9ffbf 628/*@unused@*/ extern bool uentry_isPossiblyNullTerminated( /*@sef@*/ uentry p_ue);
1ac6313d 629# define uentry_isPossiblyNullTerminated(p_ue) \
bb7c2085 630 ( uentry_hasBufStateInfo((p_ue)) ? ((p_ue)->info->var->bufinfo->bufstate \
1ac6313d 631 == BB_POSSIBLYNULLTERMINATED) : FALSE)
632
84c9ffbf 633/*@unused@*/ extern bool uentry_isNotNullTerminated( /*@sef@*/ uentry p_ue);
1ac6313d 634# define uentry_isNotNullTerminated(p_ue) \
bb7c2085 635 ( uentry_hasBufStateInfo((p_ue) ) ? ((p_ue)->info->var->bufinfo->bufstate \
1ac6313d 636 == BB_NOTNULLTERMINATED) : FALSE)
4cccc6ad 637/*@=nullderef@*/
1ac6313d 638
639/* end modifications */
640
28bf4b0b 641extern uentry uentry_makeGlobalMarker (void) ;
642extern bool uentry_isGlobalMarker (uentry) /*@*/ ;
643
7ebcc5bb 644extern /*@exposed@*/ uentry uentry_makeUnrecognized (cstring p_c, /*@only@*/ fileloc p_loc);
28bf4b0b 645
885824d3 646# ifdef DOANNOTS
5e211f69 647typedef enum
648{
649 AN_UNKNOWN, AN_FCNRETURN, AN_FCNPARAM, AN_SUFIELD, AN_TDEFN, AN_GSVAR,
650 AN_CONST, AN_LAST
651} ancontext;
885824d3 652
653extern void initAnnots ();
654extern void printAnnots (void);
655extern void uentry_tallyAnnots (uentry u, ancontext kind);
656# endif /* DOANNOTS */
657
ba45e1e4 658extern bool uentry_hasMetaStateEnsures (uentry p_e) /*@*/ ;
ccf0a4a8 659extern /*@only@*/ metaStateConstraintList uentry_getMetaStateEnsures (uentry p_e);
ba45e1e4 660
4cccc6ad 661/* start modifications */
b7b694d6 662
93307a76 663/*drl7x*/
28bf4b0b 664extern constraintList uentry_getFcnPreconditions (uentry p_ue);
665extern constraintList uentry_getFcnPostconditions (uentry p_ue);
920a3797 666
3814599d 667extern void uentry_setPostconditions (uentry p_ue, /*@only@*/ functionConstraint p_postconditions);
668
669extern void uentry_setPreconditions (uentry p_ue, /*@only@*/ functionConstraint p_preconditions);
b7b694d6 670/*end mods*/
4cccc6ad 671
6483a926 672/*
673** For debugging only
674*/
675
676# ifdef DEBUGSPLINT
677extern void uentry_checkValid (uentry p_ue) /*@modifies g_errorstream@*/ ;
678# endif
679
885824d3 680# else
681# error "Multiple include"
682# endif
683
684
685
git-cvsimport mirror of splint
This page took 0.182606 seconds and 5 git commands to generate.