src/varKinds.c

   1 /*
   2 ** Splint - annotation-assisted static program checker
   3 ** Copyright (C) 1994-2003 University of Virginia,
   4 **         Massachusetts Institute of Technology
   5 **
   6 ** This program is free software; you can redistribute it and/or modify it
   7 ** under the terms of the GNU General Public License as published by the
   8 ** Free Software Foundation; either version 2 of the License, or (at your
   9 ** option) any later version.
  10 **
  11 ** This program is distributed in the hope that it will be useful, but
  12 ** WITHOUT ANY WARRANTY; without even the implied warranty of
  13 ** MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
  14 ** General Public License for more details.
  15 **
  16 ** The GNU General Public License is available from http://www.gnu.org/ or
  17 ** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  18 ** MA 02111-1307, USA.
  19 **
  20 ** For information on splint: info@splint.org
  21 ** To report a bug: splint-bug@splint.org
  22 ** For more information: http://www.splint.org
  23 */
  24 /*
  25 ** varKinds.c
  26 */
  27
  28 # include "splintMacros.nf"
  29 # include "basic.h"
  30
  31 alkind alkind_fromInt (int n)
  32 {
  33   /*@+enumint@*/
  34   if (n < AK_UNKNOWN || n > AK_LOCAL)
  35     {
  36       llbug (message ("Alias kind out of range: %d", n));
  37     }
  38   /*@=enumint@*/
  39
  40   return ((alkind)n);
  41 }
  42
  43 nstate nstate_fromInt (int n)
  44 {
  45   /*@+enumint@*/
  46   llassertprint (n >= NS_ERROR && n <= NS_ABSNULL,
  47                  ("Bad null state: %d", n));
  48   /*@=enumint@*/
  49
  50   return ((nstate)n);
  51 }
  52
  53 sstate sstate_fromInt (int n)
  54 {
  55   /*@+enumint@*/
  56   llassert (n >= SS_UNKNOWN && n < SS_LAST);
  57   /*@=enumint@*/
  58
  59   return ((sstate)n);
  60 }
  61
  62 exkind exkind_fromInt (int n)
  63 {
  64   /*@+enumint@*/
  65   llassert (n >= XO_UNKNOWN && n <= XO_OBSERVER);
  66   /*@=enumint@*/
  67
  68   return ((exkind) n);
  69 }
  70
  71 cstring sstate_unparse (sstate s)
  72 {
  73   switch (s)
  74     {
  75     case SS_UNKNOWN:   return cstring_makeLiteralTemp ("unknown");
  76     case SS_UNUSEABLE: return cstring_makeLiteralTemp ("unuseable");
  77     case SS_UNDEFINED: return cstring_makeLiteralTemp ("undefined");
  78     case SS_MUNDEFINED:return cstring_makeLiteralTemp ("possibly undefined");
  79     case SS_ALLOCATED: return cstring_makeLiteralTemp ("allocated");
  80     case SS_PDEFINED:  return cstring_makeLiteralTemp ("partially defined");
  81     case SS_DEFINED:   return cstring_makeLiteralTemp ("defined");
  82     case SS_PARTIAL:   return cstring_makeLiteralTemp ("partial");
  83     case SS_SPECIAL:   return cstring_makeLiteralTemp ("special");
  84     case SS_DEAD:      return cstring_makeLiteralTemp ("dead");
  85     case SS_HOFFA:     return cstring_makeLiteralTemp ("probably dead");
  86     case SS_FIXED:     return cstring_makeLiteralTemp ("unmodifiable");
  87     case SS_RELDEF:    return cstring_makeLiteralTemp ("reldef");
  88     case SS_LAST:      llcontbuglit ("sstate_unparse: last");
  89                        return cstring_makeLiteralTemp ("<error>");
  90     case SS_UNDEFGLOB:     return cstring_makeLiteralTemp ("undefglob");
  91     case SS_KILLED:    return cstring_makeLiteralTemp ("killed");
  92     case SS_UNDEFKILLED:
  93       return cstring_makeLiteralTemp ("undefkilled");
  94     }
  95
  96   BADEXIT;
  97 }
  98
  99 bool nstate_possiblyNull (nstate n)
 100 {
 101   /*
 102   ** note: not NS_UNKNOWN or NS_ERROR
 103   */
 104
 105   return ((n >= NS_CONSTNULL) && (n <= NS_ABSNULL));
 106 }
 107
 108 bool nstate_perhapsNull (nstate n)
 109 {
 110   /*
 111   ** note: not NS_UNKNOWN or NS_ERROR
 112   */
 113
 114   return ((n >= NS_RELNULL) && (n <= NS_ABSNULL));
 115 }
 116
 117 cstring nstate_unparse (nstate n)
 118 {
 119   switch (n)
 120     {
 121     case NS_ERROR:     return cstring_makeLiteralTemp ("<null error>");
 122     case NS_UNKNOWN:   return cstring_makeLiteralTemp ("implicitly non-null");
 123     case NS_POSNULL:   return cstring_makeLiteralTemp ("null");
 124     case NS_DEFNULL:   return cstring_makeLiteralTemp ("null");
 125     case NS_NOTNULL:   return cstring_makeLiteralTemp ("notnull");
 126     case NS_MNOTNULL:  return cstring_makeLiteralTemp ("notnull");
 127     case NS_ABSNULL:   return cstring_makeLiteralTemp ("null");
 128     case NS_RELNULL:   return cstring_makeLiteralTemp ("relnull");
 129     case NS_CONSTNULL: return cstring_makeLiteralTemp ("null");
 130     }
 131
 132   /*@notreached@*/ llcontbuglit ("bad null state!");
 133   /*@notreached@*/ return cstring_makeLiteralTemp ("!!! bad null state !!!");
 134   BADEXIT;
 135 }
 136
 137 /*
 138 ** ??? (used to do something different for guarded)
 139 */
 140
 141 int nstate_compare (nstate n1, nstate n2)
 142 {
 143   return (generic_compare (n1, n2));
 144 }
 145
 146 /*
 147 ** This occurs when we select a field with alkind inner,
 148 ** from a structure with alkind outer.  It is probably
 149 ** unnecessary.
 150 */
 151
 152 alkind alkind_derive (alkind outer, alkind inner)
 153 {
 154   switch (outer)
 155     {
 156     case AK_ERROR:
 157     case AK_UNKNOWN: return inner;
 158     case AK_KEPT:
 159     case AK_KEEP:
 160     case AK_ONLY:
 161     case AK_IMPONLY:
 162     case AK_OWNED:
 163     case AK_IMPDEPENDENT:
 164     case AK_DEPENDENT:
 165       if (inner == AK_SHARED) return AK_SHARED;
 166       else if (outer == AK_DEPENDENT) return AK_IMPDEPENDENT;
 167       else if (outer == AK_ONLY) return AK_IMPONLY;
 168       else return outer;
 169       /* not so sure about these? */
 170     case AK_REFCOUNTED:
 171     case AK_NEWREF:
 172     case AK_KILLREF:
 173     case AK_REFS:
 174     case AK_STACK:
 175     case AK_STATIC:
 176       return outer;
 177     case AK_TEMP:
 178     case AK_IMPTEMP:
 179     case AK_SHARED:
 180     case AK_UNIQUE:
 181     case AK_LOCAL:
 182     case AK_FRESH:
 183     case AK_RETURNED:
 184       if (alkind_isKnown (inner)) return inner;
 185       else return outer;
 186     }
 187   BADEXIT;
 188 }
 189
 190 cstring alkind_unparse (alkind a)
 191 {
 192   switch (a)
 193     {
 194     case AK_ERROR:           return cstring_makeLiteralTemp ("<error>");
 195     case AK_UNKNOWN:         return cstring_makeLiteralTemp ("unqualified");
 196     case AK_ONLY:            return cstring_makeLiteralTemp ("only");
 197     case AK_IMPONLY:         return cstring_makeLiteralTemp ("implicitly only");
 198     case AK_OWNED:           return cstring_makeLiteralTemp ("owned");
 199     case AK_IMPDEPENDENT:    return cstring_makeLiteralTemp ("implicitly dependent");
 200     case AK_DEPENDENT:       return cstring_makeLiteralTemp ("dependent");
 201     case AK_KEEP:            return cstring_makeLiteralTemp ("keep");
 202     case AK_KEPT:            return cstring_makeLiteralTemp ("kept");
 203     case AK_IMPTEMP:         return cstring_makeLiteralTemp ("implicitly temp");
 204     case AK_TEMP:            return cstring_makeLiteralTemp ("temp");
 205     case AK_SHARED:          return cstring_makeLiteralTemp ("shared");
 206     case AK_UNIQUE:          return cstring_makeLiteralTemp ("unique");
 207     case AK_RETURNED:        return cstring_makeLiteralTemp ("returned");
 208     case AK_FRESH:           return cstring_makeLiteralTemp ("fresh");
 209     case AK_STACK:           return cstring_makeLiteralTemp ("stack");
 210     case AK_REFCOUNTED:      return cstring_makeLiteralTemp ("refcounted");
 211     case AK_REFS:            return cstring_makeLiteralTemp ("refs");
 212     case AK_KILLREF:         return cstring_makeLiteralTemp ("killref");
 213     case AK_NEWREF:          return cstring_makeLiteralTemp ("newref");
 214     case AK_LOCAL:           return cstring_makeLiteralTemp ("local");
 215     case AK_STATIC:          return cstring_makeLiteralTemp ("unqualified static");
 216     }
 217     BADEXIT;
 218 }
 219
 220 cstring exkind_unparse (exkind a)
 221 {
 222   switch (a)
 223     {
 224     case XO_UNKNOWN:         return cstring_makeLiteralTemp ("unknown");
 225     case XO_NORMAL:          return cstring_makeLiteralTemp ("unexposed");
 226     case XO_EXPOSED:         return cstring_makeLiteralTemp ("exposed");
 227     case XO_OBSERVER:        return cstring_makeLiteralTemp ("observer");
 228     }
 229   BADEXIT;
 230 }
 231
 232 cstring exkind_capName (exkind a)
 233 {
 234   switch (a)
 235     {
 236     case XO_UNKNOWN:         return cstring_makeLiteralTemp ("Unknown");
 237     case XO_NORMAL:          return cstring_makeLiteralTemp ("Unexposed");
 238     case XO_EXPOSED:         return cstring_makeLiteralTemp ("Exposed");
 239     case XO_OBSERVER:        return cstring_makeLiteralTemp ("Observer");
 240     }
 241   BADEXIT;
 242 }
 243
 244 cstring exkind_unparseError (exkind a)
 245 {
 246   switch (a)
 247     {
 248     case XO_UNKNOWN:         return cstring_makeLiteralTemp ("unqualified");
 249     case XO_NORMAL:          return cstring_makeLiteralTemp ("unqualifier");
 250     case XO_EXPOSED:         return cstring_makeLiteralTemp ("exposed");
 251     case XO_OBSERVER:        return cstring_makeLiteralTemp ("observer");
 252     }
 253   BADEXIT;
 254 }
 255
 256 cstring alkind_capName (alkind a)
 257 {
 258   switch (a)
 259     {
 260     case AK_ERROR:
 261       return cstring_makeLiteralTemp ("<Error>");
 262     case AK_UNKNOWN:
 263       return cstring_makeLiteralTemp ("Unqualified");
 264     case AK_ONLY:
 265       return cstring_makeLiteralTemp ("Only");
 266     case AK_IMPONLY:
 267       return cstring_makeLiteralTemp ("Implicitly only");
 268     case AK_OWNED:
 269       return cstring_makeLiteralTemp ("Owned");
 270     case AK_IMPDEPENDENT:
 271       return cstring_makeLiteralTemp ("Implicitly dependent");
 272     case AK_DEPENDENT:
 273       return cstring_makeLiteralTemp ("Dependent");
 274     case AK_KEEP:
 275       return cstring_makeLiteralTemp ("Keep");
 276     case AK_KEPT:
 277       return cstring_makeLiteralTemp ("Kept");
 278     case AK_IMPTEMP:
 279       return cstring_makeLiteralTemp ("Implicitly temp");
 280     case AK_TEMP:
 281       return cstring_makeLiteralTemp ("Temp");
 282     case AK_SHARED:
 283       return cstring_makeLiteralTemp ("Shared");
 284     case AK_UNIQUE:
 285       return cstring_makeLiteralTemp ("Unique");
 286     case AK_RETURNED:
 287       return cstring_makeLiteralTemp ("Returned");
 288     case AK_FRESH:
 289       return cstring_makeLiteralTemp ("Fresh");
 290     case AK_STACK:
 291       return cstring_makeLiteralTemp ("Stack");
 292     case AK_REFCOUNTED:
 293       return cstring_makeLiteralTemp ("Refcounted");
 294     case AK_REFS:
 295       return cstring_makeLiteralTemp ("Refs");
 296     case AK_KILLREF:
 297       return cstring_makeLiteralTemp ("Killref");
 298     case AK_NEWREF:
 299       return cstring_makeLiteralTemp ("Newref");
 300     case AK_LOCAL:
 301       return cstring_makeLiteralTemp ("Local");
 302     case AK_STATIC:
 303       return cstring_makeLiteralTemp ("Unqualified static");
 304     }
 305   BADEXIT;
 306 }
 307
 308 exkind
 309 exkind_fromQual (qual q)
 310 {
 311   if (qual_isExposed (q)) {
 312     return XO_EXPOSED;
 313   } else if (qual_isObserver (q)) {
 314     return XO_OBSERVER;
 315   } else
 316     {
 317       llcontbug (message ("exkind_fromQual: not exp qualifier: %s" ,
 318                           qual_unparse (q)));
 319       return XO_UNKNOWN;
 320     }
 321 }
 322
 323 sstate
 324 sstate_fromQual (qual q)
 325 {
 326   if (qual_isOut (q))          return SS_ALLOCATED;
 327   if (qual_isIn (q))           return SS_DEFINED;
 328   else if (qual_isPartial (q)) return SS_PARTIAL;
 329   else if (qual_isRelDef (q))  return SS_RELDEF;
 330   else if (qual_isUndef (q))   return SS_UNDEFGLOB;
 331   else if (qual_isKilled (q))  return SS_KILLED;
 332   else if (qual_isSpecial (q)) return SS_SPECIAL;
 333   else
 334     {
 335       llcontbug (message ("sstate_fromQual: not alias qualifier: %s",
 336                           qual_unparse (q)));
 337       return SS_UNKNOWN;
 338     }
 339 }
 340
 341 exitkind
 342 exitkind_fromQual (qual q)
 343 {
 344   if (qual_isExits (q))     return XK_MUSTEXIT;
 345   if (qual_isMayExit (q))   return XK_MAYEXIT;
 346   if (qual_isTrueExit (q))  return XK_TRUEEXIT;
 347   if (qual_isFalseExit (q)) return XK_FALSEEXIT;
 348   if (qual_isNeverExit (q)) return XK_NEVERESCAPE;
 349   else
 350     {
 351       llcontbug (message ("exitkind_fromQual: not exit qualifier: %s",
 352                           qual_unparse (q)));
 353       return XK_UNKNOWN;
 354     }
 355 }
 356
 357 alkind
 358 alkind_fromQual (qual q)
 359 {
 360   if (qual_isOnly (q))       return AK_ONLY;
 361   if (qual_isImpOnly (q))    return AK_IMPONLY;
 362   if (qual_isKeep (q))       return AK_KEEP;
 363   if (qual_isKept (q))       return AK_KEPT;
 364   if (qual_isTemp (q))       return AK_TEMP;
 365   if (qual_isShared (q))     return AK_SHARED;
 366   if (qual_isUnique (q))     return AK_UNIQUE;
 367   if (qual_isRefCounted (q)) return AK_REFCOUNTED;
 368   if (qual_isRefs (q))       return AK_REFS;
 369   if (qual_isNewRef (q))     return AK_NEWREF;
 370   if (qual_isKillRef (q))    return AK_KILLREF;
 371   if (qual_isTempRef (q))    return AK_KILLREF; /* kludge? use kill ref for this */
 372   if (qual_isOwned (q))      return AK_OWNED;
 373   if (qual_isDependent (q))  return AK_DEPENDENT;
 374
 375   llcontbug (message ("alkind_fromQual: not alias qualifier: %s", qual_unparse (q)));
 376   return AK_ERROR;
 377 }
 378
 379 static bool alkind_isMeaningless (alkind a1)
 380 {
 381   return (a1 == AK_ERROR || a1 == AK_UNKNOWN || a1 == AK_RETURNED
 382           || a1 == AK_STACK || a1 == AK_REFCOUNTED
 383           || a1 == AK_REFS || a1 == AK_KILLREF || a1 == AK_NEWREF
 384           || a1 == AK_LOCAL);
 385 }
 386
 387 bool alkind_compatible (alkind a1, alkind a2)
 388 {
 389   if (a1 == a2) return TRUE;
 390   if (a2 == AK_ERROR) return TRUE;
 391   if (a2 == AK_UNKNOWN)
 392     {
 393       return (alkind_isMeaningless (a1) || (a1 == AK_IMPTEMP));
 394     }
 395
 396   switch (a1)
 397     {
 398     case AK_ERROR:               return TRUE;
 399     case AK_UNKNOWN:             return (alkind_isMeaningless (a2)
 400                                          || (a2 == AK_IMPTEMP));
 401     case AK_IMPONLY:             return (a2 == AK_KEEP || a2 == AK_FRESH
 402                                          || a2 == AK_ONLY);
 403     case AK_ONLY:                return (a2 == AK_KEEP || a2 == AK_FRESH
 404                                          || a2 == AK_IMPONLY);
 405     case AK_OWNED:               return FALSE;
 406     case AK_IMPDEPENDENT:        return (a2 == AK_DEPENDENT);
 407     case AK_DEPENDENT:           return (a2 == AK_IMPDEPENDENT);
 408     case AK_KEEP:                return (a2 == AK_ONLY || a2 == AK_FRESH
 409                                          || a2 == AK_IMPONLY);
 410     case AK_KEPT:                return FALSE;
 411     case AK_IMPTEMP:             return (a2 == AK_TEMP);
 412     case AK_TEMP:                return (a2 == AK_IMPTEMP);
 413     case AK_SHARED:              return FALSE;
 414     case AK_UNIQUE:              return (a2 == AK_TEMP);
 415     case AK_RETURNED:            return (alkind_isMeaningless (a2));
 416     case AK_FRESH:               return (alkind_isOnly (a2));
 417     case AK_STACK:               return (alkind_isMeaningless (a2));
 418     case AK_REFCOUNTED:          return (alkind_isMeaningless (a2));
 419     case AK_REFS:                return (alkind_isMeaningless (a2));
 420     case AK_KILLREF:             return (alkind_isMeaningless (a2));
 421     case AK_NEWREF:              return (alkind_isMeaningless (a2));
 422     case AK_LOCAL:               return (alkind_isMeaningless (a2));
 423     case AK_STATIC:              return (alkind_isMeaningless (a2));
 424     }
 425   BADEXIT;
 426 }
 427
 428 bool alkind_equal (alkind a1, alkind a2)
 429 {
 430   if (a1 == a2) return TRUE;
 431   if (a2 == AK_ERROR) return TRUE;
 432
 433   switch (a1)
 434     {
 435     case AK_ERROR:               return TRUE;
 436     case AK_IMPONLY:             return (a2 == AK_ONLY);
 437     case AK_ONLY:                return (a2 == AK_IMPONLY);
 438     case AK_IMPDEPENDENT:        return (a2 == AK_DEPENDENT);
 439     case AK_DEPENDENT:           return (a2 == AK_IMPDEPENDENT);
 440     case AK_IMPTEMP:             return (a2 == AK_TEMP);
 441     case AK_TEMP:                return (a2 == AK_IMPTEMP);
 442     default:                     return FALSE;
 443     }
 444
 445   BADEXIT;
 446 }
 447
 448 alkind
 449 alkind_fixImplicit (alkind a)
 450 {
 451   if (a == AK_IMPTEMP) return AK_TEMP;
 452   if (a == AK_IMPONLY) return AK_IMPONLY;
 453   if (a == AK_IMPDEPENDENT) return AK_DEPENDENT;
 454
 455   return a;
 456 }
 457
 458 cstring exitkind_unparse (exitkind k)
 459 {
 460   switch (k)
 461     {
 462     case XK_ERROR:       return (cstring_makeLiteralTemp ("<error>"));
 463     case XK_UNKNOWN:     return (cstring_makeLiteralTemp ("?"));
 464     case XK_NEVERESCAPE: return (cstring_makeLiteralTemp ("never escape"));
 465     case XK_MAYEXIT:     return (cstring_makeLiteralTemp ("mayexit"));
 466     case XK_MUSTEXIT:    return (cstring_makeLiteralTemp ("exits"));
 467     case XK_TRUEEXIT:    return (cstring_makeLiteralTemp ("trueexit"));
 468     case XK_FALSEEXIT:   return (cstring_makeLiteralTemp ("falseexit"));
 469     case XK_MUSTRETURN:  return (cstring_makeLiteralTemp ("mustreturn"));
 470     case XK_MAYRETURN:   return (cstring_makeLiteralTemp ("mayreturn"));
 471     case XK_MUSTRETURNEXIT: return (cstring_makeLiteralTemp ("mustreturnexit"));
 472     case XK_MAYRETURNEXIT: return (cstring_makeLiteralTemp ("mayreturnexit"));
 473     case XK_GOTO:        return (cstring_makeLiteralTemp ("goto"));
 474     case XK_MAYGOTO:     return (cstring_makeLiteralTemp ("maygoto"));
 475     }
 476
 477  BADEXIT;
 478 }
 479
 480 exitkind exitkind_makeConditional (exitkind k)
 481 {
 482   switch (k)
 483     {
 484     case XK_TRUEEXIT:
 485     case XK_FALSEEXIT:
 486     case XK_MUSTEXIT:       return XK_MAYEXIT;
 487     case XK_MUSTRETURN:     return XK_MAYRETURN;
 488     case XK_MUSTRETURNEXIT: return XK_MAYRETURNEXIT;
 489     case XK_GOTO:           return XK_MAYGOTO;
 490     default:                return k;
 491     }
 492 }
 493
 494 exitkind exitkind_combine (exitkind k1, exitkind k2)
 495 {
 496   if (k1 == k2)
 497     {
 498       return k1;
 499     }
 500
 501   if (k2 == XK_ERROR)
 502     {
 503       return XK_ERROR;
 504     }
 505
 506   switch (k1)
 507     {
 508     case XK_ERROR: return XK_ERROR;
 509     case XK_UNKNOWN:
 510     case XK_NEVERESCAPE: return (exitkind_makeConditional (k2));
 511     case XK_MUSTEXIT:
 512       switch (k2)
 513         {
 514         case XK_MUSTRETURNEXIT:
 515         case XK_MUSTRETURN: return XK_MUSTRETURNEXIT;
 516         case XK_MAYRETURNEXIT:
 517         case XK_MAYRETURN:  return XK_MAYRETURNEXIT;
 518         default:             return XK_MAYEXIT;
 519         }
 520       BADEXIT;
 521
 522     case XK_MAYEXIT:
 523     case XK_TRUEEXIT:
 524     case XK_FALSEEXIT:
 525       switch (k2)
 526         {
 527         case XK_MUSTRETURNEXIT:
 528         case XK_MAYRETURNEXIT:
 529         case XK_MAYRETURN:
 530         case XK_MUSTRETURN: return XK_MAYRETURNEXIT;
 531         default:             return XK_MAYEXIT;
 532         }
 533       BADEXIT;
 534
 535     case XK_MUSTRETURN:
 536       switch (k2)
 537         {
 538         case XK_MUSTRETURNEXIT:
 539         case XK_MUSTEXIT:    return XK_MUSTRETURNEXIT;
 540         case XK_MAYRETURNEXIT:
 541         case XK_TRUEEXIT:
 542         case XK_FALSEEXIT:
 543         case XK_MAYEXIT:     return XK_MAYRETURNEXIT;
 544         default:              return XK_MAYRETURN;
 545         }
 546       BADEXIT;
 547
 548     case XK_MAYRETURN:
 549       if (exitkind_couldExit (k2))
 550         {
 551           return XK_MAYRETURNEXIT;
 552         }
 553       else
 554         {
 555           return XK_MAYRETURN;
 556         }
 557
 558     case XK_MUSTRETURNEXIT:
 559       switch (k2)
 560         {
 561         case XK_MUSTRETURN:
 562         case XK_MUSTEXIT:    return XK_MUSTRETURNEXIT;
 563         default:              return XK_MAYRETURNEXIT;
 564         }
 565       BADEXIT;
 566
 567     case XK_MAYRETURNEXIT:   return XK_MAYRETURNEXIT;
 568     case XK_GOTO:
 569     case XK_MAYGOTO:
 570       if (exitkind_couldExit (k2))
 571         {
 572           return XK_MAYRETURNEXIT;
 573         }
 574       return XK_MAYGOTO;
 575     }
 576
 577  BADEXIT;
 578 }
 579
 580 bool exitkind_couldExit (exitkind e)
 581 {
 582   switch (e)
 583     {
 584     case XK_MAYEXIT:
 585     case XK_MUSTEXIT:
 586     case XK_TRUEEXIT:
 587     case XK_FALSEEXIT:
 588     case XK_MAYRETURNEXIT:
 589     case XK_MUSTRETURNEXIT:
 590     case XK_GOTO:
 591     case XK_MAYGOTO: return TRUE;
 592     default: return FALSE;
 593     }
 594 }
 595
 596 static bool exitkind_couldReturn (exitkind e) /*@*/
 597 {
 598   switch (e)
 599     {
 600     case XK_MUSTRETURN:
 601     case XK_MAYRETURN:
 602     case XK_MAYRETURNEXIT:
 603     case XK_MUSTRETURNEXIT:  return TRUE;
 604     default: return FALSE;
 605     }
 606 }
 607
 608 static bool exitkind_couldGoto (exitkind e) /*@*/
 609 {
 610   return (e == XK_GOTO || e == XK_MAYGOTO);
 611 }
 612
 613 bool exitkind_couldEscape (exitkind e)
 614 {
 615   return exitkind_couldReturn (e) || exitkind_couldExit (e)
 616     || exitkind_couldGoto (e);
 617 }
 618
 619 exitkind exitkind_fromInt (int x)
 620 {
 621   /*@+enumint@*/
 622   llassert (x >= XK_ERROR && x <= XK_LAST);
 623   /*@=enumint@*/
 624
 625   return (exitkind) x;
 626 }
 627
 628
 629
 630
 631
 632
 633