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 265