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