src/Headers/varKinds.h

   1 /*
   2 ** varKinds.h
   3 */
   4
   5 # ifndef VARKINDSH
   6 # define VARKINDSH
   7
   8 /*
   9 ** states of storage
  10 */
  11
  12 typedef enum {
  13   SS_UNKNOWN,
  14   SS_UNUSEABLE, /* cannot use (unallocated pointer reference) */
  15   SS_UNDEFINED, /* cannot use value (e.g., unbound variable) */
  16   SS_MUNDEFINED,/* maybe undefined */
  17   SS_ALLOCATED, /* allocated pointer */
  18   SS_PDEFINED,  /* partially defined: must check reachable values */
  19   SS_DEFINED,   /* completely defined: can use value and all reachable values */
  20   SS_PARTIAL,   /* defined, but can be bashed without error (partial structure returned) */
  21   SS_DEAD,      /* cannot use (after giving aways as only)
  22                  * same meaning as UNUSEABLE, except that we
  23                  * want to generate better error messages. */
  24   SS_HOFFA,     /* "probably dead" */
  25   SS_FIXED,     /* cannot modify */
  26   SS_RELDEF,    /* a structure field that may or may not be defined (up to
  27                  * programmer to worry about it. */
  28
  29   SS_UNDEFGLOB,   /* global only: undefined before call */
  30   SS_KILLED,      /* global only: undefined after call */
  31   SS_UNDEFKILLED, /* global only: undefined before and after call */
  32
  33   SS_SPECIAL,     /* marker for uses/defines/allocates/releases-specified */
  34
  35   SS_LAST
  36 } sstate;
  37
  38 extern bool sstate_isValid (/*@sef@*/ sstate) /*@*/ ;
  39 # define sstate_isValid(s) ((s) >= SS_UNKNOWN && (s) <= SS_LAST)
  40
  41 typedef enum {
  42   SCNONE,
  43   SCEXTERN,
  44   SCSTATIC
  45 } storageClassCode ;
  46
  47 typedef enum {
  48   NS_ERROR = -1,     /* error (suppress messages) */
  49   NS_UNKNOWN = 0,    /* no annotation */
  50   NS_NOTNULL,        /* definitely not null */
  51   NS_MNOTNULL,       /* marked with notnull */
  52
  53                      /* perhaps null */
  54   NS_RELNULL,        /* relaxed null --- okay null for set, not null for checking */
  55   NS_CONSTNULL,      /* null constant (for abstract types) */
  56
  57   /* don't change the order! */             /* possibly null */
  58   NS_POSNULL,        /* possibly null */
  59   NS_DEFNULL,        /* definitely null */
  60   NS_ABSNULL         /* null from abstract type definition (concrete type unknown) */
  61 } nstate;
  62
  63 extern bool nstate_isKnown (nstate p_n) /*@*/ ;
  64 # define nstate_isKnown(n) ((n) != NS_UNKNOWN)
  65
  66 extern bool nstate_isValid (/*@sef@*/ nstate p_n) /*@*/ ;
  67 # define nstate_isValid(n) ((n) >= NS_ERROR && (n) <= NS_ABSNULL)
  68
  69 /*
  70 ** aliasing states
  71 */
  72
  73 /*
  74 ** HEY STUPID!  Don't switch around the order!
  75 **
  76 ** These numbers are fixed into the library format.  If the order
  77 ** changes, remember to remake all libraries!
  78 */
  79
  80 typedef enum {
  81   AK_UNKNOWN = 0, /* AK_UNKNOWN must be first */
  82   AK_ERROR,
  83   AK_ONLY,
  84   AK_IMPONLY,
  85   AK_KEEP,
  86   AK_KEPT,
  87   AK_TEMP,  /* 6 */
  88   AK_IMPTEMP,
  89   AK_SHARED,
  90   AK_UNIQUE,
  91   AK_RETURNED, /* 10 */
  92   AK_FRESH,        /* local only storage (may be shared) */
  93   AK_STACK,        /* allocated on local stack */
  94   AK_REFCOUNTED,
  95   AK_REFS,
  96   AK_KILLREF,
  97   AK_NEWREF,
  98   AK_OWNED,
  99   AK_DEPENDENT, /* 18 */
 100   AK_IMPDEPENDENT,
 101   AK_STATIC,
 102   AK_LOCAL        /* AK_LOCAL must be last */
 103 } alkind;
 104
 105 typedef enum {
 106   XO_UNKNOWN,
 107   XO_NORMAL,
 108   XO_EXPOSED,
 109   XO_OBSERVER
 110 } exkind;
 111
 112 extern bool sstate_isKnown (sstate p_s) /*@*/ ;
 113 # define sstate_isKnown(s)      ((s) != SS_UNKNOWN)
 114
 115 extern bool sstate_isUnknown (sstate p_s) /*@*/ ;
 116 # define sstate_isUnknown(s)      ((s) == SS_UNKNOWN)
 117
 118 extern bool exkind_isUnknown (exkind p_e) /*@*/ ;
 119 # define exkind_isUnknown(e)    ((e) == XO_UNKNOWN)
 120
 121 extern bool exkind_isKnown (/*@sef@*/ exkind p_e) /*@*/ ;
 122 # define exkind_isKnown(e)      ((e) != XO_UNKNOWN && (e) != XO_NORMAL)
 123
 124 extern bool exkind_isValid (/*@sef@*/ exkind p_e) /*@*/ ;
 125 # define exkind_isValid(e)      ((e) >= XO_UNKNOWN && (e) <= XO_OBSERVER)
 126
 127 extern bool alkind_isValid (/*@sef@*/ alkind p_a) /*@*/ ;
 128 # define alkind_isValid(a) ((a) >= AK_UNKNOWN && (a) <= AK_LOCAL)
 129
 130 extern bool alkind_isImplicit (/*@sef@*/ alkind p_a) /*@*/ ;
 131 extern bool alkind_isDependent (/*@sef@*/ alkind p_a) /*@*/ ;
 132 extern bool alkind_isOnly (/*@sef@*/ alkind p_a) /*@*/ ;
 133 extern bool alkind_isTemp (/*@sef@*/ alkind p_a) /*@*/ ;
 134
 135 # define alkind_isImplicit(a)   (((a) == AK_IMPONLY || (a) == AK_IMPDEPENDENT \
 136                                  || (a) == AK_IMPTEMP))
 137 # define alkind_isDependent(a)  (((a) == AK_DEPENDENT || (a) == AK_IMPDEPENDENT))
 138 # define alkind_isOnly(a)       ((a) == AK_ONLY || (a) == AK_IMPONLY)
 139 # define alkind_isTemp(a)       (((a) == AK_TEMP || (a) == AK_IMPTEMP))
 140
 141 extern bool alkind_equal (alkind p_a1, alkind p_a2) /*@*/ ;
 142
 143 extern bool alkind_isOwned (alkind p_a) /*@*/ ;
 144 extern bool alkind_isStack (alkind p_a) /*@*/ ;
 145 extern bool alkind_isStatic (alkind p_a) /*@*/ ;
 146 extern bool alkind_isKeep (alkind p_a) /*@*/ ;
 147 extern bool alkind_isKept (alkind p_a) /*@*/ ;
 148 extern bool alkind_isUnique (alkind p_a) /*@*/ ;
 149 extern bool alkind_isError (alkind p_a) /*@*/ ;
 150 extern bool alkind_isFresh (alkind p_a) /*@*/ ;
 151 extern bool alkind_isShared (alkind p_a) /*@*/ ;
 152 extern bool alkind_isLocal (alkind p_a) /*@*/ ;
 153 extern bool alkind_isKnown (alkind p_a) /*@*/ ;
 154 extern bool alkind_isUnknown (alkind p_a) /*@*/ ;
 155 extern bool alkind_isRefCounted (alkind p_a) /*@*/ ;
 156 extern /*@unused@*/ bool alkind_isRefs (alkind p_a) /*@*/ ;
 157 extern bool alkind_isNewRef (alkind p_a) /*@*/ ;
 158 extern bool alkind_isKillRef (alkind p_a) /*@*/ ;
 159
 160 extern alkind alkind_resolve (alkind p_a1, alkind p_a2) /*@*/ ;
 161
 162 # define alkind_isOwned(a)      ((a) == AK_OWNED)
 163 # define alkind_isStack(a)      ((a) == AK_STACK)
 164 # define alkind_isStatic(a)     ((a) == AK_STATIC)
 165 # define alkind_isKeep(a)       ((a) == AK_KEEP)
 166 # define alkind_isKept(a)       ((a) == AK_KEPT)
 167 # define alkind_isUnique(a)     ((a) == AK_UNIQUE)
 168 # define alkind_isError(a)      ((a) == AK_ERROR)
 169 # define alkind_isFresh(a)      ((a) == AK_FRESH)
 170 # define alkind_isShared(a)     ((a) == AK_SHARED)
 171 # define alkind_isLocal(a)      ((a) == AK_LOCAL)
 172 # define alkind_isKnown(a)      ((a) != AK_UNKNOWN)
 173 # define alkind_isUnknown(a)    ((a) == AK_UNKNOWN)
 174 # define alkind_isRefCounted(a) ((a) == AK_REFCOUNTED)
 175 # define alkind_isRefs(a)       ((a) == AK_REFS)
 176 # define alkind_isNewRef(a)     ((a) == AK_NEWREF)
 177 # define alkind_isKillRef(a)    ((a) == AK_KILLREF)
 178
 179 extern /*@observer@*/ cstring sstate_unparse (sstate p_s) /*@*/ ;
 180
 181 extern alkind alkind_fromQual (qual p_q) /*@*/ ;
 182 extern alkind alkind_derive (alkind p_outer, alkind p_inner) /*@*/ ;
 183 extern /*@observer@*/ cstring alkind_unparse (alkind p_a) /*@*/ ;
 184 extern /*@observer@*/ cstring alkind_capName (alkind p_a) /*@*/ ;
 185 extern alkind alkind_fromInt (int p_n) /*@*/ ;
 186 extern nstate nstate_fromInt (int p_n) /*@*/ ;
 187 extern /*@observer@*/ cstring nstate_unparse (nstate p_n) /*@*/ ;
 188 extern int nstate_compare (nstate p_n1, nstate p_n2) /*@*/ ;
 189 extern bool nstate_possiblyNull (nstate p_n) /*@*/ ;
 190 extern bool nstate_perhapsNull (nstate p_n) /*@*/ ;
 191 extern sstate sstate_fromInt (int p_n) /*@*/ ;
 192 extern exkind exkind_fromInt (int p_n) /*@*/ ;
 193 extern exkind exkind_fromQual (qual p_q) /*@*/ ;
 194 extern /*@observer@*/ cstring exkind_unparse (exkind p_a) /*@*/ ;
 195 extern /*@observer@*/ cstring exkind_capName (exkind p_a) /*@*/ ;
 196 extern /*@observer@*/ cstring exkind_unparseError (exkind p_a) /*@*/ ;
 197 extern sstate sstate_fromQual (qual p_q) /*@*/ ;
 198 extern bool alkind_compatible (alkind p_a1, alkind p_a2) /*@*/ ;
 199 extern alkind alkind_fixImplicit (alkind p_a) /*@*/ ;
 200
 201 typedef enum
 202 {
 203   XK_ERROR,
 204   XK_UNKNOWN,
 205   XK_NEVERESCAPE,
 206   XK_GOTO,
 207   XK_MAYGOTO,
 208   XK_MAYEXIT,
 209   XK_MUSTEXIT,
 210   XK_TRUEEXIT,
 211   XK_FALSEEXIT,
 212   XK_MUSTRETURN,
 213   XK_MAYRETURN,
 214   XK_MAYRETURNEXIT,
 215   XK_MUSTRETURNEXIT /* must return or exit */
 216 } exitkind;
 217
 218 /*@constant exitkind XK_LAST; @*/
 219 # define XK_LAST XK_MUSTRETURNEXIT
 220
 221 extern exitkind exitkind_fromQual (qual p_q) /*@*/ ;
 222 extern /*@unused@*/ bool exitkind_isMustExit (exitkind p_e) /*@*/ ;
 223 # define exitkind_isMustExit(e) ((e) == XK_MUSTEXIT)
 224
 225 extern bool exitkind_equal (exitkind p_e1, exitkind p_e2) /*@*/ ;
 226 # define exitkind_equal(e1,e2) ((e1) == (e2))
 227
 228 extern bool exitkind_couldExit (exitkind p_e) /*@*/ ;
 229 extern bool exitkind_couldEscape (exitkind p_e) /*@*/ ;
 230 extern exitkind exitkind_fromInt (int p_x) /*@*/ ;
 231 extern /*@observer@*/ cstring exitkind_unparse (exitkind p_k) /*@*/ ;
 232
 233 extern bool exitkind_isKnown (exitkind p_e) /*@*/ ;
 234 # define exitkind_isKnown(e) ((e) != XK_UNKNOWN)
 235
 236 extern bool exitkind_isTrueExit (exitkind p_e) /*@*/ ;
 237 # define exitkind_isTrueExit(e) \
 238   ((e) == XK_TRUEEXIT)
 239
 240 extern bool exitkind_isConditionalExit (/*@sef@*/ exitkind p_e) /*@*/ ;
 241 # define exitkind_isConditionalExit(e) \
 242   ((e) == XK_TRUEEXIT || (e) == XK_FALSEEXIT)
 243
 244 extern bool exitkind_isError (/*@sef@*/ exitkind p_e) /*@*/ ;
 245 # define exitkind_isError(e) ((e) == XK_ERROR)
 246
 247 extern bool exitkind_mustExit (/*@sef@*/ exitkind p_e) /*@*/ ;
 248 # define exitkind_mustExit(e) ((e) == XK_MUSTEXIT)
 249
 250 extern bool exitkind_mustEscape (/*@sef@*/ exitkind p_e) /*@*/ ;
 251 # define exitkind_mustEscape(e) \
 252   ((e) == XK_MUSTEXIT || (e) == XK_MUSTRETURN \
 253    || (e) == XK_MUSTRETURNEXIT || (e) == XK_GOTO)
 254
 255 extern exitkind exitkind_makeConditional (exitkind p_k) /*@*/ ;
 256 extern exitkind exitkind_combine (exitkind p_k1, exitkind p_k2) /*@*/ ;
 257
 258 /*
 259 ** NOTE: combiners are in sRef
 260 */
 261
 262 # else
 263 # error "Multiple include"
 264 # endif