2 ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2003.
3 ** See ../LICENSE for license information.
10 ** universal symbol table entry
11 ** (combines old llentry, centry, and ttentry)
15 ** vkind --- need to fix value for consistency in dump files
27 VKPARAM, VKYIELDPARAM, VKREFYIELDPARAM,
28 VKRETPARAM, VKREFPARAM,
29 VKSEFPARAM, VKREFSEFPARAM,
30 VKSEFRETPARAM, VKREFSEFRETPARAM,
34 /*@constant vkind VKFIRST;@*/
35 # define VKFIRST VKSPEC
37 /*@constant vkind VKLAST;@*/
38 # define VKLAST VKEXPMACRO
49 /* start modifications */
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 */
56 typedef /*@null@*/ struct s_bbufinfo {
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 */
64 vkind kind; /* kind (parameter, specified) */
65 chkind checked; /* how is it checked */
68 bbufinfo bufinfo; /* is valid only if the entry is a variable and (a pointer
71 /* end modifications */
75 qual abs; /* oneof QU_UNKNOWN, QU_ABSTRACT, QU_NUMABSTRACT, QU_CONCRETE */
80 /* information for specified functions */
96 typeIdSet access; /* access types */
98 /*@owned@*/ globSet globs; /* globals list */
99 /*@owned@*/ sRefSet mods; /* modifies */
101 stateClauseList specclauses;
103 /*@dependent@*/ uentryList defparams;
104 bool hasGlobs BOOLBITS;
105 bool hasMods BOOLBITS;
107 functionConstraint preconditions;
108 functionConstraint postconditions;
115 /*@owned@*/ globSet globs; /* globals list */
116 /*@owned@*/ sRefSet mods; /* modifies */
140 fileloc whereSpecified;
141 fileloc whereDefined;
142 fileloc whereDeclared;
144 /* meaning of sref is different for:
145 ** variables current state
146 ** functions state of return value
147 ** types state of datatype
150 /*@exposed@*/ /*@null@*/ sRef sref;
154 /* Location list is complete only if showalluses is set. */
158 bool lset BOOLBITS; /* set in local table */
159 bool isPrivate BOOLBITS; /* specification only */
160 bool hasNameError BOOLBITS;
162 storageClassCode storageclass;
163 /*@relnull@*/ uinfo info; /* null for KELIPSMARKER, KINVALID */
167 ** There is no uentry_isDefined to avoid confusion with
168 ** uentry_isCodeDefined (which was previously called
169 ** uentry_isDefined).
172 extern /*@nullwhentrue@*/ bool uentry_isUndefined (/*@special@*/ uentry p_e)
174 extern /*@nullwhentrue@*/ bool uentry_isInvalid (/*@special@*/ uentry p_e)
176 extern /*@falsewhennull@*/ bool uentry_isValid (/*@special@*/ uentry p_e)
179 /*@constant null uentry uentry_undefined; @*/
180 # define uentry_undefined ((uentry) NULL)
182 # define uentry_isUndefined(e) ((e) == uentry_undefined)
183 # define uentry_isValid(e) ((e) != uentry_undefined)
184 # define uentry_isInvalid(e) ((e) == uentry_undefined)
186 extern int uentry_compareStrict (uentry p_v1, uentry p_v2);
188 /*@constant int PARAMUNKNOWN; @*/
189 # define PARAMUNKNOWN -1
191 extern bool uentry_isMaybeAbstract (uentry p_e) /*@*/ ;
192 extern void uentry_setAbstract (uentry p_e) /*@modifies p_e@*/ ;
193 extern void uentry_setConcrete (uentry p_e) /*@modifies p_e@*/ ;
194 extern void uentry_setHasNameError (uentry p_ue) /*@modifies p_ue@*/ ;
196 extern /*@falsewhennull@*/ bool uentry_isLset (/*@sef@*/ uentry p_e);
197 # define uentry_isLset(e) \
198 (uentry_isValid(e) && (e)->lset)
200 extern /*@falsewhennull@*/ bool uentry_isUsed (/*@sef@*/ uentry p_e);
201 # define uentry_isUsed(e) (uentry_isValid(e) && (e)->used)
203 extern /*@unused@*/ /*@falsewhennull@*/ bool
204 uentry_isAbstractType (uentry p_e) /*@*/ ;
205 # define uentry_isAbstractType(e) (uentry_isAbstractDatatype(e))
207 extern /*@falsewhennull@*/ bool uentry_isConstant (/*@sef@*/ uentry p_e) /*@*/ ;
208 # define uentry_isConstant(e) \
209 (uentry_isValid(e) && ekind_isConst ((e)->ukind))
211 extern /*@falsewhennull@*/ bool uentry_isEitherConstant (/*@sef@*/ uentry p_e) /*@*/ ;
212 # define uentry_isEitherConstant(e) \
213 (uentry_isValid(e) && (ekind_isConst ((e)->ukind) || ekind_isEnumConst ((e)->ukind)))
215 extern /*@falsewhennull@*/ bool uentry_isEnumConstant (/*@sef@*/ uentry p_e) /*@*/ ;
216 # define uentry_isEnumConstant(e) \
217 (uentry_isValid(e) && ekind_isEnumConst ((e)->ukind))
219 extern /*@falsewhennull@*/ bool uentry_isExternal (/*@sef@*/ uentry p_e) /*@*/ ;
220 # define uentry_isExternal(c) \
221 (uentry_isValid(c) && fileloc_isExternal (uentry_whereDefined (c)))
223 extern /*@falsewhennull@*/ bool uentry_isExtern (/*@sef@*/ uentry p_e) /*@*/ ;
224 # define uentry_isExtern(c) \
225 (uentry_isValid(c) && (c)->storageclass == SCEXTERN)
227 extern bool uentry_isForward (uentry p_e) /*@*/ ;
229 extern /*@falsewhennull@*/ bool uentry_isFunction (/*@sef@*/ uentry p_e) /*@*/ ;
230 # define uentry_isFunction(e) \
231 (uentry_isValid(e) && ekind_isFunction ((e)->ukind))
233 extern /*@falsewhennull@*/ bool uentry_isPriv (/*@sef@*/ uentry p_e) /*@*/ ;
234 # define uentry_isPriv(e) \
235 (uentry_isValid(e) && (e)->isPrivate)
237 extern /*@falsewhennull@*/ bool uentry_isFileStatic (uentry p_ue) /*@*/ ;
238 extern /*@falsewhennull@*/ bool uentry_isExported (uentry p_ue) /*@*/ ;
240 extern /*@falsewhennull@*/ bool uentry_isStatic (/*@sef@*/ uentry p_e) /*@*/ ;
241 # define uentry_isStatic(c) \
242 (uentry_isValid(c) && (c)->storageclass == SCSTATIC)
244 extern void uentry_setLset (/*@sef@*/ uentry p_e);
245 # define uentry_setLset(e) \
246 (uentry_isValid(e) ? (e)->lset = TRUE : TRUE)
248 extern bool uentry_isSpecialFunction (uentry p_ue) /*@*/ ;
249 extern bool uentry_isMessageLike (uentry p_ue) /*@*/ ;
250 extern bool uentry_isScanfLike (uentry p_ue) /*@*/ ;
251 extern bool uentry_isPrintfLike (uentry p_ue) /*@*/ ;
253 extern void uentry_setMessageLike (uentry p_ue) /*@modifies p_ue@*/ ;
254 extern void uentry_setScanfLike (uentry p_ue) /*@modifies p_ue@*/ ;
255 extern void uentry_setPrintfLike (uentry p_ue) /*@modifies p_ue@*/ ;
257 extern void uentry_checkName (uentry p_ue) /*@modifies g_warningstream, p_ue@*/ ;
259 extern bool uentry_sameObject (uentry p_e1, uentry p_e2);
260 # define uentry_sameObject(e1,e2) ((e1) == (e2))
262 extern void uentry_addAccessType (uentry p_ue, typeId p_tid) /*@modifies p_ue@*/ ;
264 extern void uentry_showWhereAny (uentry p_spec)
265 /*@modifies g_warningstream@*/ ;
267 extern void uentry_checkParams (uentry p_ue);
268 extern void uentry_mergeUses (uentry p_res, uentry p_other);
269 extern void uentry_setExtern (uentry p_c);
270 extern void uentry_setUsed (uentry p_e, fileloc p_loc);
271 extern void uentry_setDefState (uentry p_ue, sstate p_defstate);
273 extern void uentry_setNotUsed (/*@sef@*/ uentry p_e);
274 # define uentry_setNotUsed(e) \
275 (uentry_isValid (e) ? (e)->used = FALSE : FALSE)
277 extern bool uentry_wasUsed (/*@sef@*/ uentry p_e);
278 # define uentry_wasUsed(e) \
279 (uentry_isValid (e) ? (e)->used : TRUE)
281 extern void uentry_mergeConstantValue (uentry p_ue, /*@only@*/ multiVal p_m);
283 extern /*@observer@*/ fileloc uentry_whereEarliest (uentry p_e) /*@*/ ;
284 extern /*@observer@*/ cstring uentry_rawName (uentry p_e) /*@*/ ;
285 extern /*@observer@*/ fileloc uentry_whereDeclared (uentry p_e) /*@*/ ;
286 extern bool uentry_equiv (uentry p_p1, uentry p_p2) /*@*/ ;
287 extern /*@falsewhennull@*/ bool uentry_hasName (uentry p_e) /*@*/ ;
288 extern /*@falsewhennull@*/ bool uentry_hasRealName (uentry p_e) /*@*/ ;
289 extern /*@falsewhennull@*/ bool uentry_isAbstractDatatype (uentry p_e) /*@*/ ;
290 extern /*@falsewhennull@*/ bool uentry_isAnyTag (/*@special@*/ uentry p_ue)
291 /*@uses p_ue->ukind@*/
293 extern /*@falsewhennull@*/ bool uentry_isDatatype (uentry p_e) /*@*/ ;
295 extern /*@falsewhennull@*/ bool uentry_isCodeDefined (uentry p_e) /*@*/ ;
297 extern /*@falsewhennull@*/ bool uentry_isDeclared (/*@special@*/ uentry p_e)
298 /*@uses p_e->whereDeclared@*/ /*@*/ ;
300 extern /*@observer@*/ cstring uentry_ekindName (uentry p_ue) /*@*/ ;
301 extern /*@observer@*/ cstring uentry_ekindNameLC (uentry p_ue) /*@*/ ;
303 extern void uentry_showWhereDefined (uentry p_spec);
304 extern /*@falsewhennull@*/ bool uentry_isEndIter (uentry p_e) /*@*/ ;
305 extern /*@falsewhennull@*/ bool uentry_isEnumTag (/*@special@*/ uentry p_ue)
306 /*@uses p_ue->ukind@*/ /*@*/ ;
307 extern /*@falsewhennull@*/ bool uentry_isFakeTag (uentry p_e) /*@*/ ;
308 extern /*@falsewhennull@*/ bool uentry_isIter (uentry p_e) /*@*/ ;
309 extern /*@falsewhennull@*/ bool uentry_isMutableDatatype (uentry p_e) /*@*/ ;
310 extern /*@falsewhennull@*/ bool uentry_isParam (uentry p_u) /*@*/ ;
311 extern /*@falsewhennull@*/ bool uentry_isExpandedMacro (uentry p_u) /*@*/ ;
312 extern /*@falsewhennull@*/ bool uentry_isSefParam (uentry p_u) /*@*/ ;
313 extern /*@falsewhennull@*/ bool uentry_isAnyParam (/*@special@*/ uentry p_u)
314 /*@uses p_u->ukind, p_u->info@*/
317 extern /*@falsewhennull@*/ bool uentry_isRealFunction (uentry p_e) /*@*/ ;
318 extern /*@falsewhennull@*/ bool uentry_isSpecified (uentry p_e) /*@*/ ;
320 extern /*@falsewhennull@*/ bool uentry_isStructTag (/*@special@*/ uentry p_ue)
321 /*@uses p_ue->ukind@*/ /*@*/ ;
322 extern /*@falsewhennull@*/ bool uentry_isUnionTag (/*@special@*/ uentry p_ue)
323 /*@uses p_ue->ukind@*/ /*@*/ ;
325 extern /*@falsewhennull@*/ bool uentry_isVar (/*@special@*/ uentry p_e)
326 /*@uses p_e->ukind@*/
329 extern /*@falsewhennull@*/ bool uentry_isVariable (/*@special@*/ uentry p_e)
330 /*@uses p_e->ukind@*/
333 extern cstring uentry_dump (uentry p_v) ;
334 extern cstring uentry_dumpParam (uentry p_v);
336 extern /*@observer@*/ cstring uentry_observeRealName (uentry p_e) /*@*/ ;
338 extern cstring uentry_getName (/*@special@*/ uentry p_e)
339 /*@uses p_e->ukind, p_e->info, p_e->uname@*/
342 extern cstring uentry_unparse (uentry p_v) /*@*/ ;
343 extern cstring uentry_unparseAbbrev (uentry p_v) /*@*/ ;
344 extern cstring uentry_unparseFull (uentry p_v) /*@*/ ;
345 extern void uentry_setMutable (uentry p_e) /*@modifies p_e@*/ ;
346 extern ctype uentry_getAbstractType (uentry p_e) /*@*/ ;
347 extern ctype uentry_getRealType (uentry p_e) /*@globals internalState@*/ ;
348 extern ctype uentry_getType (uentry p_e) /*@*/ ;
349 extern ekind uentry_getKind (uentry p_e) /*@*/ ;
350 extern /*@observer@*/ fileloc uentry_whereDefined (uentry p_e) /*@*/ ;
351 extern /*@observer@*/ fileloc uentry_whereSpecified (uentry p_e) /*@*/ ;
352 extern int uentry_compare (uentry p_u1, uentry p_u2);
353 extern /*@exposed@*/ sRef uentry_getSref (/*@temp@*/ uentry p_e) /*@*/ ;
354 extern /*@observer@*/ sRefSet uentry_getMods (uentry p_l) /*@*/ ;
355 extern typeIdSet uentry_accessType (uentry p_e) /*@*/ ;
356 extern /*@observer@*/ fileloc uentry_whereEither (uentry p_e) /*@*/ ;
357 extern /*@notnull@*/ uentry uentry_makeExpandedMacro (cstring p_s,
358 /*@temp@*/ fileloc p_f)
361 extern void uentry_checkMatchParam (uentry p_u1, uentry p_u2, int p_paramno, exprNode p_e) /*@modifies g_warningstream@*/ ;
363 extern /*@observer@*/ stateClauseList uentry_getStateClauseList (uentry p_ue) /*@*/ ;
365 extern void uentry_showWhereLastExtra (uentry p_spec, /*@only@*/ cstring p_extra)
366 /*@modifies g_warningstream@*/ ;
368 extern void uentry_setRefCounted (uentry p_e);
370 extern /*@notnull@*/ /*@only@*/ uentry uentry_makeUnnamedVariable (ctype p_t);
371 extern /*@falsewhennull@*/ bool uentry_isUnnamedVariable (uentry) /*@*/;
373 extern /*@notnull@*/ uentry
374 uentry_makeUnspecFunction (cstring p_n, ctype p_t, typeIdSet p_access,
375 /*@keep@*/ fileloc p_f);
377 extern /*@notnull@*/ uentry
378 uentry_makePrivFunction2 (cstring p_n, ctype p_t,
380 /*@only@*/ globSet p_globs,
381 /*@only@*/ sRefSet p_mods, /*@keep@*/ fileloc p_f);
383 extern /*@notnull@*/ uentry
384 uentry_makeSpecEnumConstant (cstring p_n, ctype p_t, /*@keep@*/ fileloc p_loc) /*@*/ ;
386 extern /*@notnull@*/ uentry
387 uentry_makeEnumTag (cstring p_n, ctype p_t, /*@only@*/ fileloc p_loc) /*@*/ ;
389 extern /*@notnull@*/ uentry
390 uentry_makeTypeListFunction (cstring p_n, typeIdSet p_access, /*@only@*/ fileloc p_f)
393 extern /*@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);
398 extern /*@notnull@*/ uentry
399 uentry_makeEnumConstant (cstring p_n, ctype p_t) /*@*/ ;
401 extern /*@notnull@*/ uentry
402 uentry_makeEnumInitializedConstant (cstring p_n, ctype p_t, exprNode p_expr) /*@*/ ;
404 extern /*@notnull@*/ /*@only@*/ uentry
405 uentry_makeConstant (/*@temp@*/ cstring p_n, ctype p_t, /*@keep@*/ fileloc p_f)
408 extern /*@only@*/ /*@notnull@*/ uentry
409 uentry_makeConstantValue (/*@temp@*/ cstring p_n, ctype p_t, /*@keep@*/ fileloc p_f,
410 bool p_priv, /*@only@*/ multiVal p_val)
413 extern /*@notnull@*/ /*@only@*/ uentry
414 uentry_makeMacroConstant (/*@temp@*/ cstring p_n, ctype p_t, /*@keep@*/ fileloc p_f)
417 extern /*@notnull@*/ /*@only@*/ uentry
418 uentry_makeDatatype (/*@temp@*/ cstring p_n, ctype p_t, ynm p_mut, qual p_abstract,
419 /*@only@*/ fileloc p_f) /*@*/ ;
420 extern /*@notnull@*/ /*@only@*/ uentry
421 uentry_makeDatatypeAux (/*@temp@*/ cstring p_n, ctype p_t, ynm p_mut,
422 qual p_abstract, /*@keep@*/ fileloc p_f, bool p_priv) /*@*/ ;
423 extern /*@notnull@*/ uentry uentry_makeElipsisMarker (void) /*@*/ ;
425 extern void uentry_makeVarFunction (/*@temp@*/ uentry p_ue) /*@modifies p_ue@*/ ;
426 extern void uentry_makeConstantFunction (/*@temp@*/ uentry p_ue) /*@modifies p_ue@*/ ;
428 extern bool uentry_isElipsisMarker (/*@sef@*/ uentry p_u) /*@*/ ;
429 # define uentry_isElipsisMarker(u) \
430 (uentry_isValid(u) && ekind_isElipsis ((u)->ukind))
432 extern /*@notnull@*/ uentry
433 uentry_makeEndIter (cstring p_n, /*@only@*/ fileloc p_f) /*@*/ ;
434 extern /*@notnull@*/ uentry
435 uentry_makeEnumTagLoc (cstring p_n, ctype p_t) /*@*/ ;
436 extern /*@notnull@*/ uentry
437 uentry_makeForwardFunction (cstring p_n, typeId p_access, /*@temp@*/ fileloc p_f) /*@*/ ;
439 extern /*@notnull@*/ uentry
440 uentry_makeFunction (cstring p_n, ctype p_t,
442 /*@only@*/ globSet p_globs, /*@only@*/ sRefSet p_mods,
443 /*@only@*/ warnClause p_warn,
444 /*@only@*/ fileloc p_f);
446 extern /*@notnull@*/ uentry
447 uentry_makeIter (cstring p_n, ctype p_ct, /*@only@*/ fileloc p_f) /*@*/ ;
448 extern /*@notnull@*/ uentry
449 uentry_makeParam (idDecl p_t, int p_i) /*@*/ ;
451 extern /*@notnull@*/ uentry
452 uentry_makeStructTag (cstring p_n, ctype p_t, /*@only@*/ fileloc p_loc);
453 extern /*@notnull@*/ uentry
454 uentry_makeStructTagLoc (cstring p_n, ctype p_t);
455 extern /*@notnull@*/ uentry
456 uentry_makeUnionTag (cstring p_n, ctype p_t, /*@only@*/ fileloc p_loc);
457 extern /*@notnull@*/ uentry
458 uentry_makeUnionTagLoc (cstring p_n, ctype p_t);
459 extern /*@notnull@*/ uentry
460 uentry_makeVariable (cstring p_n, ctype p_t, /*@keep@*/ fileloc p_f, bool p_isPriv);
461 extern /*@notnull@*/ /*@only@*/ uentry
462 uentry_makeVariableLoc (cstring p_n, ctype p_t);
464 extern /*@notnull@*/ /*@only@*/
465 uentry uentry_makeVariableParam (cstring p_n, ctype p_t, fileloc p_loc);
467 extern /*@notnull@*/ /*@only@*/
468 uentry uentry_makeVariableSrefParam (cstring p_n, ctype p_t, /*@only@*/ fileloc p_loc,
469 /*@exposed@*/ sRef p_s);
470 extern /*@notnull@*/ /*@only@*/
471 uentry uentry_makeIdFunction (idDecl p_id);
472 extern /*@notnull@*/ /*@only@*/
473 uentry uentry_makeIdDatatype (idDecl p_id);
474 extern /*@notnull@*/ /*@only@*/
475 uentry uentry_makeBoolDatatype (qual p_abstract);
476 extern void uentry_mergeDefinition (uentry p_old, /*@only@*/ uentry p_unew);
477 extern void uentry_mergeEntries (uentry p_spec, /*@only@*/ uentry p_def);
478 extern uentry uentry_nameCopy (/*@only@*/ cstring p_name, uentry p_e);
479 extern uentry uentry_undump (ekind p_kind, fileloc p_loc, char **p_s);
480 extern /*@observer@*/ uentryList uentry_getParams (uentry p_l) /*@*/ ;
481 extern void uentry_resetParams (uentry p_ue, /*@only@*/ uentryList p_pn)
482 /*@modifies p_ue@*/ ;
483 extern /*@observer@*/ globSet uentry_getGlobs (uentry p_l) /*@*/ ;
484 extern qual uentry_nullPred (uentry p_u);
485 extern void uentry_free (/*@only@*/ /*@only@*/ uentry p_e);
486 extern void uentry_setDatatype (uentry p_e, usymId p_uid);
488 extern void uentry_setDefined (/*@special@*/ uentry p_e, fileloc p_f)
489 /*@uses p_e->whereDefined, p_e->ukind, p_e->uname, p_e->info@*/
492 extern void uentry_checkDecl (void);
493 extern void uentry_clearDecl (void);
494 extern void uentry_setDeclared (uentry p_e, fileloc p_f);
495 extern void uentry_setDeclaredOnly (uentry p_e, /*@only@*/ fileloc p_f);
496 extern void uentry_setDeclaredForceOnly (uentry p_e, /*@only@*/ fileloc p_f);
497 extern void uentry_setFunctionDefined (uentry p_e, fileloc p_loc);
498 extern void uentry_setName (uentry p_e, /*@only@*/ cstring p_n);
499 extern void uentry_setParam (uentry p_e);
500 extern void uentry_setSref (uentry p_e, /*@exposed@*/ sRef p_s);
501 extern void uentry_setStatic (uentry p_c);
503 extern void uentry_setModifies (uentry p_ue, /*@owned@*/ sRefSet p_sr)
504 /*@modifies p_ue, p_sr@*/;
506 extern bool uentry_hasWarning (uentry p_ue) /*@*/ ;
508 extern void uentry_addWarning (uentry p_ue, /*@only@*/ warnClause p_warn)
511 extern void uentry_setStateClauseList (uentry p_ue, /*@only@*/ stateClauseList p_clauses)
512 /*@modifies p_ue@*/ ;
514 extern void uentry_setType (uentry p_e, ctype p_t);
516 extern /*@unused@*/ /*@observer@*/ cstring uentry_checkedName (uentry p_ue);
517 extern void uentry_showWhereLastPlain (uentry p_spec) /*@modifies g_warningstream@*/ ;
520 uentry_showWhereSpecifiedExtra (uentry p_spec, /*@only@*/ cstring p_s)
521 /*@modifies g_warningstream@*/ ;
523 extern void uentry_showWhereSpecified (uentry p_spec) /*@modifies g_warningstream@*/ ;
524 extern void uentry_showWhereLast (uentry p_spec) /*@modifies g_warningstream@*/ ;
525 extern void uentry_showWhereDeclared (uentry p_spec) /*@modifies g_warningstream@*/ ;
527 extern /*@notnull@*/ /*@only@*/ uentry uentry_makeIdVariable (idDecl p_t) /*@*/ ;
528 extern uentry uentry_copy (uentry p_e) /*@*/ ;
529 extern uentry uentry_copyNoSave (uentry p_e) /*@*/ ; /* for use for uentries that do not live beyond function exits */
530 extern void uentry_freeComplete (/*@only@*/ uentry p_e) ;
531 extern void uentry_clearDefined (uentry p_e) /*@modifies p_e@*/;
532 extern /*@observer@*/ cstring uentry_specDeclName (uentry p_u) /*@*/ ;
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@*/ ;
539 extern void uentry_setState (uentry p_res, uentry p_other)
540 /*@modifies p_res, p_other@*/ ;
542 extern void uentry_setRefParam (uentry p_e) /*@modifies p_e@*/ ;
544 extern void uentry_setDeclaredForce (uentry p_e, fileloc p_f) /*@modifies p_e@*/;
545 extern bool uentry_isNonLocal (uentry p_ue) /*@*/ ;
546 extern bool uentry_isGlobalVariable (uentry p_ue) /*@*/;
547 extern bool uentry_isVisibleExternally (uentry p_ue) /*@*/;
548 extern bool uentry_isRefParam (uentry p_u) /*@*/ ;
549 extern bool uentry_hasGlobs (uentry p_ue) /*@*/ ;
550 extern bool uentry_hasMods (uentry p_ue) /*@*/ ;
552 extern bool uentry_hasStateClauseList (uentry p_ue) /*@*/ ;
553 extern bool uentry_hasConditions (uentry p_ue) /*@*/ ;
555 extern exitkind uentry_getExitCode (uentry p_ue) /*@*/ ;
557 extern void uentry_checkYieldParam (uentry p_old, uentry p_unew);
558 extern bool uentry_isOnly (uentry p_ue) /*@*/ ;
559 extern bool uentry_isUnique (uentry p_ue) /*@*/ ;
560 extern void uentry_reflectQualifiers (uentry p_ue, qualList p_q) /*@modifies p_ue@*/;
561 extern bool uentry_isOut (uentry p_u) /*@*/ ;
562 extern bool uentry_isPartial (uentry p_u) /*@*/ ;
563 extern bool uentry_isStateSpecial (uentry p_u) /*@*/ ;
564 extern bool uentry_possiblyNull (uentry p_u) /*@*/ ;
565 extern ctype uentry_getForceRealType (uentry p_e) /*@globals internalState@*/ ;
566 extern alkind uentry_getAliasKind (uentry p_u) /*@*/ ;
567 extern exkind uentry_getExpKind (uentry p_u) /*@*/ ;
568 extern /*@observer@*/ multiVal uentry_getConstantValue (uentry p_e) /*@*/ ;
569 extern void uentry_fixupSref (uentry p_ue) /*@modifies p_ue@*/ ;
570 extern void uentry_setGlobals (uentry p_ue, /*@only@*/ globSet p_globs) /*@modifies p_ue, p_globs@*/ ;
571 extern bool uentry_isYield (uentry p_ue) /*@*/ ;
572 extern /*@notnull@*/ uentry uentry_makeIdConstant (idDecl p_t) /*@*/ ;
573 extern /*@observer@*/ cstring uentry_getRealName (uentry p_e) /*@*/ ;
574 extern int uentry_xcomparealpha (uentry *p_p1, uentry *p_p2) /*@*/ ;
575 extern int uentry_xcompareuses (uentry *p_p1, uentry *p_p2) /*@*/ ;
576 extern /*@observer@*/ cstring uentry_specOrDefName (uentry p_u) /*@*/ ;
577 extern void uentry_copyState (uentry p_res, uentry p_other);
578 extern bool uentry_sameKind (uentry p_u1, uentry p_u2);
579 extern /*@exposed@*/ sRef uentry_returnedRef (uentry p_u, exprNodeList p_args, fileloc p_loc);
580 extern bool uentry_isReturned (uentry p_u);
581 extern bool uentry_isRefCountedDatatype (uentry p_e);
582 extern sstate uentry_getDefState (uentry p_u);
583 extern /*@unused@*/ void uentry_markFree (/*@owned@*/ uentry p_u);
584 extern /*@dependent@*/ sRef uentry_getOrigSref (uentry p_e);
585 extern void uentry_destroyMod (void) /*@modifies internalState@*/;
586 extern void uentry_showDefSpecInfo (uentry p_ce, fileloc p_fwhere);
587 extern void uentry_markOwned (/*@owned@*/ uentry p_u);
589 extern /*@observer@*/ fileloc uentry_whereLast (uentry p_e) /*@*/ ;
590 extern void uentry_setParamNo (uentry p_ue, int p_pno) /*@modifies p_ue@*/;
592 extern /*@observer@*/ filelocList uentry_getUses (/*@sef@*/ uentry p_e) /*@*/ ;
593 # define uentry_getUses(u) (uentry_isValid (u) ? (u)->uses : filelocList_undefined)
595 extern bool uentry_isCheckedUnknown (uentry p_ue) /*@*/ ;
596 extern bool uentry_isCheckedModify (uentry p_ue) /*@*/ ;
597 extern bool uentry_isUnchecked (uentry p_ue) /*@*/ ;
598 extern bool uentry_isChecked (uentry p_ue) /*@*/ ;
599 extern bool uentry_isCheckMod (uentry p_ue) /*@*/ ;
600 extern bool uentry_isCheckedStrict (uentry p_ue) /*@*/ ;
601 extern void uentry_setUnchecked (uentry p_ue) /*@modifies p_ue@*/ ;
602 extern void uentry_setChecked (uentry p_ue) /*@modifies p_ue@*/ ;
603 extern void uentry_setCheckMod (uentry p_ue) /*@modifies p_ue@*/ ;
604 extern void uentry_setCheckedStrict (uentry p_ue) /*@modifies p_ue@*/ ;
606 extern bool uentry_hasAccessType (uentry p_e);
608 /*@constant cstring GLOBAL_MARKER_NAME@*/
609 # define GLOBAL_MARKER_NAME cstring_makeLiteralTemp ("#GM#")
611 /* functions for making modification to null-term info */
612 extern void uentry_setNullTerminatedState (uentry p_e);
613 extern void uentry_setPossiblyNullTerminatedState (uentry p_e);
614 extern void uentry_setSize(uentry p_e, int p_size);
615 extern void uentry_setLen(uentry p_e, int p_len);
619 extern bool uentry_hasBufStateInfo (uentry p_ue);
620 # define uentry_hasBufStateInfo(p_ue) \
621 (((p_ue)->info->var->bufinfo != NULL) ? TRUE : FALSE)
623 /*@unused@*/ extern bool uentry_isNullTerminated(/*@sef@*/uentry p_ue);
624 # define uentry_isNullTerminated(p_ue) \
625 ( uentry_hasBufStateInfo((p_ue ) ) ? ((p_ue)->info->var->bufinfo->bufstate \
626 == BB_NULLTERMINATED) : FALSE)
628 /*@unused@*/ extern bool uentry_isPossiblyNullTerminated( /*@sef@*/ uentry p_ue);
629 # define uentry_isPossiblyNullTerminated(p_ue) \
630 ( uentry_hasBufStateInfo((p_ue)) ? ((p_ue)->info->var->bufinfo->bufstate \
631 == BB_POSSIBLYNULLTERMINATED) : FALSE)
633 /*@unused@*/ extern bool uentry_isNotNullTerminated( /*@sef@*/ uentry p_ue);
634 # define uentry_isNotNullTerminated(p_ue) \
635 ( uentry_hasBufStateInfo((p_ue) ) ? ((p_ue)->info->var->bufinfo->bufstate \
636 == BB_NOTNULLTERMINATED) : FALSE)
639 /* end modifications */
641 extern uentry uentry_makeGlobalMarker (void) ;
642 extern bool uentry_isGlobalMarker (uentry) /*@*/ ;
644 extern /*@exposed@*/ uentry uentry_makeUnrecognized (cstring p_c, /*@only@*/ fileloc p_loc);
649 AN_UNKNOWN, AN_FCNRETURN, AN_FCNPARAM, AN_SUFIELD, AN_TDEFN, AN_GSVAR,
653 extern void initAnnots ();
654 extern void printAnnots (void);
655 extern void uentry_tallyAnnots (uentry u, ancontext kind);
656 # endif /* DOANNOTS */
658 extern bool uentry_hasMetaStateEnsures (uentry p_e) /*@*/ ;
659 extern /*@only@*/ metaStateConstraintList uentry_getMetaStateEnsures (uentry p_e);
661 /* start modifications */
664 extern constraintList uentry_getFcnPreconditions (uentry p_ue);
665 extern constraintList uentry_getFcnPostconditions (uentry p_ue);
667 extern void uentry_setPostconditions (uentry p_ue, /*@only@*/ functionConstraint p_postconditions);
669 extern void uentry_setPreconditions (uentry p_ue, /*@only@*/ functionConstraint p_preconditions);
673 ** For debugging only
677 extern void uentry_checkValid (uentry p_ue) /*@modifies g_errorstream@*/ ;
681 # error "Multiple include"