src/Headers/sRef.h

   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