src/Headers/uentry.h

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