1 /* 2 ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2003. 3 ** See ../LICENSE for license information. 4 ** 5 */ 6 /* 7 ** storeRef.h 8 */ 9 10 # ifndef STOREREF_H 11 # define STOREREF_H 12 13 /* 14 ** note: forwardTypes defines sRef 15 */ 16 17 /* 18 ** kinds of storage references 19 */ 20 21 typedef enum { 22 SR_NOTHING, 23 SR_INTERNAL, 24 SR_SPECSTATE, 25 SR_SYSTEM, 26 SR_GLOBALMARKER 27 } speckind; 28 29 typedef enum { 30 SK_PARAM, 31 SK_ARRAYFETCH, 32 SK_FIELD, 33 SK_PTR, 34 SK_ADR, 35 SK_CONST, 36 SK_CVAR, 37 SK_UNCONSTRAINED, 38 SK_OBJECT, 39 SK_CONJ, 40 SK_EXTERNAL, 41 SK_DERIVED, 42 SK_NEW, 43 SK_TYPE, 44 SK_RESULT, 45 SK_SPECIAL, 46 SK_UNKNOWN 47 } skind; 48 49 typedef struct 50 { 51 int lexlevel; 52 usymId index; 53 } *cref; 54 55 typedef struct 56 { 57 /*@exposed@*/ /*@notnull@*/ sRef arr; 58 bool indknown; 59 int ind; 60 } *ainfo; 61 62 typedef struct 63 { 64 /*@exposed@*/ /*@notnull@*/ sRef rec; 65 /*@observer@*/ cstring field; 66 } *fldinfo ; 67 68 typedef struct 69 { 70 /*@exposed@*/ /*@notnull@*/ sRef a; 71 /*@exposed@*/ /*@notnull@*/ sRef b; 72 } *cjinfo ; 73 74 typedef union 75 { 76 /*@only@*/ cref cvar; 77 int paramno; 78 /*@only@*/ ainfo arrayfetch; 79 /*@only@*/ fldinfo field; 80 ctype object; 81 /*@observer@*/ cstring fname; /* unconstrained, new */ 82 /*@exposed@*/ /*@notnull@*/ sRef ref; 83 /*@only@*/ cjinfo conj; 84 speckind spec; 85 } *sinfo; 86 87 struct s_sRef 88 { 89 /* does it need to be inside parens (macros) */ 90 bool safe; 91 92 /* has it been modified */ 93 bool modified; /* BOOLBITS; */ 94 95 /* for debugging: make this sRef as immutable. */ 96 bool immut; /* BOOLBITS; */ 97 98 skind kind; 99 ctype type; 100 101 multiVal val; /* Some sRef's have known values */ 102 103 sstate defstate; 104 nstate nullstate; 105 106 /* start modifications: We keep a track of the buf state(nullterm info)*/ 107 struct s_bbufinfo bufinfo; 108 /* end modifications */ 109 110 alkind aliaskind; 111 alkind oaliaskind; 112 113 exkind expkind; /* exposed, observer, normal */ 114 exkind oexpkind; 115 116 /* where it becomes observer/exposed */ 117 /*@null@*/ /*@only@*/ stateInfo expinfo; 118 119 /* where it changed alias kind */ 120 /*@null@*/ /*@only@*/ stateInfo aliasinfo; 121 122 /* where it is defined/allocated */ 123 /*@null@*/ /*@only@*/ stateInfo definfo; 124 125 /* where it is null */ 126 /*@null@*/ /*@only@*/ stateInfo nullinfo; 127 128 /*@only@*/ /*@relnull@*/ sinfo info; 129 130 /* stores fields for structs, elements for arrays, derefs for pointers */ 131 /*@only@*/ sRefSet deriv; 132 133 /* sRef's include a lookup table of state variables. */ 134 /*@only@*/ valueTable state; 135 } ; 136 137 extern bool sRef_perhapsNull (sRef p_s); 138 extern bool sRef_possiblyNull (sRef p_s); 139 extern bool sRef_definitelyNull (sRef p_s); 140 141 extern bool sRef_definitelyNullContext (sRef p_s); 142 extern bool sRef_definitelyNullAltContext (sRef p_s); 143 144 extern void sRef_setNullError (sRef p_s); 145 extern void sRef_setNullUnknown (sRef p_s, fileloc p_loc); 146 extern void sRef_setNotNull (sRef p_s, fileloc p_loc); 147 extern void sRef_setNullState (sRef p_s, nstate p_n, fileloc p_loc); 148 extern void sRef_setNullStateInnerComplete (sRef p_s, nstate p_n, fileloc p_loc); 149 extern void sRef_setPosNull (sRef p_s, fileloc p_loc); 150 extern void sRef_setDefNull (sRef p_s, fileloc p_loc); 151 152 extern /*@nullwhentrue@*/ bool sRef_isInvalid (sRef p_s) /*@*/ ; 153 extern /*@falsewhennull@*/ bool sRef_isValid (sRef p_s) /*@*/ ; 154 extern /*@falsewhennull@*/ bool sRef_isReasonable (sRef p_s) /*@*/ ; 155 156 /*@constant null sRef sRef_undefined; @*/ 157 # define sRef_undefined ((sRef) NULL) 158 # define sRef_isInvalid(s) ((s) == NULL) 159 # define sRef_isValid(s) ((s) != NULL) 160 161 extern bool sRef_isRecursiveField (sRef p_s) /*@*/ ; 162 extern void sRef_copyRealDerivedComplete (sRef p_s1, sRef p_s2) /*@modifies p_s1@*/ ; 163 extern nstate sRef_getNullState (/*@sef@*/ sRef p_s) /*@*/ ; 164 extern bool sRef_isNotNull (sRef p_s) /*@*/ ; 165 166 extern bool sRef_isDefinitelyNull (sRef p_s) /*@*/ ; 167 168 extern /*@falsewhennull@*/ bool sRef_isLocalVar (sRef p_s) /*@*/ ; 169 extern /*@falsewhennull@*/ bool sRef_isNSLocalVar (sRef p_s) /*@*/ ; 170 extern /*@falsewhennull@*/ bool sRef_isRealLocalVar (sRef p_s) /*@*/ ; 171 extern /*@falsewhennull@*/ bool sRef_isLocalParamVar (sRef p_s) /*@*/ ; 172 extern /*@falsewhennull@*/ bool sRef_isKnown (/*@sef@*/ sRef p_s) /*@*/ ; 173 174 extern bool sRef_hasLastReference (sRef p_s) /*@*/ ; 175 # define sRef_hasLastReference(s) (sRef_hasAliasInfoRef (s)) 176 177 # define sRef_isKnown(s) (sRef_isValid(s) && (s)->kind != SK_UNKNOWN) 178 179 extern bool sRef_isMeaningful (/*@sef@*/ sRef p_s) /*@*/ ; 180 # define sRef_isMeaningful(s) (sRef_isValid(s) && sRef_isKnown(s) \ 181 && (s)->kind != SK_NEW && (s)->kind != SK_TYPE) 182 183 extern bool sRef_isSomewhatMeaningful (/*@sef@*/ sRef p_s) /*@*/ ; 184 # define sRef_isSomewhatMeaningful(s) (sRef_isValid(s) && sRef_isKnown(s) \ 185 && (s)->kind != SK_TYPE) 186 extern bool sRef_isNew (/*@sef@*/ sRef p_s) /*@*/ ; 187 # define sRef_isNew(s) (sRef_isValid(s) && (s)->kind == SK_NEW) 188 189 extern bool sRef_isType (/*@sef@*/ sRef p_s) /*@*/ ; 190 # define sRef_isType(s) (sRef_isValid(s) && (s)->kind == SK_TYPE) 191 192 extern bool sRef_isSafe (/*@sef@*/ sRef p_s) /*@*/ ; 193 # define sRef_isSafe(s) (sRef_isValid(s) && (s)->safe) 194 195 extern bool sRef_isUnsafe (/*@sef@*/ sRef p_s) /*@*/ ; 196 # define sRef_isUnsafe(s) (sRef_isValid(s) && !(s)->safe) 197 198 extern void sRef_clearAliasKind (/*@sef@*/ sRef p_s) /*@modifies p_s@*/ ; 199 # define sRef_clearAliasKind(s) (sRef_isValid(s) ? (s)->aliaskind = AK_UNKNOWN : AK_ERROR) 200 201 extern bool sRef_stateKnown (/*@sef@*/ sRef p_s) /*@*/ ; 202 # define sRef_stateKnown(s) (sRef_isValid(s) && (s)->defstate != SS_UNKNOWN) 203 204 extern alkind sRef_getAliasKind (/*@sef@*/ sRef p_s) /*@*/ ; 205 206 extern alkind sRef_getOrigAliasKind (/*@sef@*/ sRef p_s) /*@*/ ; 207 # define sRef_getOrigAliasKind(s) (sRef_isValid(s) ? (s)->oaliaskind : AK_ERROR) 208 209 extern /*@falsewhennull@*/ bool sRef_isConj (/*@sef@*/ sRef p_s) /*@*/ ; 210 # define sRef_isConj(s) (sRef_isValid(s) && (s)->kind == SK_CONJ) 211 212 extern /*@exposed@*/ sRef sRef_buildArrow (sRef p_s, /*@dependent@*/ cstring p_f); 213 extern /*@exposed@*/ sRef sRef_makeArrow (sRef p_s, /*@dependent@*/ cstring p_f); 214 215 extern bool sRef_isAllocIndexRef (sRef p_s) /*@*/ ; 216 extern void sRef_setAliasKind (sRef p_s, alkind p_kind, fileloc p_loc) /*@modifies p_s@*/ ; 217 extern void sRef_setPdefined (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ; 218 219 extern /*@unused@*/ bool sRef_hasDerived (sRef p_s) /*@*/ ; 220 extern void sRef_clearDerived (sRef p_s); 221 extern void sRef_clearDerivedComplete (sRef p_s); 222 extern /*@exposed@*/ sRef sRef_getBaseSafe (sRef p_s); 223 224 extern /*@observer@*/ sRefSet sRef_derivedFields (/*@temp@*/ sRef p_rec) /*@*/ ; 225 extern bool sRef_sameName (sRef p_s1, sRef p_s2) /*@*/ ; 226 extern bool sRef_isDirectParam (sRef p_s) /*@*/ ; 227 extern /*@exposed@*/ sRef sRef_makeAnyArrayFetch (/*@exposed@*/ sRef p_arr); 228 extern bool sRef_isUnknownArrayFetch (sRef p_s) /*@*/ ; 229 230 extern void sRef_setPartialDefinedComplete (sRef p_s, fileloc p_loc); 231 extern bool sRef_isMacroParamRef (sRef p_s) /*@*/ ; 232 233 extern void sRef_destroyMod (void) /*@modifies internalState@*/ ; 234 235 extern bool sRef_deepPred (bool (p_predf) (sRef), sRef p_s); 236 237 extern bool sRef_aliasCompleteSimplePred (bool (p_predf) (sRef), sRef p_s); 238 239 extern void sRef_clearExKindComplete (sRef p_s, fileloc p_loc); 240 241 extern /*@falsewhennull@*/ bool sRef_isKindSpecial (/*@sef@*/ sRef p_s) /*@*/ ; 242 # define sRef_isKindSpecial(s) (sRef_isValid (s) && (s)->kind == SK_SPECIAL) 243 244 extern /*@observer@*/ cstring sRef_nullMessage (sRef p_s) /*@*/ ; 245 246 extern bool sRef_isSystemState (sRef p_s) /*@*/ ; 247 extern bool sRef_isGlobalMarker (sRef p_s) /*@*/ ; 248 extern bool sRef_isInternalState (sRef p_s) /*@*/ ; 249 extern bool sRef_isResult (sRef p_s) /*@*/ ; 250 extern bool sRef_isSpecInternalState (sRef p_s) /*@*/ ; 251 extern bool sRef_isSpecState (sRef p_s) /*@*/ ; 252 extern bool sRef_isNothing (sRef p_s) /*@*/ ; 253 254 extern bool sRef_isFileOrGlobalScope (sRef p_s) /*@*/ ; 255 extern bool sRef_isReference (sRef p_s) /*@*/ ; 256 257 extern ctype sRef_deriveType (sRef p_s, uentryList p_cl) /*@*/ ; 258 extern ctype sRef_getType (sRef p_s) /*@*/ ; 259 260 extern void sRef_markImmutable (sRef p_s) /*@modifies p_s@*/ ; 261 262 extern /*@falsewhennull@*/ bool sRef_isAddress (sRef p_s) /*@*/ ; 263 extern /*@falsewhennull@*/ bool sRef_isArrayFetch (sRef p_s) /*@*/ ; 264 extern /*@falsewhennull@*/ bool sRef_isConst (sRef p_s) /*@*/ ; 265 extern /*@falsewhennull@*/ bool sRef_isCvar (sRef p_s) /*@*/ ; 266 extern /*@falsewhennull@*/ bool sRef_isField (sRef p_s) /*@*/ ; 267 extern /*@falsewhennull@*/ bool sRef_isParam (sRef p_s) /*@*/ ; 268 extern /*@falsewhennull@*/ bool sRef_isPointer (sRef p_s) /*@*/ ; 269 270 extern void sRef_setType (sRef p_s, ctype p_t); 271 extern void sRef_setTypeFull (sRef p_s, ctype p_t); 272 extern void sRef_mergeNullState (sRef p_s, nstate p_n); 273 extern void sRef_setLastReference (/*@temp@*/ sRef p_s, /*@exposed@*/ sRef p_ref, fileloc p_loc); 274 extern bool sRef_canModify (sRef p_s, sRefSet p_sl) /*@modifies p_s@*/ ; 275 extern bool sRef_canModifyVal (sRef p_s, sRefSet p_sl) /*@modifies p_s@*/ ; 276 extern bool sRef_isIReference (sRef p_s) /*@*/ ; 277 extern bool sRef_isIndexKnown (sRef p_arr) /*@*/ ; 278 extern bool sRef_isModified (sRef p_s) /*@*/ ; 279 280 extern bool sRef_isExternallyVisible (sRef p_s) /*@*/ ; 281 extern int sRef_compare (sRef p_s1, sRef p_s2) /*@*/ ; 282 extern bool sRef_realSame (sRef p_s1, sRef p_s2) /*@*/ ; 283 extern bool sRef_sameObject (sRef p_s1, sRef p_s2) /*@*/ ; 284 extern bool sRef_same (sRef p_s1, sRef p_s2) /*@*/ ; 285 extern bool sRef_similar (sRef p_s1, sRef p_s2) /*@*/ ; 286 extern /*@observer@*/ cstring sRef_getField (sRef p_s) /*@*/ ; 287 extern /*@only@*/ cstring sRef_unparse (sRef p_s) /*@*/ ; 288 extern /*@observer@*/ cstring sRef_stateVerb (sRef p_s) /*@*/ ; 289 extern /*@observer@*/ cstring sRef_stateAltVerb (sRef p_s) /*@*/ ; 290 extern /*@only@*/ cstring sRef_unparseOpt (sRef p_s) /*@*/ ; 291 extern /*@only@*/ cstring sRef_unparseDebug (sRef p_s) /*@*/ ; 292 extern void sRef_killComplete (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ; 293 extern int sRef_getIndex (sRef p_arr) /*@*/ ; 294 extern /*@dependent@*/ sRef sRef_fixOuterRef (/*@returned@*/ sRef p_s); 295 296 /* Use this one to clear after error */ 297 extern void sRef_setDefinedCompleteDirect (sRef p_s, fileloc p_loc) ; 298 299 extern void sRef_setDefinedComplete (sRef p_s, fileloc p_loc) ; 300 extern void sRef_setDefinedNCComplete (sRef p_s, fileloc p_loc) ; 301 extern int sRef_getParam (sRef p_s) /*@*/ ; 302 extern int sRef_lexLevel (sRef p_s) /*@*/ ; 303 extern void sRef_setOrigAliasKind (sRef p_s, alkind p_kind); 304 305 extern /*@exposed@*/ sRef 306 sRef_fixBase (/*@returned@*/ sRef p_s, /*@returned@*/ sRef p_base) 307 /*@modifies p_s, p_base@*/ ; 308 309 extern void sRef_showNotReallyDefined (sRef p_s) /*@modifies g_warningstream@*/ ; 310 311 extern void sRef_enterFunctionScope (void) /*@modifies internalState@*/ ; 312 extern void sRef_setGlobalScope (void) /*@modifies internalState@*/ ; 313 extern bool sRef_inGlobalScope (void) /*@*/ ; 314 extern void sRef_exitFunctionScope (void) /*@modifies internalState@*/ ; 315 extern void sRef_clearGlobalScopeSafe (void) /*@modifies internalState@*/ ; 316 extern void sRef_setGlobalScopeSafe (void) /*@modifies internalState@*/ ; 317 318 extern /*@notnull@*/ /*@exposed@*/ sRef 319 sRef_buildArrayFetch (/*@exposed@*/ sRef p_arr); 320 extern /*@notnull@*/ /*@exposed@*/ sRef sRef_buildArrayFetchKnown (/*@exposed@*/ sRef p_arr, int p_i); 321 extern /*@exposed@*/ sRef 322 sRef_buildField (/*@exposed@*/ sRef p_rec, /*@dependent@*/ cstring p_f) 323 /*@modifies p_rec@*/ ; 324 extern /*@exposed@*/ sRef sRef_buildPointer (/*@exposed@*/ sRef p_t) 325 /*@modifies p_t@*/ ; 326 327 extern /*@exposed@*/ sRef sRef_makeAddress (/*@exposed@*/ sRef p_t); 328 329 /* evans 2002-07-12: the parameter was exposed (but this led to invalid reads, reported by valgrind */ 330 extern /*@notnull@*/ /*@dependent@*/ sRef sRef_makeUnconstrained (/*@temp@*/ cstring) /*@*/ ; 331 332 extern /*@falsewhennull@*/ bool sRef_isUnconstrained (sRef p_s) /*@*/ ; 333 334 extern /*@observer@*/ cstring sRef_unconstrainedName (sRef p_s) /*@*/ ; 335 336 extern /*@notnull@*/ /*@exposed@*/ sRef sRef_makeArrayFetch (/*@exposed@*/ sRef p_arr) /*@*/ ; 337 extern /*@notnull@*/ /*@exposed@*/ sRef 338 sRef_makeArrayFetchKnown (/*@exposed@*/ sRef p_arr, int p_i); 339 extern /*@notnull@*/ /*@dependent@*/ sRef 340 sRef_makeConj (/*@exposed@*/ /*@returned@*/ sRef p_a, /*@exposed@*/ sRef p_b); 341 extern /*@notnull@*/ /*@dependent@*/ sRef 342 sRef_makeCvar (int p_level, usymId p_index, ctype p_ct, /*@only@*/ stateInfo p_stinfo); 343 extern /*@notnull@*/ /*@dependent@*/ sRef 344 sRef_makeConst (ctype p_ct); 345 extern /*@exposed@*/ sRef 346 sRef_makeField (sRef p_rec, /*@dependent@*/ cstring p_f); 347 extern /*@notnull@*/ /*@dependent@*/ sRef 348 sRef_makeGlobal (usymId p_l, ctype p_ct, /*@only@*/ stateInfo); 349 extern /*@exposed@*/ sRef 350 sRef_makeNCField (/*@exposed@*/ sRef p_rec, /*@dependent@*/ cstring p_f) /*@*/ ; 351 extern void sRef_maybeKill (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ; 352 extern /*@unused@*/ /*@notnull@*/ /*@dependent@*/ sRef 353 sRef_makeObject (ctype p_o) /*@*/ ; 354 extern /*@notnull@*/ /*@dependent@*/ sRef sRef_makeType (ctype p_ct) /*@*/ ; 355 extern /*@notnull@*/ /*@dependent@*/ sRef sRef_makeParam (int p_l, ctype p_ct, /*@only@*/ stateInfo p_stinfo) /*@*/ ; 356 extern /*@exposed@*/ sRef sRef_makePointer (/*@exposed@*/ sRef p_s) /*@modifies p_s@*/ ; 357 extern void sRef_makeSafe (sRef p_s) /*@modifies p_s@*/ ; 358 extern void sRef_makeUnsafe (sRef p_s) /*@modifies p_s@*/ ; 359 360 extern /*@dependent@*/ sRef sRef_makeUnknown (void) /*@*/ ; 361 extern /*@dependent@*/ sRef sRef_makeNothing (void) /*@*/ ; 362 extern /*@dependent@*/ sRef sRef_makeInternalState (void) /*@*/ ; 363 extern /*@dependent@*/ sRef sRef_makeSpecState (void) /*@*/ ; 364 extern /*@dependent@*/ sRef sRef_makeGlobalMarker (void) /*@*/ ; 365 extern /*@dependent@*/ sRef sRef_makeSystemState (void) /*@*/ ; 366 367 extern /*@dependent@*/ /*@notnull@*/ sRef sRef_makeResult (ctype) /*@*/ ; 368 extern /*@exposed@*/ sRef 369 sRef_fixResultType (/*@returned@*/ sRef p_s, ctype p_typ, uentry p_ue) 370 /*@modifies p_s@*/; 371 372 extern void sRef_setParamNo (sRef p_s, int p_l) /*@modifies p_s;@*/; 373 374 extern /*@notnull@*/ /*@dependent@*/ sRef 375 sRef_makeNew (ctype p_ct, sRef p_t, /*@exposed@*/ cstring p_name) ; 376 377 extern usymId sRef_getScopeIndex (sRef p_s) /*@*/ ; 378 extern /*@exposed@*/ uentry sRef_getBaseUentry (sRef p_s); 379 380 extern /*@exposed@*/ sRef 381 sRef_fixBaseParam (/*@returned@*/ sRef p_s, exprNodeList p_args) 382 /*@modifies p_s@*/ ; 383 384 /* 385 drl7x 386 added function 387 12/24/2000 388 */ 389 390 /*@only@*/ constraintExpr sRef_fixConstraintParam (/*@observer@*/ sRef p_s, /*@observer@*/ /*@temp@*/ exprNodeList p_args); 391 392 extern bool sRef_isUnionField (sRef p_s); 393 extern void sRef_setModified (sRef p_s); 394 395 extern void sRef_resetState (sRef p_s); 396 extern void sRef_resetStateComplete (sRef p_s); 397 398 extern void sRef_storeState (sRef p_s); 399 extern /*@exposed@*/ sRef sRef_getBase (sRef p_s) /*@*/ ; 400 extern /*@exposed@*/ sRef sRef_getRootBase (sRef p_s) /*@*/ ; 401 402 extern /*@observer@*/ uentry sRef_getUentry (sRef p_s); 403 404 extern cstring sRef_dump (sRef p_s) /*@*/ ; 405 extern cstring sRef_dumpGlobal (sRef p_s) /*@*/ ; 406 extern /*@exposed@*/ sRef sRef_undump (char **p_c) /*@modifies *p_c@*/ ; 407 extern /*@exposed@*/ sRef sRef_undumpGlobal (char **p_c) /*@modifies *p_c@*/ ; 408 409 extern /*@only@*/ sRef sRef_saveCopy (sRef p_s); 410 extern /*@dependent@*/ sRef sRef_copy (sRef p_s); 411 412 extern cstring sRef_unparseState (sRef p_s) /*@*/ ; 413 extern ynm sRef_isWriteable (sRef p_s) /*@*/ ; 414 extern ynm sRef_isValidLvalue (sRef p_s) /*@*/ ; 415 extern bool sRef_isStrictReadable (sRef p_s) /*@*/ ; 416 extern bool sRef_hasNoStorage (sRef p_s) /*@*/ ; 417 extern void sRef_showExpInfo (sRef p_s) /*@modifies g_warningstream*/ ; 418 extern void sRef_setDefined (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ; 419 extern void sRef_setUndefined (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ; 420 extern void sRef_setOnly (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ; 421 extern void sRef_setDependent (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ; 422 extern void sRef_setOwned (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ; 423 extern void sRef_setKept (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ; 424 extern void sRef_setKeptComplete (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ; 425 extern void sRef_setFresh (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ; 426 extern void sRef_setShared (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ; 427 extern void sRef_showAliasInfo (sRef p_s) /*@modifies g_warningstream@*/ ; 428 extern void sRef_showMetaStateInfo (sRef p_s, cstring p_key) /*@modifies g_warningstream@*/ ; 429 extern void sRef_showNullInfo (sRef p_s) /*@modifies g_warningstream@*/ ; 430 extern void sRef_showStateInfo (sRef p_s) /*@modifies g_warningstream@*/ ; 431 extern void sRef_setStateFromType (sRef p_s, ctype p_ct) /*@modifies p_s@*/ ; 432 extern void sRef_kill (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ; 433 extern void sRef_setAllocated (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ; 434 extern void sRef_setAllocatedShallowComplete (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ; 435 extern void sRef_setAllocatedComplete (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ; 436 extern /*@only@*/ cstring sRef_unparseKindNamePlain (sRef p_s) /*@*/ ; 437 extern /*@falsewhennull@*/ bool sRef_isRealGlobal(sRef p_s) /*@*/ ; 438 extern /*@falsewhennull@*/ bool sRef_isFileStatic (sRef p_s) /*@*/ ; 439 440 extern int sRef_getScope (sRef p_s) /*@*/ ; 441 extern /*@observer@*/ cstring sRef_getScopeName (sRef p_s) /*@*/ ; 442 443 /* must be real function (passed as function param) */ 444 extern /*@falsewhennull@*/ bool sRef_isDead (sRef p_s) /*@*/ ; 445 extern /*@falsewhennull@*/ bool sRef_isDeadStorage (sRef p_s) /*@*/ ; 446 extern bool sRef_isStateLive (sRef p_s) /*@*/ ; 447 extern /*@falsewhennull@*/ bool sRef_isPossiblyDead (sRef p_s) /*@*/ ; 448 extern /*@nullwhentrue@*/ bool sRef_isStateUndefined (sRef p_s) /*@*/ ; 449 extern bool sRef_isUnuseable (sRef p_s) /*@*/ ; 450 451 extern /*@exposed@*/ sRef sRef_constructDeref (sRef p_t) 452 /*@modifies p_t@*/ ; 453 454 extern /*@exposed@*/ sRef sRef_constructDeadDeref (sRef p_t) 455 /*@modifies p_t@*/ ; 456 457 extern bool sRef_isJustAllocated (sRef p_s) /*@*/ ; 458 459 extern /*@falsewhennull@*/ bool sRef_isAllocated (sRef p_s) /*@*/ ; 460 461 extern bool sRef_isUndefGlob (/*@sef@*/ sRef p_s) /*@*/ ; 462 # define sRef_isUndefGlob(s) \ 463 ((sRef_isValid(s)) \ 464 && ((s)->defstate == SS_UNDEFGLOB || (s)->defstate == SS_UNDEFKILLED)) 465 466 extern bool sRef_isKilledGlob (/*@sef@*/ sRef p_s) /*@*/ ; 467 # define sRef_isKilledGlob(s) \ 468 ((sRef_isValid(s)) \ 469 && ((s)->defstate == SS_KILLED || (s)->defstate == SS_UNDEFKILLED)) 470 471 extern bool sRef_isRelDef (/*@sef@*/ sRef p_s) /*@*/ ; 472 # define sRef_isRelDef(s) \ 473 ((sRef_isValid(s)) && ((s)->defstate == SS_RELDEF)) 474 475 extern bool sRef_isPartial (/*@sef@*/ sRef p_s) /*@*/ ; 476 # define sRef_isPartial(s) \ 477 ((sRef_isValid(s)) && ((s)->defstate == SS_PARTIAL)) 478 479 extern bool sRef_isStateSpecial (/*@sef@*/ sRef p_s) /*@*/ ; 480 # define sRef_isStateSpecial(s) \ 481 ((sRef_isValid(s)) && ((s)->defstate == SS_SPECIAL)) 482 483 extern bool sRef_makeStateSpecial (sRef p_s) 484 /*@modifies p_s@*/ 485 /* returns false is sRef already has an inconsistend defstate */ ; 486 487 extern bool sRef_isStateDefined (/*@sef@*/ sRef p_s) /*@*/ ; 488 # define sRef_isStateDefined(s) \ 489 ((sRef_isValid(s)) && (((s)->defstate == SS_DEFINED) \ 490 || (s)->defstate == SS_RELDEF)) 491 492 extern bool sRef_isAnyDefined (/*@sef@*/ sRef p_s) /*@*/ ; 493 # define sRef_isAnyDefined(s) ((sRef_isValid(s)) && \ 494 (((s)->defstate == SS_DEFINED) \ 495 || ((s)->defstate == SS_RELDEF) \ 496 || ((s)->defstate == SS_PARTIAL))) 497 498 extern /*@falsewhennull@*/ bool sRef_isPdefined (/*@sef@*/ sRef p_s) /*@*/ ; 499 # define sRef_isPdefined(s) \ 500 ((sRef_isValid(s)) && ((s)->defstate == SS_PDEFINED)) 501 502 extern bool sRef_isReallyDefined (sRef p_s) /*@*/ ; 503 504 extern bool sRef_isStateUnknown (/*@sef@*/ sRef p_s) /*@*/ ; 505 # define sRef_isStateUnknown(s) \ 506 ((sRef_isValid(s)) && ((s)->defstate == SS_UNKNOWN)) 507 508 extern /*@falsewhennull@*/ bool sRef_isRefCounted (/*@sef@*/ sRef p_s) /*@*/ ; 509 # define sRef_isRefCounted(s) \ 510 ((sRef_isValid(s)) && ((s)->aliaskind == AK_REFCOUNTED)) 511 512 extern /*@falsewhennull@*/ bool sRef_isNewRef (/*@sef@*/ sRef p_s) /*@*/ ; 513 # define sRef_isNewRef(s) \ 514 ((sRef_isValid(s)) && ((s)->aliaskind == AK_NEWREF)) 515 516 extern /*@falsewhennull@*/ bool sRef_isKillRef (/*@sef@*/ sRef p_s) /*@*/ ; 517 # define sRef_isKillRef(s) \ 518 ((sRef_isValid(s)) && ((s)->aliaskind == AK_KILLREF)) 519 520 extern bool sRef_isOnly (sRef p_s) /*@*/ ; 521 extern bool sRef_isDependent (sRef p_s) /*@*/ ; 522 extern bool sRef_isOwned (/*@sef@*/ sRef p_s) /*@*/ ; 523 extern bool sRef_isKeep (/*@sef@*/ sRef p_s) /*@*/ ; 524 525 extern bool sRef_isKept (/*@sef@*/ sRef p_s) /*@*/ ; 526 # define sRef_isKept(s) \ 527 ((sRef_isValid(s)) && ((s)->aliaskind == AK_KEPT)) 528 529 extern /*@unused@*/ bool sRef_isTemp (sRef p_s) /*@*/ ; 530 531 extern bool sRef_isStack (sRef p_s) /*@*/ ; 532 extern bool sRef_isLocalState (sRef p_s) /*@*/ ; 533 extern bool sRef_isUnique (sRef p_s) /*@*/ ; 534 extern bool sRef_isShared (sRef p_s) /*@*/ ; 535 extern bool sRef_isExposed (sRef p_s) /*@*/ ; 536 extern bool sRef_isObserver (sRef p_s) /*@*/ ; 537 extern bool sRef_isFresh (sRef p_s) /*@*/ ; 538 539 extern bool sRef_isRefsField (/*@sef@*/ sRef p_s) /*@*/ ; 540 # define sRef_isRefsField(s) \ 541 ((sRef_isValid(s)) && ((s)->aliaskind == AK_REFS)) 542 543 extern void sRef_protectDerivs (void) /*@modifies internalState@*/ ; 544 extern void sRef_clearProtectDerivs (void) /*@modifies internalState@*/ ; 545 546 extern exkind sRef_getExKind (sRef p_s) /*@*/ ; 547 extern exkind sRef_getOrigExKind (sRef p_s) /*@*/ ; 548 extern void sRef_setExKind (sRef p_s, exkind p_exp, fileloc p_loc) /*@modifies p_s@*/ ; 549 extern void sRef_setExposed (sRef p_s, fileloc p_loc) /*@modifies p_s@*/; 550 551 extern bool sRef_isAnyParam (sRef p_s) /*@*/ ; 552 extern /*@observer@*/ sRef sRef_getAliasInfoRef (/*@temp@*/ sRef p_s) /*@*/ ; 553 extern bool sRef_hasAliasInfoRef (sRef p_s) /*@*/ ; 554 555 extern /*@exposed@*/ sRef sRef_constructPointer (/*@exposed@*/ sRef p_t) /*@modifies p_t*/ ; 556 extern bool sRef_isAliasCheckedGlobal (sRef p_s) /*@*/ ; 557 extern bool sRef_includedBy (sRef p_small, sRef p_big) /*@*/ ; 558 extern /*@dependent@*/ /*@exposed@*/ sRef sRef_makeExternal (/*@exposed@*/ sRef p_t) /*@*/ ; 559 extern bool sRef_similarRelaxed (sRef p_s1, sRef p_s2) /*@*/ ; 560 extern /*@only@*/ cstring sRef_unparseKindName (sRef p_s) /*@*/ ; 561 extern void sRef_copyState (sRef p_s1, sRef p_s2) /*@modifies p_s1@*/ ; 562 extern /*@unused@*/ bool sRef_isObject (sRef p_s) /*@*/ ; 563 extern bool sRef_isNotUndefined (sRef p_s) /*@*/ ; 564 extern bool sRef_isExternal (sRef p_s) /*@*/ ; 565 extern cstring sRef_unparseDeep (sRef p_s) /*@*/ ; 566 extern cstring sRef_unparseFull (sRef p_s) /*@*/ ; 567 extern /*@observer@*/ cstring sRef_unparseScope (sRef p_s) /*@*/ ; 568 extern void sRef_mergeState (sRef p_res, sRef p_other, clause p_cl, fileloc p_loc) 569 /*@modifies p_res, p_other@*/ ; 570 extern void sRef_mergeOptState (sRef p_res, sRef p_other, clause p_cl, fileloc p_loc) 571 /*@modifies p_res, p_other@*/ ; 572 extern void sRef_mergeStateQuiet (sRef p_res, sRef p_other) 573 /*@modifies p_res@*/ ; 574 extern void sRef_mergeStateQuietReverse (/*@dependent@*/ sRef p_res, /*@dependent@*/ sRef p_other) 575 /*@modifies p_res@*/ ; 576 extern void sRef_setStateFromUentry (sRef p_s, uentry p_ue) 577 /*@modifies p_s@*/ ; 578 extern bool sRef_isStackAllocated (sRef p_s) /*@*/ ; 579 extern bool sRef_modInFunction (void) /*@*/ ; 580 extern void sRef_clearAliasState (sRef p_s, fileloc p_loc) 581 /*@modifies p_s@*/ ; 582 extern void sRef_setPartial (sRef p_s, fileloc p_loc) 583 /*@modifies p_s@*/ ; 584 extern void sRef_setDerivNullState (sRef p_set, sRef p_guide, nstate p_ns) 585 /*@modifies p_set@*/ ; 586 587 extern void sRef_clearGlobalScope (void) /*@modifies internalState@*/ ; 588 589 extern /*@dependent@*/ sRef sRef_makeDerived (/*@exposed@*/ sRef p_t); 590 591 extern sstate sRef_getDefState (sRef p_s) /*@*/ ; 592 extern void sRef_setDefState (sRef p_s, sstate p_defstate, fileloc p_loc); 593 extern void sRef_showRefLost (sRef p_s); 594 extern void sRef_showRefKilled (sRef p_s); 595 extern /*@exposed@*/ sRef sRef_updateSref (sRef p_s); 596 597 extern void sRef_reflectAnnotation (sRef p_s, annotationInfo p_a, fileloc p_loc); 598 extern /*@observer@*/ valueTable sRef_getValueTable (sRef p_s) /*@*/ ; 599 600 extern void sRef_aliasCheckPred (bool (p_predf) (sRef, exprNode, sRef, exprNode), 601 /*@null@*/ bool (p_checkAliases) (sRef), 602 sRef p_s, exprNode p_e, exprNode p_err); 603 extern bool sRef_aliasCheckSimplePred (sRefTest p_predf, sRef p_s); 604 605 extern void sRef_showStateInconsistent (sRef p_s); 606 607 extern void sRef_setDependentComplete (sRef p_s, fileloc p_loc); 608 609 extern void sRef_setAliasKindComplete (sRef p_s, alkind p_kind, fileloc p_loc); 610 611 extern bool sRef_isThroughArrayFetch (sRef p_s) /*@*/ ; 612 613 extern /*@exposed@*/ /*@notnull@*/ sRef sRef_getConjA (sRef p_s) /*@*/ ; 614 extern /*@exposed@*/ /*@notnull@*/ sRef sRef_getConjB (sRef p_s) /*@*/ ; 615 616 extern /*@only@*/ cstring sRef_unparsePreOpt (sRef p_s) /*@*/ ; 617 618 extern bool sRef_hasName (sRef p_s) /*@*/ ; 619 extern void sRef_free (/*@only@*/ sRef p_s); 620 extern void sRef_setObserver (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ; 621 622 /* start modifications */ 623 /* functions for making modification to null-term info */ 624 extern void sRef_setNullTerminatedStateInnerComplete(sRef p_s, struct s_bbufinfo p_b, fileloc p_loc); 625 extern struct s_bbufinfo sRef_getNullTerminatedState(sRef p_s); 626 extern void sRef_setNullTerminatedState (sRef p_s); 627 extern void sRef_setPossiblyNullTerminatedState (sRef p_s); 628 extern void sRef_setNotNullTerminatedState (sRef p_s); 629 extern void sRef_setSize(sRef p_s, int p_size); 630 extern void sRef_setLen(sRef p_s, int p_len); 631 632 extern int sRef_getSize(sRef p_s); 633 634 /*@-nullderef@*/ 635 636 #define sRef_getSize(p_s) \ 637 ((p_s)->bufinfo.size) 638 639 extern int sRef_getLen(sRef p_s); 640 #define sRef_getLen(p_s) \ 641 ((p_s)->bufinfo.len) 642 643 extern /*@falsewhennull@*/ bool sRef_hasExpInfoLoc (sRef) /*@*/ ; 644 extern /*@falsewhennull@*/ bool sRef_hasStateInfoLoc (sRef) /*@*/ ; 645 extern /*@falsewhennull@*/ bool sRef_hasAliasInfoLoc (sRef) /*@*/ ; 646 647 extern bool sRef_hasBufStateInfo(sRef p_s); 648 # define sRef_hasBufStateInfo(p_s) \ 649 (sRef_isValid(p_s)) 650 651 extern bool sRef_isNullTerminated(/*@sef@*/sRef p_s); 652 # define sRef_isNullTerminated(p_s) \ 653 ( sRef_hasBufStateInfo((p_s)) ? ((p_s)->bufinfo.bufstate \ 654 == BB_NULLTERMINATED) : FALSE) 655 656 extern bool sRef_isPossiblyNullTerminated(/*@sef@*/sRef p_s); 657 # define sRef_isPossiblyNullTerminated(p_s) \ 658 ( sRef_hasBufStateInfo((p_s)) ? ((p_s)->bufinfo.bufstate \ 659 == BB_POSSIBLYNULLTERMINATED) : FALSE) 660 661 extern bool sRef_isNotNullTerminated(/*@sef@*/sRef p_s); 662 # define sRef_isNotNullTerminated(p_s) \ 663 ( sRef_hasBufStateInfo((p_s)) ? ((p_s)->bufinfo.bufstate \ 664 == BB_NOTNULLTERMINATED) : FALSE) 665 666 /*@=nullderef@*/ 667 668 669 /*drl7x 11/28/00*/ 670 extern bool sRef_isFixedArray (sRef p_s) /*@*/; 671 extern size_t sRef_getArraySize (sRef p_s) /*@*/; 672 673 extern /*@observer@*/ cstring sRef_ntMessage (sRef p_s); 674 extern void sRef_resetLen (sRef p_s) /*@modifies p_s@*/ ; 675 676 /* end modifications */ 677 678 extern void sRef_setMetaStateValueComplete (sRef p_s, cstring p_key, int p_value, fileloc p_loc) 679 /*@modifies p_s@*/ ; 680 681 extern void sRef_setMetaStateValue (sRef p_s, cstring p_key, int p_value, fileloc p_loc) 682 /*@modifies p_s@*/ ; 683 684 extern /*@observer@*/ stateValue sRef_getMetaStateValue (sRef p_s, cstring p_key) /*@*/ ; 685 686 extern bool sRef_checkMetaStateValue (sRef p_s, cstring p_key, int p_value) 687 /*@modifies p_s@*/ ; 688 689 extern void sRef_setValue (sRef p_s, /*@only@*/ multiVal p_val) /*@modifies p_s@*/ ; 690 extern bool sRef_hasValue (sRef p_s) /*@*/ ; 691 extern /*@observer@*/ multiVal sRef_getValue (sRef p_s) /*@*/ ; 692 693 extern /*@maynotreturn@*/ void sRef_checkValid (/*@temp@*/ sRef p_s) /*@modifies stderr@*/ ; 694 695 extern void 696 sRef_aliasSetComplete (void (p_predf) (sRef, fileloc), sRef p_s, fileloc p_loc) 697 /*@modifies p_s@*/ ; 698 699 extern void 700 sRef_aliasSetCompleteParam (void (p_predf) (sRef, int, fileloc), sRef p_s, 701 int p_kind, fileloc p_loc) 702 /*@modifies p_s@*/ ; 703 704 extern void 705 sRef_aliasSetCompleteAlkParam (void (p_predf) (sRef, alkind, fileloc), sRef p_s, 706 alkind p_kind, fileloc p_loc) 707 /*@modifies p_s@*/ ; 708 709 # ifdef DEBUGSPLINT 710 extern void sRef_checkCompletelyReasonable (sRef p_s) /*@modifies g_errorstream@*/ ; 711 # endif 712 713 # else 714 # error "Multiple include" 715 # endif 716 717 718 719 720 721 722 723 724 725 726 727 728 729