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 670