src/Headers/uentry.h

   1 /*
   2 ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2003.
   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
  18 typedef struct
  19 {
  20   typeIdSet access;
  21   bool macro;
  22 } *ucinfo;
  23
  24 typedef 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
  40 typedef enum
  41 {
  42   CH_UNKNOWN,
  43   CH_UNCHECKED,
  44   CH_CHECKED,
  45   CH_CHECKMOD,
  46   CH_CHECKEDSTRICT
  47 } chkind;
  48
  49 /* start modifications */
  50 typedef enum  {
  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
  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 */
  60 } *bbufinfo ;
  61
  62 typedef struct
  63 {
  64   vkind   kind;      /* kind (parameter, specified) */
  65   chkind  checked;   /* how is it checked */
  66   sstate  defstate;
  67   nstate  nullstate;
  68   bbufinfo bufinfo; /* is valid only if the entry is a variable and (a pointer
  69                        or array) */
  70 } *uvinfo ;
  71 /* end modifications */
  72
  73 typedef struct
  74 {
  75   qual abs; /* oneof QU_UNKNOWN, QU_ABSTRACT, QU_NUMABSTRACT, QU_CONCRETE */
  76   ynm   mut;
  77   ctype type;
  78 } *udinfo ;
  79
  80 /* information for specified functions */
  81
  82 typedef enum
  83 {
  84   SPC_NONE,
  85   SPC_PRINTFLIKE,
  86   SPC_SCANFLIKE,
  87   SPC_MESSAGELIKE,
  88   SPC_LAST
  89 } specCode;
  90
  91 typedef struct
  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
 101   stateClauseList specclauses;
 102
 103   /*@dependent@*/ uentryList defparams;
 104   bool hasGlobs BOOLBITS;
 105   bool hasMods  BOOLBITS;
 106
 107   functionConstraint preconditions;
 108   functionConstraint postconditions;
 109
 110 } *ufinfo ;
 111
 112 typedef struct
 113 {
 114                   typeIdSet  access;
 115   /*@owned@*/     globSet     globs;      /* globals list */
 116   /*@owned@*/     sRefSet     mods;       /* modifies */
 117 } *uiinfo ;
 118
 119 typedef struct
 120 {
 121   typeIdSet access;
 122 } *ueinfo ;
 123
 124 typedef union
 125 {
 126   ucinfo uconst;
 127   uvinfo var;
 128   udinfo datatype;
 129   ufinfo fcn;
 130   uiinfo iter;
 131   ueinfo enditer;
 132 } *uinfo ;
 133
 134 struct s_uentry
 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   */
 149
 150   /*@exposed@*/ /*@null@*/ sRef sref;
 151
 152   warnClause warn;
 153
 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
 169 ** uentry_isDefined).
 170 */
 171
 172 extern /*@nullwhentrue@*/ bool uentry_isUndefined (/*@special@*/ uentry p_e)
 173    /*@*/ ;
 174 extern /*@nullwhentrue@*/ bool uentry_isInvalid (/*@special@*/ uentry p_e)
 175    /*@*/ ;
 176 extern /*@falsewhennull@*/ bool uentry_isValid (/*@special@*/ uentry p_e)
 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
 186 extern int uentry_compareStrict (uentry p_v1, uentry p_v2);
 187
 188 /*@constant int PARAMUNKNOWN; @*/
 189 # define PARAMUNKNOWN -1
 190
 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@*/ ;
 195
 196 extern /*@falsewhennull@*/ bool uentry_isLset (/*@sef@*/ uentry p_e);
 197 # define uentry_isLset(e) \
 198   (uentry_isValid(e) && (e)->lset)
 199
 200 extern /*@falsewhennull@*/ bool uentry_isUsed (/*@sef@*/ uentry p_e);
 201 # define uentry_isUsed(e)         (uentry_isValid(e) && (e)->used)
 202
 203 extern /*@unused@*/ /*@falsewhennull@*/ bool
 204   uentry_isAbstractType (uentry p_e) /*@*/ ;
 205 # define uentry_isAbstractType(e) (uentry_isAbstractDatatype(e))
 206
 207 extern /*@falsewhennull@*/ bool uentry_isConstant (/*@sef@*/ uentry p_e) /*@*/ ;
 208 # define uentry_isConstant(e) \
 209   (uentry_isValid(e) && ekind_isConst ((e)->ukind))
 210
 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)))
 214
 215 extern /*@falsewhennull@*/ bool uentry_isEnumConstant (/*@sef@*/ uentry p_e) /*@*/ ;
 216 # define uentry_isEnumConstant(e) \
 217   (uentry_isValid(e) && ekind_isEnumConst ((e)->ukind))
 218
 219 extern /*@falsewhennull@*/ bool uentry_isExternal (/*@sef@*/ uentry p_e) /*@*/ ;
 220 # define uentry_isExternal(c) \
 221   (uentry_isValid(c) && fileloc_isExternal (uentry_whereDefined (c)))
 222
 223 extern /*@falsewhennull@*/ bool uentry_isExtern (/*@sef@*/ uentry p_e) /*@*/ ;
 224 # define uentry_isExtern(c) \
 225   (uentry_isValid(c) && (c)->storageclass == SCEXTERN)
 226
 227 extern bool uentry_isForward (uentry p_e) /*@*/ ;
 228
 229 extern /*@falsewhennull@*/ bool uentry_isFunction (/*@sef@*/ uentry p_e) /*@*/ ;
 230 # define uentry_isFunction(e) \
 231   (uentry_isValid(e) && ekind_isFunction ((e)->ukind))
 232
 233 extern /*@falsewhennull@*/ bool uentry_isPriv (/*@sef@*/ uentry p_e) /*@*/ ;
 234 # define uentry_isPriv(e) \
 235   (uentry_isValid(e) && (e)->isPrivate)
 236
 237 extern /*@falsewhennull@*/ bool uentry_isFileStatic (uentry p_ue) /*@*/ ;
 238 extern /*@falsewhennull@*/ bool uentry_isExported (uentry p_ue) /*@*/ ;
 239
 240 extern /*@falsewhennull@*/ bool uentry_isStatic (/*@sef@*/ uentry p_e) /*@*/ ;
 241 # define uentry_isStatic(c) \
 242   (uentry_isValid(c) && (c)->storageclass == SCSTATIC)
 243
 244 extern void uentry_setLset (/*@sef@*/ uentry p_e);
 245 # define uentry_setLset(e) \
 246   (uentry_isValid(e) ? (e)->lset = TRUE : TRUE)
 247
 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) /*@*/ ;
 252
 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@*/ ;
 256
 257 extern void uentry_checkName (uentry p_ue) /*@modifies g_warningstream, p_ue@*/ ;
 258
 259 extern bool uentry_sameObject (uentry p_e1, uentry p_e2);
 260 # define uentry_sameObject(e1,e2) ((e1) == (e2))
 261
 262 extern void uentry_addAccessType (uentry p_ue, typeId p_tid) /*@modifies p_ue@*/ ;
 263
 264 extern void uentry_showWhereAny (uentry p_spec)
 265      /*@modifies g_warningstream@*/ ;
 266
 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);
 272
 273 extern void uentry_setNotUsed (/*@sef@*/ uentry p_e);
 274 # define uentry_setNotUsed(e) \
 275   (uentry_isValid (e) ? (e)->used = FALSE : FALSE)
 276
 277 extern bool uentry_wasUsed (/*@sef@*/ uentry p_e);
 278 # define uentry_wasUsed(e) \
 279   (uentry_isValid (e) ? (e)->used : TRUE)
 280
 281 extern void uentry_mergeConstantValue (uentry p_ue, /*@only@*/ multiVal p_m);
 282
 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@*/
 292    /*@*/ ;
 293 extern /*@falsewhennull@*/ bool uentry_isDatatype (uentry p_e) /*@*/ ;
 294
 295 extern /*@falsewhennull@*/ bool uentry_isCodeDefined (uentry p_e) /*@*/ ;
 296
 297 extern /*@falsewhennull@*/ bool uentry_isDeclared (/*@special@*/ uentry p_e)
 298    /*@uses p_e->whereDeclared@*/ /*@*/ ;
 299
 300 extern /*@observer@*/ cstring uentry_ekindName (uentry p_ue) /*@*/ ;
 301 extern /*@observer@*/ cstring uentry_ekindNameLC (uentry p_ue) /*@*/ ;
 302
 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@*/
 315    /*@*/ ;
 316
 317 extern /*@falsewhennull@*/ bool uentry_isRealFunction (uentry p_e) /*@*/ ;
 318 extern /*@falsewhennull@*/ bool uentry_isSpecified (uentry p_e) /*@*/ ;
 319
 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@*/ /*@*/ ;
 324
 325 extern /*@falsewhennull@*/ bool uentry_isVar (/*@special@*/ uentry p_e)
 326    /*@uses p_e->ukind@*/
 327    /*@*/ ;
 328
 329 extern /*@falsewhennull@*/ bool uentry_isVariable (/*@special@*/ uentry p_e)
 330    /*@uses p_e->ukind@*/
 331    /*@*/ ;
 332
 333 extern cstring uentry_dump (uentry p_v) ;
 334 extern cstring uentry_dumpParam (uentry p_v);
 335
 336 extern /*@observer@*/ cstring uentry_observeRealName (uentry p_e) /*@*/ ;
 337
 338 extern cstring uentry_getName (/*@special@*/ uentry p_e)
 339    /*@uses p_e->ukind, p_e->info, p_e->uname@*/
 340    /*@*/ ;
 341
 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
 358 extern /*@exposed@*/ uentry uentry_makeUnrecognized (cstring p_c, /*@only@*/ fileloc p_loc);
 359 extern /*@notnull@*/ uentry uentry_makeExpandedMacro (cstring p_s,
 360                                                       /*@temp@*/ fileloc p_f)
 361   /*@*/ ;
 362
 363 extern void uentry_checkMatchParam (uentry p_u1, uentry p_u2, int p_paramno, exprNode p_e) /*@modifies g_warningstream@*/ ;
 364
 365 extern /*@observer@*/ stateClauseList uentry_getStateClauseList (uentry p_ue) /*@*/ ;
 366
 367 extern void uentry_showWhereLastExtra (uentry p_spec, /*@only@*/ cstring p_extra)
 368    /*@modifies g_warningstream@*/ ;
 369
 370 extern void uentry_setRefCounted (uentry p_e);
 371
 372 extern /*@notnull@*/ /*@only@*/ uentry uentry_makeUnnamedVariable (ctype p_t);
 373 extern /*@falsewhennull@*/ bool uentry_isUnnamedVariable (uentry) /*@*/;
 374
 375 extern /*@notnull@*/ uentry
 376   uentry_makeUnspecFunction (cstring p_n, ctype p_t, typeIdSet p_access,
 377                              /*@keep@*/ fileloc p_f);
 378
 379 extern /*@notnull@*/ uentry
 380   uentry_makePrivFunction2 (cstring p_n, ctype p_t,
 381                             typeIdSet p_access,
 382                             /*@only@*/ globSet p_globs,
 383                             /*@only@*/ sRefSet p_mods, /*@keep@*/ fileloc p_f);
 384
 385 extern /*@notnull@*/ uentry
 386   uentry_makeSpecEnumConstant (cstring p_n, ctype p_t, /*@keep@*/ fileloc p_loc) /*@*/ ;
 387
 388 extern /*@notnull@*/ uentry
 389   uentry_makeEnumTag (cstring p_n, ctype p_t, /*@only@*/ fileloc p_loc) /*@*/ ;
 390
 391 extern /*@notnull@*/ uentry
 392   uentry_makeTypeListFunction (cstring p_n, typeIdSet p_access, /*@only@*/ fileloc p_f)
 393   /*@*/ ;
 394
 395 extern /*@notnull@*/ uentry
 396   uentry_makeSpecFunction (cstring p_n, ctype p_t,
 397                            typeIdSet p_access, /*@only@*/ globSet p_globs,
 398                            /*@only@*/ sRefSet p_mods, /*@keep@*/ fileloc p_f);
 399
 400 extern /*@notnull@*/ uentry
 401   uentry_makeEnumConstant (cstring p_n, ctype p_t) /*@*/ ;
 402
 403 extern /*@notnull@*/ uentry
 404   uentry_makeEnumInitializedConstant (cstring p_n, ctype p_t, exprNode p_expr) /*@*/ ;
 405
 406 extern /*@notnull@*/ /*@only@*/ uentry
 407   uentry_makeConstant (/*@temp@*/ cstring p_n, ctype p_t, /*@keep@*/ fileloc p_f)
 408   /*@*/ ;
 409
 410 extern /*@only@*/ /*@notnull@*/ uentry
 411   uentry_makeConstantValue (/*@temp@*/ cstring p_n, ctype p_t, /*@keep@*/ fileloc p_f,
 412                             bool p_priv, /*@only@*/ multiVal p_val)
 413   /*@*/ ;
 414
 415 extern /*@notnull@*/ /*@only@*/ uentry
 416   uentry_makeMacroConstant (/*@temp@*/ cstring p_n, ctype p_t, /*@keep@*/ fileloc p_f)
 417   /*@*/ ;
 418
 419 extern /*@notnull@*/ /*@only@*/ uentry
 420   uentry_makeDatatype (/*@temp@*/ cstring p_n, ctype p_t, ynm p_mut, qual p_abstract,
 421                        /*@only@*/ fileloc p_f) /*@*/ ;
 422 extern /*@notnull@*/ /*@only@*/ uentry
 423   uentry_makeDatatypeAux (/*@temp@*/ cstring p_n, ctype p_t, ynm p_mut,
 424                           qual p_abstract, /*@keep@*/ fileloc p_f, bool p_priv) /*@*/ ;
 425 extern /*@notnull@*/ uentry uentry_makeElipsisMarker (void) /*@*/ ;
 426
 427 extern void uentry_makeVarFunction (/*@temp@*/ uentry p_ue) /*@modifies p_ue@*/ ;
 428 extern void uentry_makeConstantFunction (/*@temp@*/ uentry p_ue) /*@modifies p_ue@*/ ;
 429
 430 extern bool uentry_isElipsisMarker (/*@sef@*/ uentry p_u) /*@*/ ;
 431 # define uentry_isElipsisMarker(u) \
 432   (uentry_isValid(u) && ekind_isElipsis ((u)->ukind))
 433
 434 extern /*@notnull@*/ uentry
 435   uentry_makeEndIter (cstring p_n, /*@only@*/ fileloc p_f) /*@*/ ;
 436 extern /*@notnull@*/ uentry
 437   uentry_makeEnumTagLoc (cstring p_n, ctype p_t) /*@*/ ;
 438 extern /*@notnull@*/ uentry
 439   uentry_makeForwardFunction (cstring p_n, typeId p_access, /*@temp@*/ fileloc p_f) /*@*/ ;
 440
 441 extern /*@notnull@*/ uentry
 442   uentry_makeFunction (cstring p_n, ctype p_t,
 443                        typeId p_access,
 444                        /*@only@*/ globSet p_globs, /*@only@*/ sRefSet p_mods,
 445                        /*@only@*/ warnClause p_warn,
 446                        /*@only@*/ fileloc p_f);
 447
 448 extern /*@notnull@*/ uentry
 449   uentry_makeIter (cstring p_n, ctype p_ct, /*@only@*/ fileloc p_f) /*@*/ ;
 450 extern /*@notnull@*/ uentry
 451   uentry_makeParam (idDecl p_t, int p_i) /*@*/ ;
 452
 453 extern /*@notnull@*/ uentry
 454   uentry_makeStructTag (cstring p_n, ctype p_t, /*@only@*/ fileloc p_loc);
 455 extern /*@notnull@*/ uentry
 456   uentry_makeStructTagLoc (cstring p_n, ctype p_t);
 457 extern /*@notnull@*/ uentry
 458   uentry_makeUnionTag (cstring p_n, ctype p_t, /*@only@*/ fileloc p_loc);
 459 extern /*@notnull@*/ uentry
 460   uentry_makeUnionTagLoc (cstring p_n, ctype p_t);
 461 extern /*@notnull@*/ uentry
 462   uentry_makeVariable (cstring p_n, ctype p_t, /*@keep@*/ fileloc p_f, bool p_isPriv);
 463 extern /*@notnull@*/ /*@only@*/ uentry
 464   uentry_makeVariableLoc (cstring p_n, ctype p_t);
 465
 466 extern /*@notnull@*/ /*@only@*/
 467   uentry uentry_makeVariableParam (cstring p_n, ctype p_t, fileloc p_loc);
 468
 469 extern /*@notnull@*/ /*@only@*/
 470 uentry uentry_makeVariableSrefParam (cstring p_n, ctype p_t, /*@only@*/ fileloc p_loc,
 471                                      /*@exposed@*/ sRef p_s);
 472 extern /*@notnull@*/ /*@only@*/
 473   uentry uentry_makeIdFunction (idDecl p_id);
 474 extern /*@notnull@*/ /*@only@*/
 475   uentry uentry_makeIdDatatype (idDecl p_id);
 476 extern /*@notnull@*/ /*@only@*/
 477   uentry uentry_makeBoolDatatype (qual p_abstract);
 478 extern void uentry_mergeDefinition (uentry p_old, /*@only@*/ uentry p_unew);
 479 extern void uentry_mergeEntries (uentry p_spec, /*@only@*/ uentry p_def);
 480 extern uentry uentry_nameCopy (/*@only@*/ cstring p_name, uentry p_e);
 481 extern uentry uentry_undump (ekind p_kind, fileloc p_loc, char **p_s);
 482 extern /*@observer@*/ uentryList uentry_getParams (uentry p_l) /*@*/ ;
 483 extern void uentry_resetParams (uentry p_ue, /*@only@*/ uentryList p_pn)
 484                /*@modifies p_ue@*/ ;
 485 extern /*@observer@*/ globSet uentry_getGlobs (uentry p_l) /*@*/ ;
 486 extern qual uentry_nullPred (uentry p_u);
 487 extern void uentry_free (/*@only@*/ /*@only@*/ uentry p_e);
 488 extern void uentry_setDatatype (uentry p_e, typeId p_uid);
 489
 490 extern void uentry_setDefined (/*@special@*/ uentry p_e, fileloc p_f)
 491    /*@uses p_e->whereDefined, p_e->ukind, p_e->uname, p_e->info@*/
 492    /*@modifies p_e@*/ ;
 493
 494 extern void uentry_checkDecl (void);
 495 extern void uentry_clearDecl (void);
 496 extern void uentry_setDeclared (uentry p_e, fileloc p_f);
 497 extern void uentry_setDeclaredOnly (uentry p_e, /*@only@*/ fileloc p_f);
 498 extern void uentry_setDeclaredForceOnly (uentry p_e, /*@only@*/ fileloc p_f);
 499 extern void uentry_setFunctionDefined (uentry p_e, fileloc p_loc);
 500 extern void uentry_setName (uentry p_e, /*@only@*/ cstring p_n);
 501 extern void uentry_setParam (uentry p_e);
 502 extern void uentry_setSref (uentry p_e, /*@exposed@*/ sRef p_s);
 503 extern void uentry_setStatic (uentry p_c);
 504
 505 extern void uentry_setModifies (uentry p_ue, /*@owned@*/ sRefSet p_sr)
 506    /*@modifies p_ue, p_sr@*/;
 507
 508 extern bool uentry_hasWarning (uentry p_ue) /*@*/ ;
 509
 510 extern void uentry_addWarning (uentry p_ue, /*@only@*/ warnClause p_warn)
 511    /*@modifies p_ue*/;
 512
 513 extern void uentry_setStateClauseList (uentry p_ue, /*@only@*/ stateClauseList p_clauses)
 514    /*@modifies p_ue@*/ ;
 515
 516 extern void uentry_setType (uentry p_e, ctype p_t);
 517
 518 extern /*@unused@*/ /*@observer@*/ cstring uentry_checkedName (uentry p_ue);
 519 extern void uentry_showWhereLastPlain (uentry p_spec) /*@modifies g_warningstream@*/ ;
 520
 521 extern void
 522   uentry_showWhereSpecifiedExtra (uentry p_spec, /*@only@*/ cstring p_s)
 523   /*@modifies g_warningstream@*/ ;
 524
 525 extern void uentry_showWhereSpecified (uentry p_spec) /*@modifies g_warningstream@*/ ;
 526 extern void uentry_showWhereLast (uentry p_spec) /*@modifies g_warningstream@*/ ;
 527 extern void uentry_showWhereDeclared (uentry p_spec) /*@modifies g_warningstream@*/ ;
 528
 529 extern /*@notnull@*/ /*@only@*/ uentry uentry_makeIdVariable (idDecl p_t) /*@*/ ;
 530 extern uentry uentry_copy (uentry p_e) /*@*/ ;
 531 extern uentry uentry_copyNoSave (uentry p_e) /*@*/ ; /* for use for uentries that do not live beyond function exits */
 532 extern void uentry_freeComplete (/*@only@*/ uentry p_e) ;
 533 extern void uentry_clearDefined (uentry p_e) /*@modifies p_e@*/;
 534 extern /*@observer@*/ cstring uentry_specDeclName (uentry p_u) /*@*/ ;
 535
 536 extern void
 537   uentry_mergeState (uentry p_res, uentry p_other, fileloc p_loc,
 538                      bool p_mustReturn, bool p_flip, bool p_opt,
 539                      clause p_cl) /*@modifies p_res, p_other@*/ ;
 540
 541 extern void uentry_setState (uentry p_res, uentry p_other)
 542    /*@modifies p_res, p_other@*/ ;
 543
 544 extern void uentry_setRefParam (uentry p_e) /*@modifies p_e@*/ ;
 545
 546 extern void uentry_setDeclaredForce (uentry p_e, fileloc p_f) /*@modifies p_e@*/;
 547 extern bool uentry_isNonLocal (uentry p_ue) /*@*/ ;
 548 extern bool uentry_isGlobalVariable (uentry p_ue) /*@*/;
 549 extern bool uentry_isVisibleExternally (uentry p_ue) /*@*/;
 550 extern bool uentry_isRefParam (uentry p_u) /*@*/ ;
 551 extern bool uentry_hasGlobs (uentry p_ue) /*@*/ ;
 552 extern bool uentry_hasMods (uentry p_ue) /*@*/ ;
 553
 554 extern bool uentry_hasStateClauseList (uentry p_ue) /*@*/ ;
 555 extern bool uentry_hasConditions (uentry p_ue) /*@*/ ;
 556
 557 extern exitkind uentry_getExitCode (uentry p_ue) /*@*/ ;
 558
 559 extern void uentry_checkYieldParam (uentry p_old, uentry p_unew);
 560 extern bool uentry_isOnly (uentry p_ue) /*@*/ ;
 561 extern bool uentry_isUnique (uentry p_ue) /*@*/ ;
 562 extern void uentry_reflectQualifiers (uentry p_ue, qualList p_q) /*@modifies p_ue@*/;
 563 extern bool uentry_isOut (uentry p_u) /*@*/ ;
 564 extern bool uentry_isPartial (uentry p_u) /*@*/ ;
 565 extern bool uentry_isStateSpecial (uentry p_u) /*@*/ ;
 566 extern bool uentry_possiblyNull (uentry p_u) /*@*/ ;
 567 extern ctype uentry_getForceRealType (uentry p_e) /*@globals internalState@*/ ;
 568 extern alkind uentry_getAliasKind (uentry p_u) /*@*/ ;
 569 extern exkind uentry_getExpKind (uentry p_u) /*@*/ ;
 570 extern /*@observer@*/ multiVal uentry_getConstantValue (uentry p_e) /*@*/ ;
 571 extern void uentry_fixupSref (uentry p_ue) /*@modifies p_ue@*/ ;
 572 extern void uentry_setGlobals (uentry p_ue, /*@only@*/ globSet p_globs) /*@modifies p_ue, p_globs@*/ ;
 573 extern bool uentry_isYield (uentry p_ue) /*@*/ ;
 574 extern /*@notnull@*/ uentry uentry_makeIdConstant (idDecl p_t) /*@*/ ;
 575 extern /*@observer@*/ cstring uentry_getRealName (uentry p_e) /*@*/ ;
 576 extern int uentry_xcomparealpha (uentry *p_p1, uentry *p_p2) /*@*/ ;
 577 extern int uentry_xcompareuses (uentry *p_p1, uentry *p_p2) /*@*/ ;
 578 extern /*@observer@*/ cstring uentry_specOrDefName (uentry p_u) /*@*/ ;
 579 extern void uentry_copyState (uentry p_res, uentry p_other);
 580 extern bool uentry_sameKind (uentry p_u1, uentry p_u2);
 581 extern /*@exposed@*/ sRef uentry_returnedRef (uentry p_u, exprNodeList p_args, fileloc p_loc);
 582 extern bool uentry_isReturned (uentry p_u);
 583 extern bool uentry_isRefCountedDatatype (uentry p_e);
 584 extern sstate uentry_getDefState (uentry p_u);
 585 extern /*@unused@*/ void uentry_markFree (/*@owned@*/ uentry p_u);
 586 extern /*@dependent@*/ sRef uentry_getOrigSref (uentry p_e);
 587 extern void uentry_destroyMod (void) /*@modifies internalState@*/;
 588 extern void uentry_showDefSpecInfo (uentry p_ce, fileloc p_fwhere);
 589 extern void uentry_markOwned (/*@owned@*/ uentry p_u);
 590
 591 extern /*@observer@*/ fileloc uentry_whereLast (uentry p_e) /*@*/ ;
 592 extern void uentry_setParamNo (uentry p_ue, int p_pno) /*@modifies p_ue@*/;
 593
 594 extern /*@observer@*/ filelocList uentry_getUses (/*@sef@*/ uentry p_e) /*@*/ ;
 595 # define uentry_getUses(u) (uentry_isValid (u) ? (u)->uses : filelocList_undefined)
 596
 597 extern bool uentry_isCheckedUnknown (uentry p_ue) /*@*/ ;
 598 extern bool uentry_isCheckedModify (uentry p_ue) /*@*/ ;
 599 extern bool uentry_isUnchecked (uentry p_ue) /*@*/ ;
 600 extern bool uentry_isChecked (uentry p_ue) /*@*/ ;
 601 extern bool uentry_isCheckMod (uentry p_ue) /*@*/ ;
 602 extern bool uentry_isCheckedStrict (uentry p_ue) /*@*/ ;
 603 extern void uentry_setUnchecked (uentry p_ue) /*@modifies p_ue@*/ ;
 604 extern void uentry_setChecked (uentry p_ue) /*@modifies p_ue@*/ ;
 605 extern void uentry_setCheckMod (uentry p_ue) /*@modifies p_ue@*/ ;
 606 extern void uentry_setCheckedStrict (uentry p_ue) /*@modifies p_ue@*/ ;
 607
 608 extern bool uentry_hasAccessType (uentry p_e);
 609
 610 /*@constant cstring GLOBAL_MARKER_NAME@*/
 611 # define GLOBAL_MARKER_NAME cstring_makeLiteralTemp ("#GM#")
 612
 613 /* Null Termination */
 614
 615 extern void uentry_setNullTerminatedState (uentry p_e);
 616 extern void uentry_setPossiblyNullTerminatedState (uentry p_e);
 617 extern void uentry_setSize(uentry p_e, int p_size);
 618 extern void uentry_setLen(uentry p_e, int p_len);
 619
 620 extern /*@falsewhennull@*/ bool uentry_hasBufStateInfo (uentry p_ue) /*@*/ ;
 621 extern bool uentry_isNullTerminated (uentry p_ue) /*@*/ ;
 622 extern bool uentry_isPossiblyNullTerminated (uentry p_ue) /*@*/ ;
 623 extern bool uentry_isNotNullTerminated (uentry p_ue) /*@*/ ;
 624
 625 /* Global Markers */
 626
 627 extern uentry uentry_makeGlobalMarker (void) ;
 628 extern bool uentry_isGlobalMarker (uentry) /*@*/ ;
 629
 630 # ifdef DOANNOTS
 631 typedef enum
 632 {
 633   AN_UNKNOWN, AN_FCNRETURN, AN_FCNPARAM, AN_SUFIELD, AN_TDEFN, AN_GSVAR,
 634   AN_CONST, AN_LAST
 635 } ancontext;
 636
 637 extern void initAnnots ();
 638 extern void printAnnots (void);
 639 extern void uentry_tallyAnnots (uentry u, ancontext kind);
 640 # endif /* DOANNOTS */
 641
 642 extern bool uentry_hasMetaStateEnsures (uentry p_e) /*@*/ ;
 643 extern /*@only@*/ metaStateConstraintList uentry_getMetaStateEnsures (uentry p_e);
 644
 645 /* start modifications */
 646
 647 /*drl7x*/
 648 extern constraintList uentry_getFcnPreconditions (uentry p_ue);
 649 extern constraintList uentry_getFcnPostconditions (uentry p_ue);
 650
 651 extern void uentry_setPostconditions (uentry p_ue, /*@only@*/ functionConstraint p_postconditions);
 652
 653 extern void uentry_setPreconditions (uentry p_ue, /*@only@*/ functionConstraint p_preconditions);
 654 /*end mods*/
 655
 656 /*
 657 ** For debugging only
 658 */
 659
 660 # ifdef DEBUGSPLINT
 661 extern void uentry_checkValid (uentry p_ue) /*@modifies g_errorstream@*/ ;
 662 # endif
 663
 664 # else
 665 # error "Multiple include"
 666 # endif
 667
 668
 669