src/Headers/sRef.h

   1 /*
   2 ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2000.
   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 } speckind;
  27
  28 typedef enum {
  29   SK_PARAM,
  30   SK_ARRAYFETCH,
  31   SK_FIELD,
  32   SK_PTR,
  33   SK_ADR,
  34   SK_CONST,
  35   SK_CVAR,
  36   SK_UNCONSTRAINED,
  37   SK_OBJECT,
  38   SK_CONJ,
  39   SK_EXTERNAL,
  40   SK_DERIVED,
  41   SK_NEW,
  42   SK_TYPE,
  43   SK_RESULT,
  44   SK_SPECIAL,
  45   SK_UNKNOWN
  46 } skind;
  47
  48 typedef struct _cref
  49 {
  50   int    lexlevel;
  51   usymId index;
  52 } *cref;
  53
  54 typedef struct _ainfo
  55 {
  56   /*@exposed@*/ /*@notnull@*/ sRef arr;
  57   bool indknown;
  58   int  ind;
  59 } *ainfo;
  60
  61 typedef struct _fldinfo
  62 {
  63   /*@exposed@*/ /*@notnull@*/  sRef rec;
  64   /*@observer@*/ cstring field;
  65 } *fldinfo ;
  66
  67 typedef struct _cjinfo
  68 {
  69   /*@exposed@*/ /*@notnull@*/ sRef a;
  70   /*@exposed@*/ /*@notnull@*/ sRef b;
  71 } *cjinfo ;
  72
  73 typedef union _sinfo
  74 {
  75   /*@only@*/ cref     cvar;
  76              int      paramno;
  77   /*@only@*/ ainfo    arrayfetch;
  78   /*@only@*/ fldinfo    field;
  79              ctype    object;
  80   /*@observer@*/ cstring fname; /* unconstrained, new */
  81   /*@exposed@*/ /*@notnull@*/ sRef     ref;
  82   /*@only@*/ cjinfo   conj;
  83              speckind   spec;
  84 } *sinfo;
  85
  86 typedef /*@null@*/ struct _alinfo
  87 {
  88   /*@only@*/ fileloc  loc;
  89   /*@observer@*/ sRef ref;
  90   /*@observer@*/ uentry ue;
  91 } *alinfo;
  92
  93 struct _sRef
  94 {
  95   /* does it need to be inside parens (macros) */
  96   bool safe      BOOLBITS;
  97
  98   /* has it been modified */
  99   bool modified  BOOLBITS;
 100
 101   skind kind;
 102   ctype type;
 103
 104   sstate defstate;
 105   nstate nullstate;
 106
 107   alkind aliaskind;
 108   alkind oaliaskind;
 109
 110   exkind expkind;     /* exposed, observer, normal */
 111   exkind oexpkind;
 112
 113   /* where it becomes observer/exposed */
 114   /*@null@*/ /*@only@*/ alinfo expinfo;
 115
 116   /* where it changed alias kind */
 117   /*@null@*/ /*@only@*/ alinfo aliasinfo;
 118
 119   /* where it is defined/allocated */
 120   /*@null@*/ /*@only@*/ alinfo definfo;
 121
 122   /* where it changes null state */
 123   /*@null@*/ /*@only@*/ alinfo nullinfo;
 124
 125   /*@only@*/ /*@relnull@*/ sinfo info;
 126
 127   /* stores fields for structs, elements for arrays, derefs for pointers */
 128   /*@only@*/ sRefSet deriv;
 129 } ;
 130
 131 extern bool sRef_perhapsNull (sRef p_s);
 132 extern bool sRef_possiblyNull (sRef p_s);
 133 extern bool sRef_definitelyNull (sRef p_s);
 134
 135 extern void sRef_setNullError (sRef p_s);
 136 extern void sRef_setNullUnknown (sRef p_s, fileloc p_loc);
 137 extern void sRef_setNotNull (sRef p_s, fileloc p_loc);
 138 extern void sRef_setNullState (sRef p_s, nstate p_n, fileloc p_loc);
 139 extern void sRef_setNullStateInnerComplete (sRef p_s, nstate p_n, fileloc p_loc);
 140 extern void sRef_setPosNull (sRef p_s, fileloc p_loc);
 141 extern void sRef_setDefNull (sRef p_s, fileloc p_loc);
 142
 143 extern /*@truenull@*/ bool sRef_isInvalid (sRef p_s) /*@*/ ;
 144 extern /*@falsenull@*/ bool sRef_isValid (sRef p_s) /*@*/ ;
 145
 146 /*@constant null sRef sRef_undefined; @*/
 147 # define sRef_undefined    ((sRef) NULL)
 148 # define sRef_isInvalid(s) ((s) == NULL)
 149 # define sRef_isValid(s)   ((s) != NULL)
 150
 151 extern bool sRef_isRecursiveField (sRef p_s) /*@*/ ;
 152 extern void sRef_copyRealDerivedComplete (sRef p_s1, sRef p_s2) /*@modifies p_s1@*/ ;
 153 extern nstate sRef_getNullState (/*@sef@*/ sRef p_s) /*@*/ ;
 154 extern bool sRef_isNotNull (sRef p_s) /*@*/ ;
 155
 156 # define sRef_getNullState(s)    (sRef_isValid(s) ? (s)->nullstate : NS_UNKNOWN)
 157 extern bool sRef_isDefinitelyNull (sRef p_s) /*@*/ ;
 158
 159 extern /*@falsenull@*/ bool sRef_isLocalVar (sRef p_s) /*@*/ ;
 160 extern /*@falsenull@*/ bool sRef_isNSLocalVar (sRef p_s) /*@*/ ;
 161 extern /*@falsenull@*/ bool sRef_isRealLocalVar (sRef p_s) /*@*/ ;
 162 extern /*@falsenull@*/ bool sRef_isLocalParamVar (sRef p_s) /*@*/ ;
 163 extern /*@falsenull@*/ bool sRef_isKnown (/*@sef@*/ sRef p_s) /*@*/ ;
 164
 165 extern bool sRef_hasLastReference (sRef p_s) /*@*/ ;
 166 # define sRef_hasLastReference(s) (sRef_hasAliasInfoRef (s))
 167
 168 # define sRef_isKnown(s)          (sRef_isValid(s) && (s)->kind != SK_UNKNOWN)
 169
 170 extern bool sRef_isMeaningful (/*@sef@*/ sRef p_s) /*@*/ ;
 171 # define sRef_isMeaningful(s)     (sRef_isValid(s) && sRef_isKnown(s) \
 172                                    && (s)->kind != SK_NEW && (s)->kind != SK_TYPE)
 173 extern bool sRef_isNew (/*@sef@*/ sRef p_s) /*@*/ ;
 174 # define sRef_isNew(s)            (sRef_isValid(s) && (s)->kind == SK_NEW)
 175
 176 extern bool sRef_isType (/*@sef@*/ sRef p_s) /*@*/ ;
 177 # define sRef_isType(s)           (sRef_isValid(s) && (s)->kind == SK_TYPE)
 178
 179 extern bool sRef_isSafe (/*@sef@*/ sRef p_s) /*@*/ ;
 180 # define sRef_isSafe(s)           (sRef_isValid(s) && (s)->safe)
 181
 182 extern bool sRef_isUnsafe (/*@sef@*/ sRef p_s) /*@*/ ;
 183 # define sRef_isUnsafe(s)         (sRef_isValid(s) && !(s)->safe)
 184
 185 extern void sRef_clearAliasKind (/*@sef@*/ sRef p_s) /*@modifies p_s@*/ ;
 186 # define sRef_clearAliasKind(s)   (sRef_isValid(s) ? (s)->aliaskind = AK_UNKNOWN : AK_ERROR)
 187
 188 extern bool sRef_stateKnown (/*@sef@*/ sRef p_s) /*@*/ ;
 189 # define sRef_stateKnown(s)       (sRef_isValid(s) && (s)->defstate != SS_UNKNOWN)
 190
 191 extern alkind sRef_getAliasKind (/*@sef@*/ sRef p_s) /*@*/ ;
 192 # define sRef_getAliasKind(s)     (sRef_isValid(s) ? (s)->aliaskind : AK_ERROR)
 193
 194 extern alkind sRef_getOrigAliasKind (/*@sef@*/ sRef p_s) /*@*/ ;
 195 # define sRef_getOrigAliasKind(s) (sRef_isValid(s) ? (s)->oaliaskind : AK_ERROR)
 196
 197 extern /*@falsenull@*/ bool sRef_isConj (/*@sef@*/ sRef p_s) /*@*/ ;
 198 # define sRef_isConj(s)           (sRef_isValid(s) && (s)->kind == SK_CONJ)
 199
 200 extern /*@exposed@*/ sRef sRef_buildArrow (sRef p_s, /*@dependent@*/ cstring p_f);
 201 extern /*@exposed@*/ sRef sRef_makeArrow (sRef p_s, /*@dependent@*/ cstring p_f);
 202
 203 extern bool sRef_isAllocIndexRef (sRef p_s) /*@*/ ;
 204 extern void sRef_setAliasKind (sRef p_s, alkind p_kind, fileloc p_loc) /*@modifies p_s@*/ ;
 205 extern void sRef_setPdefined (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
 206
 207 extern /*@unused@*/ bool sRef_hasDerived (sRef p_s) /*@*/ ;
 208 extern void sRef_clearDerived (sRef p_s);
 209 extern void sRef_clearDerivedComplete (sRef p_s);
 210 extern /*@exposed@*/ sRef sRef_getBaseSafe (sRef p_s);
 211
 212 extern /*@observer@*/ sRefSet sRef_derivedFields (/*@dependent@*/ sRef p_rec) /*@*/ ;
 213 extern bool sRef_sameName (sRef p_s1, sRef p_s2) /*@*/ ;
 214 extern bool sRef_isDirectParam (sRef p_s) /*@*/ ;
 215 extern /*@exposed@*/ sRef sRef_makeAnyArrayFetch (/*@exposed@*/ sRef p_arr);
 216 extern bool sRef_isUnknownArrayFetch (sRef p_s) /*@*/ ;
 217
 218 extern void sRef_setPartialDefinedComplete (sRef p_s, fileloc p_loc);
 219 extern bool sRef_isMacroParamRef (sRef p_s) /*@*/ ;
 220
 221 extern void sRef_destroyMod (void) /*@modifies internalState@*/ ;
 222
 223 extern bool sRef_deepPred (bool (p_predf) (sRef), sRef p_s);
 224
 225 extern bool sRef_aliasCompleteSimplePred (bool (p_predf) (sRef), sRef p_s);
 226
 227 extern void sRef_clearExKindComplete (sRef p_s, fileloc p_loc);
 228
 229 extern /*@falsenull@*/ bool sRef_isKindSpecial (/*@sef@*/ sRef p_s) /*@*/ ;
 230 # define sRef_isKindSpecial(s) (sRef_isValid (s) && (s)->kind == SK_SPECIAL)
 231
 232 extern /*@observer@*/ cstring sRef_nullMessage (sRef p_s) /*@*/ ;
 233
 234 extern bool sRef_isSystemState (sRef p_s) /*@*/ ;
 235 extern bool sRef_isInternalState (sRef p_s) /*@*/ ;
 236 extern bool sRef_isResult (sRef p_s) /*@*/ ;
 237 extern bool sRef_isSpecInternalState (sRef p_s) /*@*/ ;
 238 extern bool sRef_isSpecState (sRef p_s) /*@*/ ;
 239 extern bool sRef_isNothing (sRef p_s) /*@*/ ;
 240
 241 extern bool sRef_isGlobal (sRef p_s) /*@*/ ;
 242 extern bool sRef_isReference (sRef p_s) /*@*/ ;
 243
 244 extern ctype sRef_deriveType (sRef p_s, uentryList p_cl) /*@*/ ;
 245 extern ctype sRef_getType (sRef p_s) /*@*/ ;
 246
 247 extern /*@falsenull@*/ bool sRef_isAddress (sRef p_s) /*@*/ ;
 248 extern /*@falsenull@*/ bool sRef_isArrayFetch (sRef p_s) /*@*/ ;
 249 extern /*@falsenull@*/ bool sRef_isConst (sRef p_s) /*@*/ ;
 250 extern /*@falsenull@*/ bool sRef_isCvar (sRef p_s) /*@*/ ;
 251 extern /*@falsenull@*/ bool sRef_isField (sRef p_s) /*@*/ ;
 252 extern /*@falsenull@*/ bool sRef_isParam (sRef p_s) /*@*/ ;
 253 extern /*@falsenull@*/ bool sRef_isPointer (sRef p_s) /*@*/ ;
 254
 255 extern void sRef_setType (sRef p_s, ctype p_t);
 256 extern void sRef_setTypeFull (sRef p_s, ctype p_t);
 257 extern void sRef_mergeNullState (sRef p_s, nstate p_n);
 258 extern void sRef_setLastReference (sRef p_s, sRef p_ref, fileloc p_loc);
 259 extern bool sRef_canModify (sRef p_s, sRefSet p_sl) /*@modifies p_s@*/ ;
 260 extern bool sRef_canModifyVal (sRef p_s, sRefSet p_sl) /*@modifies p_s@*/ ;
 261 extern bool sRef_isIReference (sRef p_s) /*@*/ ;
 262 extern bool sRef_isIndexKnown (sRef p_arr) /*@*/ ;
 263 extern bool sRef_isModified (sRef p_s) /*@*/ ;
 264
 265 extern bool sRef_isExternallyVisible (sRef p_s) /*@*/ ;
 266 extern int sRef_compare (sRef p_s1, sRef p_s2) /*@*/ ;
 267 extern bool sRef_realSame (sRef p_s1, sRef p_s2) /*@*/ ;
 268 extern bool sRef_same (sRef p_s1, sRef p_s2) /*@*/ ;
 269 extern bool sRef_similar (sRef p_s1, sRef p_s2) /*@*/ ;
 270 extern /*@observer@*/ cstring sRef_getField (sRef p_s) /*@*/ ;
 271 extern /*@only@*/ cstring sRef_unparse (sRef p_s) /*@*/ ;
 272 extern /*@observer@*/ cstring sRef_stateVerb (sRef p_s) /*@*/ ;
 273 extern /*@observer@*/ cstring sRef_stateAltVerb (sRef p_s) /*@*/ ;
 274 extern /*@only@*/ cstring sRef_unparseOpt (sRef p_s) /*@*/ ;
 275 extern /*@only@*/ cstring sRef_unparseDebug (sRef p_s) /*@*/ ;
 276 extern void sRef_killComplete (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
 277 extern int sRef_getIndex (sRef p_arr) /*@*/ ;
 278 extern /*@dependent@*/ sRef sRef_fixOuterRef (/*@returned@*/ sRef p_s);
 279 extern void sRef_setDefinedComplete (sRef p_s, fileloc p_loc);
 280 extern void sRef_setDefinedNCComplete (sRef p_s, fileloc p_loc);
 281 extern int sRef_getParam (sRef p_s) /*@*/ ;
 282 extern int sRef_lexLevel (sRef p_s) /*@*/ ;
 283 extern void sRef_setOrigAliasKind (sRef p_s, alkind p_kind);
 284 extern /*@exposed@*/ sRef
 285   sRef_fixBase (/*@returned@*/ sRef p_s, /*@returned@*/ sRef p_base)
 286   /*@modifies p_s, p_base@*/ ;
 287
 288 extern void sRef_showNotReallyDefined (sRef p_s) /*@modifies g_msgstream@*/ ;
 289
 290 extern void sRef_enterFunctionScope (void);
 291 extern void sRef_setGlobalScope (void);
 292 extern void sRef_exitFunctionScope (void);
 293 extern void sRef_clearGlobalScopeSafe (void);
 294 extern void sRef_setGlobalScopeSafe (void);
 295
 296 extern /*@notnull@*/ /*@exposed@*/ sRef
 297   sRef_buildArrayFetch (/*@exposed@*/ sRef p_arr);
 298 extern /*@notnull@*/ /*@exposed@*/ sRef sRef_buildArrayFetchKnown (/*@exposed@*/ sRef p_arr, int p_i);
 299 extern /*@exposed@*/ sRef
 300   sRef_buildField (sRef p_rec, /*@dependent@*/ cstring p_f)
 301   /*@modifies p_rec@*/ ;
 302 extern /*@exposed@*/ sRef sRef_buildPointer (/*@exposed@*/ sRef p_t)
 303   /*@modifies p_t@*/ ;
 304
 305 extern /*@exposed@*/ sRef sRef_makeAddress (/*@exposed@*/ sRef p_t);
 306 extern /*@notnull@*/ /*@dependent@*/ sRef sRef_makeUnconstrained (/*@exposed@*/ cstring) /*@*/ ;
 307
 308 extern /*@falsenull@*/ bool sRef_isUnconstrained (sRef p_s) /*@*/ ;
 309
 310 extern /*@observer@*/ cstring sRef_unconstrainedName (sRef p_s) /*@*/ ;
 311
 312 extern /*@notnull@*/ /*@exposed@*/ sRef sRef_makeArrayFetch (sRef p_arr) /*@*/ ;
 313 extern /*@notnull@*/ /*@exposed@*/ sRef
 314   sRef_makeArrayFetchKnown (sRef p_arr, int p_i);
 315 extern /*@notnull@*/ /*@dependent@*/ sRef
 316   sRef_makeConj (/*@exposed@*/ /*@returned@*/ sRef p_a, /*@exposed@*/ sRef p_b);
 317 extern /*@notnull@*/ /*@dependent@*/ sRef
 318   sRef_makeCvar (int p_level, usymId p_index, ctype p_ct);
 319 extern /*@notnull@*/ /*@dependent@*/ sRef
 320   sRef_makeConst (ctype p_ct);
 321 extern /*@exposed@*/ sRef
 322   sRef_makeField (sRef p_rec, /*@dependent@*/ cstring p_f);
 323 extern /*@notnull@*/ /*@dependent@*/ sRef
 324   sRef_makeGlobal (usymId p_l, ctype p_ct);
 325 extern /*@exposed@*/ sRef
 326   sRef_makeNCField (sRef p_rec, /*@dependent@*/ cstring p_f) /*@*/ ;
 327 extern void sRef_maybeKill (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
 328 extern /*@unused@*/ /*@notnull@*/ /*@dependent@*/ sRef
 329   sRef_makeObject (ctype p_o) /*@*/ ;
 330 extern /*@notnull@*/ /*@dependent@*/ sRef sRef_makeType (ctype p_ct) /*@*/ ;
 331 extern /*@notnull@*/ /*@dependent@*/ sRef sRef_makeParam (int p_l, ctype p_ct) /*@*/ ;
 332 extern /*@exposed@*/ sRef sRef_makePointer (sRef p_s) /*@modifies p_s@*/ ;
 333 extern void sRef_makeSafe (sRef p_s) /*@modifies p_s@*/ ;
 334 extern void sRef_makeUnsafe (sRef p_s) /*@modifies p_s@*/ ;
 335 extern sRef sRef_makeUnknown (void) /*@*/ ;
 336
 337 extern sRef sRef_makeNothing (void) /*@*/ ;
 338 extern sRef sRef_makeInternalState (void) /*@*/ ;
 339 extern sRef sRef_makeSpecState (void) /*@*/ ;
 340 extern sRef sRef_makeSystemState (void) /*@*/ ;
 341
 342 extern /*@notnull@*/ sRef sRef_makeResult (void) /*@*/ ;
 343 extern /*@exposed@*/ sRef
 344   sRef_fixResultType (/*@returned@*/ sRef p_s, ctype p_typ, uentry p_ue)
 345   /*@modifies p_s@*/;
 346
 347 extern void sRef_setParamNo (sRef p_s, int p_l) /*@modifies p_s;@*/;
 348
 349 extern /*@notnull@*/ sRef
 350   sRef_makeNew (ctype p_ct, sRef p_t, /*@exposed@*/ cstring p_name);
 351
 352 extern usymId sRef_getScopeIndex (sRef p_s) /*@*/ ;
 353 extern /*@exposed@*/ uentry sRef_getBaseUentry (sRef p_s);
 354
 355 extern /*@exposed@*/ sRef
 356   sRef_fixBaseParam (/*@returned@*/ sRef p_s, exprNodeList p_args)
 357   /*@modifies p_s@*/ ;
 358
 359 extern bool sRef_isUnionField (sRef p_s);
 360 extern void sRef_setModified (sRef p_s);
 361
 362 extern void sRef_resetState (sRef p_s);
 363 extern void sRef_resetStateComplete (sRef p_s);
 364
 365 extern void sRef_storeState (sRef p_s);
 366 extern /*@exposed@*/ sRef sRef_getBase (sRef p_s) /*@*/ ;
 367 extern /*@exposed@*/ sRef sRef_getRootBase (sRef p_s) /*@*/ ;
 368
 369 extern /*@observer@*/ uentry sRef_getUentry (sRef p_s);
 370
 371 extern cstring sRef_dump (sRef p_s) /*@*/ ;
 372 extern cstring sRef_dumpGlobal (sRef p_s) /*@*/ ;
 373 extern /*@exposed@*/ sRef sRef_undump (char **p_c) /*@modifies *p_c@*/ ;
 374 extern /*@exposed@*/ sRef sRef_undumpGlobal (char **p_c) /*@modifies *p_c@*/ ;
 375
 376 extern /*@only@*/ sRef sRef_saveCopy (sRef p_s);
 377 extern /*@dependent@*/ sRef sRef_copy (sRef p_s);
 378
 379 extern cstring sRef_unparseState (sRef p_s) /*@*/ ;
 380 extern ynm sRef_isWriteable (sRef p_s) /*@*/ ;
 381 extern ynm sRef_isReadable (sRef p_s) /*@*/ ;
 382 extern bool sRef_isStrictReadable (sRef p_s) /*@*/ ;
 383 extern bool sRef_hasNoStorage (sRef p_s) /*@*/ ;
 384 extern void sRef_showExpInfo (sRef p_s) /*@modifies g_msgstream*/ ;
 385 extern void sRef_setDefined (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
 386 extern void sRef_setUndefined (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
 387 extern void sRef_setOnly (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
 388 extern void sRef_setDependent (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
 389 extern void sRef_setOwned (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
 390 extern void sRef_setKept (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
 391 extern void sRef_setKeptComplete (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
 392 extern void sRef_setFresh (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
 393 extern void sRef_setShared (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
 394 extern void sRef_showAliasInfo (sRef p_s) /*@modifies g_msgstream@*/ ;
 395 extern void sRef_showNullInfo (sRef p_s) /*@modifies g_msgstream@*/ ;
 396 extern void sRef_showStateInfo (sRef p_s) /*@modifies g_msgstream@*/ ;
 397 extern void sRef_setStateFromType (sRef p_s, ctype p_ct) /*@modifies p_s@*/ ;
 398 extern void sRef_kill (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
 399 extern void sRef_setAllocated (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
 400 extern void sRef_setAllocatedShallowComplete (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
 401 extern void sRef_setAllocatedComplete (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
 402 extern /*@only@*/ cstring sRef_unparseKindNamePlain (sRef p_s) /*@*/ ;
 403 extern /*@falsenull@*/ bool sRef_isRealGlobal(sRef p_s) /*@*/ ;
 404 extern /*@falsenull@*/ bool sRef_isFileStatic (sRef p_s) /*@*/ ;
 405
 406 extern int sRef_getScope (sRef p_s) /*@*/ ;
 407 extern /*@observer@*/ cstring sRef_getScopeName (sRef p_s) /*@*/ ;
 408
 409 /* must be real function (passed as function param) */
 410 extern /*@falsenull@*/ bool sRef_isDead (sRef p_s) /*@*/ ;
 411 extern /*@falsenull@*/ bool sRef_isDeadStorage (sRef p_s) /*@*/ ;
 412 extern bool sRef_isStateLive (sRef p_s) /*@*/ ;
 413 extern /*@falsenull@*/ bool sRef_isPossiblyDead (sRef p_s) /*@*/ ;
 414 extern /*@truenull@*/ bool sRef_isStateUndefined (sRef p_s) /*@*/ ;
 415 extern bool sRef_isUnuseable (sRef p_s) /*@*/ ;
 416
 417 extern /*@exposed@*/ sRef sRef_constructDeref (sRef p_t)
 418    /*@modifies p_t@*/ ;
 419
 420 extern /*@exposed@*/ sRef sRef_constructDeadDeref (sRef p_t)
 421    /*@modifies p_t@*/ ;
 422
 423 extern bool sRef_isJustAllocated (sRef p_s) /*@*/ ;
 424
 425 extern /*@falsenull@*/ bool sRef_isAllocated (sRef p_s) /*@*/ ;
 426
 427 extern bool sRef_isUndefGlob (/*@sef@*/ sRef p_s) /*@*/ ;
 428 # define sRef_isUndefGlob(s) \
 429     ((sRef_isValid(s)) \
 430      && ((s)->defstate == SS_UNDEFGLOB || (s)->defstate == SS_UNDEFKILLED))
 431
 432 extern bool sRef_isKilledGlob (/*@sef@*/ sRef p_s) /*@*/ ;
 433 # define sRef_isKilledGlob(s) \
 434     ((sRef_isValid(s)) \
 435      && ((s)->defstate == SS_KILLED || (s)->defstate == SS_UNDEFKILLED))
 436
 437 extern bool sRef_isRelDef (/*@sef@*/ sRef p_s) /*@*/ ;
 438 # define sRef_isRelDef(s) \
 439   ((sRef_isValid(s)) && ((s)->defstate == SS_RELDEF))
 440
 441 extern bool sRef_isPartial (/*@sef@*/ sRef p_s) /*@*/ ;
 442 # define sRef_isPartial(s) \
 443   ((sRef_isValid(s)) && ((s)->defstate == SS_PARTIAL))
 444
 445 extern bool sRef_isStateSpecial (/*@sef@*/ sRef p_s) /*@*/ ;
 446 # define sRef_isStateSpecial(s) \
 447   ((sRef_isValid(s)) && ((s)->defstate == SS_SPECIAL))
 448
 449 extern bool sRef_isStateDefined (/*@sef@*/ sRef p_s) /*@*/ ;
 450 # define sRef_isStateDefined(s) \
 451   ((sRef_isValid(s)) && (((s)->defstate == SS_DEFINED) \
 452                          || (s)->defstate == SS_RELDEF))
 453
 454 extern bool sRef_isAnyDefined (/*@sef@*/ sRef p_s) /*@*/ ;
 455 # define sRef_isAnyDefined(s)   ((sRef_isValid(s)) && \
 456                                  (((s)->defstate == SS_DEFINED) \
 457                                   || ((s)->defstate == SS_RELDEF) \
 458                                   || ((s)->defstate == SS_PARTIAL)))
 459
 460 extern /*@falsenull@*/ bool sRef_isPdefined (/*@sef@*/ sRef p_s) /*@*/ ;
 461 # define sRef_isPdefined(s) \
 462   ((sRef_isValid(s)) && ((s)->defstate == SS_PDEFINED))
 463
 464 extern bool sRef_isReallyDefined (sRef p_s) /*@*/ ;
 465
 466 extern bool sRef_isStateUnknown (/*@sef@*/ sRef p_s) /*@*/ ;
 467 # define sRef_isStateUnknown(s) \
 468   ((sRef_isValid(s)) && ((s)->defstate == SS_UNKNOWN))
 469
 470 extern /*@falsenull@*/ bool sRef_isRefCounted (/*@sef@*/ sRef p_s) /*@*/ ;
 471 # define sRef_isRefCounted(s) \
 472   ((sRef_isValid(s)) && ((s)->aliaskind == AK_REFCOUNTED))
 473
 474 extern /*@falsenull@*/ bool sRef_isNewRef (/*@sef@*/ sRef p_s) /*@*/ ;
 475 # define sRef_isNewRef(s) \
 476   ((sRef_isValid(s)) && ((s)->aliaskind == AK_NEWREF))
 477
 478 extern /*@falsenull@*/ bool sRef_isKillRef (/*@sef@*/ sRef p_s) /*@*/ ;
 479 # define sRef_isKillRef(s) \
 480   ((sRef_isValid(s)) && ((s)->aliaskind == AK_KILLREF))
 481
 482 extern bool sRef_isOnly (sRef p_s) /*@*/ ;
 483 extern bool sRef_isDependent (sRef p_s) /*@*/ ;
 484 extern bool sRef_isOwned (/*@sef@*/ sRef p_s) /*@*/ ;
 485 extern bool sRef_isKeep (/*@sef@*/ sRef p_s) /*@*/ ;
 486
 487 extern bool sRef_isKept (/*@sef@*/ sRef p_s) /*@*/ ;
 488 # define sRef_isKept(s) \
 489   ((sRef_isValid(s)) && ((s)->aliaskind == AK_KEPT))
 490
 491 extern /*@unused@*/ bool sRef_isTemp (sRef p_s) /*@*/ ;
 492
 493 extern bool sRef_isStack (sRef p_s) /*@*/ ;
 494 extern bool sRef_isLocalState (sRef p_s) /*@*/ ;
 495 extern bool sRef_isUnique (sRef p_s) /*@*/ ;
 496 extern bool sRef_isShared (sRef p_s) /*@*/ ;
 497 extern bool sRef_isExposed (sRef p_s) /*@*/ ;
 498 extern bool sRef_isObserver (sRef p_s) /*@*/ ;
 499 extern bool sRef_isFresh (sRef p_s) /*@*/ ;
 500
 501 extern bool sRef_isRefsField (/*@sef@*/ sRef p_s) /*@*/ ;
 502 # define sRef_isRefsField(s) \
 503   ((sRef_isValid(s)) && ((s)->aliaskind == AK_REFS))
 504
 505 extern void sRef_protectDerivs (void) /*@modifies internalState@*/ ;
 506 extern void sRef_clearProtectDerivs (void) /*@modifies internalState@*/ ;
 507
 508 extern exkind sRef_getExKind (sRef p_s) /*@*/ ;
 509 extern exkind sRef_getOrigExKind (sRef p_s) /*@*/ ;
 510 extern void sRef_setExKind (sRef p_s, exkind p_exp, fileloc p_loc) /*@modifies p_s@*/ ;
 511 extern void sRef_setExposed (sRef p_s, fileloc p_loc) /*@modifies p_s@*/;
 512
 513 extern bool sRef_isAnyParam (sRef p_s) /*@*/ ;
 514 extern /*@observer@*/ sRef sRef_getAliasInfoRef (/*@exposed@*/ sRef p_s) /*@*/ ;
 515 extern bool sRef_hasAliasInfoRef (sRef p_s) /*@*/ ;
 516
 517 extern /*@exposed@*/ sRef sRef_constructPointer (sRef p_t) /*@modifies p_t*/ ;
 518 extern bool sRef_isAliasCheckedGlobal (sRef p_s) /*@*/ ;
 519 extern bool sRef_includedBy (sRef p_small, sRef p_big) /*@*/ ;
 520 extern /*@dependent@*/ /*@exposed@*/ sRef sRef_makeExternal (/*@exposed@*/ sRef p_t) /*@*/ ;
 521 extern bool sRef_similarRelaxed (sRef p_s1, sRef p_s2) /*@*/ ;
 522 extern /*@only@*/ cstring sRef_unparseKindName (sRef p_s) /*@*/ ;
 523 extern void sRef_copyState (sRef p_s1, sRef p_s2) /*@modifies p_s1@*/ ;
 524 extern /*@unused@*/ bool sRef_isObject (sRef p_s) /*@*/ ;
 525 extern bool sRef_isNotUndefined (sRef p_s) /*@*/ ;
 526 extern bool sRef_isExternal (sRef p_s) /*@*/ ;
 527 extern cstring sRef_unparseDeep (sRef p_s) /*@*/ ;
 528 extern cstring sRef_unparseFull (sRef p_s) /*@*/ ;
 529 extern /*@observer@*/ cstring sRef_unparseScope (sRef p_s) /*@*/ ;
 530 extern void sRef_mergeState (sRef p_res, sRef p_other, clause p_cl, fileloc p_loc)
 531    /*@modifies p_res, p_other@*/ ;
 532 extern void sRef_mergeOptState (sRef p_res, sRef p_other, clause p_cl, fileloc p_loc)
 533    /*@modifies p_res, p_other@*/ ;
 534 extern void sRef_mergeStateQuiet (sRef p_res, sRef p_other)
 535    /*@modifies p_res@*/ ;
 536 extern void sRef_mergeStateQuietReverse (sRef p_res, sRef p_other)
 537    /*@modifies p_res@*/ ;
 538 extern void sRef_setStateFromUentry (sRef p_s, uentry p_ue)
 539    /*@modifies p_s@*/ ;
 540 extern bool sRef_isStackAllocated (sRef p_s) /*@*/ ;
 541 extern bool sRef_modInFunction (void) /*@*/ ;
 542 extern void sRef_clearAliasState (sRef p_s, fileloc p_loc)
 543    /*@modifies p_s@*/ ;
 544 extern void sRef_setPartial (sRef p_s, fileloc p_loc)
 545    /*@modifies p_s@*/ ;
 546 extern void sRef_setDerivNullState (sRef p_set, sRef p_guide, nstate p_ns)
 547    /*@modifies p_set@*/ ;
 548
 549 extern void sRef_clearGlobalScope (void) /*@modifies internalState@*/ ;
 550
 551 extern sRef sRef_makeDerived (/*@exposed@*/ sRef p_t);
 552
 553 extern sstate sRef_getDefState (sRef p_s) /*@*/ ;
 554 extern void sRef_setDefState (sRef p_s, sstate p_defstate, fileloc p_loc);
 555 extern void sRef_showRefLost (sRef p_s);
 556 extern void sRef_showRefKilled (sRef p_s);
 557 extern /*@exposed@*/ sRef sRef_updateSref (sRef p_s);
 558
 559 extern void sRef_aliasCheckPred (bool (p_predf) (sRef, exprNode, sRef, exprNode),
 560                                  /*@null@*/ bool (p_checkAliases) (sRef),
 561                                  sRef p_s, exprNode p_e, exprNode p_err);
 562 extern bool sRef_aliasCheckSimplePred (sRefTest p_predf, sRef p_s);
 563
 564 extern void sRef_showStateInconsistent (sRef p_s);
 565
 566 extern void sRef_setDependentComplete (sRef p_s, fileloc p_loc);
 567
 568 extern void sRef_setAliasKindComplete (sRef p_s, alkind p_kind, fileloc p_loc);
 569
 570 extern bool sRef_isThroughArrayFetch (sRef p_s) /*@*/ ;
 571
 572 extern /*@exposed@*/ /*@notnull@*/ sRef sRef_getConjA (sRef p_s) /*@*/ ;
 573 extern /*@exposed@*/ /*@notnull@*/ sRef sRef_getConjB (sRef p_s) /*@*/ ;
 574
 575 extern /*@only@*/ cstring sRef_unparsePreOpt (sRef p_s) /*@*/ ;
 576
 577 extern bool sRef_hasName (sRef p_s) /*@*/ ;
 578
 579 extern void sRef_free (/*@only@*/ sRef p_s);
 580
 581 extern void sRef_setObserver (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
 582
 583 # else
 584 # error "Multiple include"
 585 # endif
 586
 587
 588
 589
 590
 591
 592
 593
 594
 595
 596
 597
 598