src/stateClause.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 ** stateClause.c
  26 */
  27
  28 # include "splintMacros.nf"
  29 # include "basic.h"
  30 # include "cgrammar.h"
  31 # include "cgrammar_tokens.h"
  32
  33 static stateClause
  34 stateClause_createRaw (stateConstraint st, stateClauseKind sk, /*@only@*/ sRefSet s)
  35 {
  36   stateClause ret = (stateClause) dmalloc (sizeof (*ret));
  37
  38   ret->state = st;
  39   ret->kind = sk;
  40   ret->squal = qual_createUnknown ();
  41   ret->refs = s;
  42   ret->loc = fileloc_undefined;
  43   return ret;
  44 }
  45
  46 stateClause
  47 stateClause_create (lltok tok, qual q, sRefSet s)
  48 {
  49   stateClause ret = (stateClause) dmalloc (sizeof (*ret));
  50
  51   if (lltok_getTok (tok) == QPRECLAUSE)
  52     {
  53       ret->state = TK_BEFORE;
  54     }
  55   else if (lltok_getTok (tok) == QPOSTCLAUSE)
  56     {
  57       ret->state = TK_AFTER;
  58     }
  59   else
  60     {
  61       BADBRANCH;
  62     }
  63
  64   ret->loc = fileloc_copy (lltok_getLoc (tok));
  65
  66   ret->squal = q;
  67   ret->refs = s;
  68
  69   if (sRefSet_isDefined (s))
  70     {
  71       ret->kind = SP_QUAL;
  72     }
  73   else
  74     {
  75       ret->kind = SP_GLOBAL;
  76     }
  77
  78   return ret;
  79 }
  80
  81 bool stateClause_isBeforeOnly (stateClause cl)
  82 {
  83   return (cl->state == TK_BEFORE);
  84 }
  85
  86 bool stateClause_isBefore (stateClause cl)
  87 {
  88   return (cl->state == TK_BEFORE || cl->state == TK_BOTH);
  89 }
  90
  91 bool stateClause_isAfter (stateClause cl)
  92 {
  93   return (cl->state == TK_AFTER || cl->state == TK_BOTH);
  94 }
  95
  96 bool stateClause_isEnsures (stateClause cl)
  97 {
  98   return (cl->state == TK_AFTER);
  99 }
 100
 101 bool stateClause_isQual (stateClause cl)
 102 {
 103   return (cl->kind == SP_QUAL);
 104 }
 105
 106 bool stateClause_isMemoryAllocation (stateClause cl)
 107 {
 108   switch (cl->kind)
 109     {
 110     case SP_ALLOCATES:
 111     case SP_RELEASES:
 112       return TRUE;
 113     case SP_USES:
 114     case SP_DEFINES:
 115     case SP_SETS:
 116       return FALSE;
 117     case SP_GLOBAL:
 118       return FALSE;
 119     case SP_QUAL:
 120       return (qual_isMemoryAllocation (cl->squal)
 121               || qual_isSharing (cl->squal));
 122     }
 123
 124   BADEXIT;
 125 }
 126
 127 /*
 128 ** An error is reported if the test is NOT true.
 129 */
 130 \r
 131 # ifdef WIN32\r
 132 /* Microsoft doesn't believe in higher order functions... */\r
 133 # pragma warning( disable : 4550 )\r
 134 # endif  \r
 135
 136 sRefTest stateClause_getPreTestFunction (stateClause cl)
 137 {
 138   switch (cl->kind)
 139     {
 140     case SP_USES:
 141       return sRef_isStrictReadable;
 142     case SP_ALLOCATES:
 143       return sRef_hasNoStorage;
 144     case SP_DEFINES:
 145       return sRef_hasNoStorage;
 146     case SP_SETS:
 147       return sRef_isNotUndefined;
 148     case SP_RELEASES:
 149       return sRef_isNotUndefined;
 150     case SP_GLOBAL:
 151       BADBRANCH;
 152     case SP_QUAL:
 153       {
 154         if (qual_isOnly (cl->squal)) {
 155           return sRef_isOnly;
 156         } else if (qual_isShared (cl->squal)) {
 157           return sRef_isShared;
 158         } else if (qual_isDependent (cl->squal)) {
 159           return sRef_isDependent;
 160         } else if (qual_isOwned (cl->squal)) {
 161           return sRef_isOwned;
 162         } else if (qual_isObserver (cl->squal)) {
 163           return sRef_isObserver;
 164         } else if (qual_isExposed (cl->squal)) {
 165           return sRef_isExposed;
 166         } else if (qual_isNotNull (cl->squal)) {
 167           return sRef_isNotNull;
 168         } else if (qual_isIsNull (cl->squal)) {
 169           return sRef_isDefinitelyNull;
 170         } else {
 171           BADBRANCH;
 172         }
 173       }
 174   }
 175
 176   BADEXIT;
 177 }
 178
 179 sRefTest stateClause_getPostTestFunction (stateClause cl)
 180 {
 181   llassert (stateClause_isAfter (cl));
 182
 183   switch (cl->kind)
 184     {
 185     case SP_USES:
 186       return NULL;
 187     case SP_ALLOCATES:
 188       return sRef_isAllocated;
 189     case SP_DEFINES:
 190       return sRef_isReallyDefined;
 191     case SP_SETS:
 192       return sRef_isReallyDefined;
 193     case SP_RELEASES:
 194       return sRef_isDeadStorage;
 195     case SP_GLOBAL:
 196       BADBRANCH;
 197     case SP_QUAL:
 198       if (qual_isOnly (cl->squal)) {
 199         return sRef_isOnly;
 200       } else if (qual_isShared (cl->squal)) {
 201         return sRef_isShared;
 202       } else if (qual_isDependent (cl->squal)) {
 203         return sRef_isDependent;
 204       } else if (qual_isOwned (cl->squal)) {
 205         return sRef_isOwned;
 206       } else if (qual_isObserver (cl->squal)) {
 207         return sRef_isObserver;
 208       } else if (qual_isExposed (cl->squal)) {
 209         return sRef_isExposed;
 210       } else if (qual_isNotNull (cl->squal)) {
 211         return sRef_isNotNull;
 212       } else if (qual_isIsNull (cl->squal)) {
 213         return sRef_isDefinitelyNull;
 214       } else {
 215         BADBRANCH;
 216       }
 217     }
 218
 219   BADEXIT;
 220 }
 221
 222 sRefShower stateClause_getPostTestShower (stateClause cl)
 223 {
 224   switch (cl->kind)
 225     {
 226     case SP_USES:
 227     case SP_ALLOCATES:
 228       return NULL;
 229     case SP_DEFINES:
 230     case SP_SETS:
 231       return sRef_showNotReallyDefined;
 232     case SP_RELEASES:
 233       return NULL;
 234     case SP_GLOBAL:
 235       BADBRANCH;
 236     case SP_QUAL:
 237       if (qual_isMemoryAllocation (cl->squal)) {
 238         return sRef_showAliasInfo;
 239       } else if (qual_isSharing (cl->squal)) {
 240         return sRef_showExpInfo;
 241       } else if (qual_isIsNull (cl->squal) || qual_isNotNull (cl->squal)) {
 242         return sRef_showNullInfo;
 243       } else {
 244         BADBRANCH;
 245       }
 246     }
 247
 248   BADEXIT;
 249 }
 250
 251 sRefMod stateClause_getEntryFunction (stateClause cl)
 252 {
 253   if (cl->state == TK_BEFORE || cl->state == TK_BOTH)
 254     {
 255       switch (cl->kind)
 256         {
 257         case SP_USES:
 258           return sRef_setDefinedComplete;
 259         case SP_ALLOCATES:
 260           return sRef_setUndefined; /* evans 2002-01-01 */
 261         case SP_DEFINES:
 262           return sRef_setUndefined; /* evans 2002-01-01 */
 263         case SP_SETS:
 264           return sRef_setAllocatedComplete;
 265         case SP_RELEASES:
 266           return sRef_setDefinedComplete;
 267         case SP_GLOBAL:
 268           BADBRANCH;
 269         case SP_QUAL:
 270           if (qual_isOnly (cl->squal)) {
 271             return sRef_setOnly;
 272           } else if (qual_isShared (cl->squal)) {
 273             return sRef_setShared;
 274           } else if (qual_isDependent (cl->squal)) {
 275             return sRef_setDependent;
 276           } else if (qual_isOwned (cl->squal)) {
 277             return sRef_setOwned;
 278           } else if (qual_isObserver (cl->squal)) {
 279             return sRef_setObserver;
 280           } else if (qual_isExposed (cl->squal)) {
 281             return sRef_setExposed;
 282           } else if (qual_isNotNull (cl->squal)) {
 283             return sRef_setNotNull;
 284           } else if (qual_isIsNull (cl->squal)) {
 285             return sRef_setDefNull;
 286           } else {
 287             DPRINTF (("Here we are: %s",
 288                       qual_unparse (cl->squal)));
 289             BADBRANCH;
 290           }
 291         }
 292
 293       BADBRANCH;
 294     }
 295   else
 296     {
 297       return NULL;
 298     }
 299
 300   BADBRANCHNULL;
 301 }
 302
 303 sRefMod stateClause_getEffectFunction (stateClause cl)
 304 {
 305   if (cl->state == TK_AFTER || cl->state == TK_BOTH)
 306     {
 307       switch (cl->kind)
 308         {
 309         case SP_USES:
 310           return NULL;
 311         case SP_ALLOCATES:
 312           return sRef_setAllocatedComplete;
 313         case SP_DEFINES:
 314           return sRef_setDefinedNCComplete;
 315         case SP_SETS:
 316           return sRef_setDefinedNCComplete;
 317         case SP_RELEASES:
 318           return sRef_killComplete;
 319         case SP_GLOBAL:
 320           BADBRANCH;
 321         case SP_QUAL:
 322           if (qual_isOnly (cl->squal)) {
 323             return sRef_setOnly;
 324           } else if (qual_isShared (cl->squal)) {
 325             return sRef_setShared;
 326           } else if (qual_isDependent (cl->squal)) {
 327             return sRef_setDependent;
 328           } else if (qual_isOwned (cl->squal)) {
 329             return sRef_setOwned;
 330           } else if (qual_isObserver (cl->squal)) {
 331             return sRef_setObserver;
 332           } else if (qual_isExposed (cl->squal)) {
 333             return sRef_setExposed;
 334           } else if (qual_isNotNull (cl->squal)) {
 335             return sRef_setNotNull;
 336           } else if (qual_isIsNull (cl->squal)) {
 337             return sRef_setDefNull;
 338           } else {
 339             BADBRANCH;
 340           }
 341         }
 342
 343       BADBRANCH;
 344     }
 345   else
 346     {
 347       return NULL;
 348     }
 349
 350   BADBRANCHNULL;
 351 }
 352
 353 sRefMod stateClause_getReturnEffectFunction (stateClause cl)
 354 {
 355   if (cl->state == TK_AFTER || cl->state == TK_BOTH)
 356     {
 357       switch (cl->kind)
 358         {
 359         case SP_USES:
 360         case SP_ALLOCATES:
 361         case SP_DEFINES:
 362         case SP_SETS:
 363         case SP_RELEASES:
 364           return NULL;
 365         case SP_GLOBAL:
 366           BADBRANCH;
 367         case SP_QUAL:
 368           if (qual_isOnly (cl->squal)) {
 369             return sRef_killComplete;
 370           } else {
 371             return NULL;
 372           }
 373         }
 374
 375       BADBRANCH;
 376     }
 377   else
 378     {
 379       return NULL;
 380     }
 381
 382   BADBRANCHNULL;
 383 }
 384
 385 static flagcode stateClause_qualErrorCode (stateClause cl)
 386 {
 387   if (qual_isOnly (cl->squal)) {
 388     return FLG_ONLYTRANS;
 389   } else if (qual_isShared (cl->squal)) {
 390     return FLG_SHAREDTRANS;
 391   } else if (qual_isDependent (cl->squal)) {
 392     return FLG_DEPENDENTTRANS;
 393   } else if (qual_isOwned (cl->squal)) {
 394     return FLG_OWNEDTRANS;
 395   } else if (qual_isObserver (cl->squal)) {
 396     return FLG_OBSERVERTRANS;
 397   } else if (qual_isExposed (cl->squal)) {
 398     return FLG_EXPOSETRANS;
 399   } else if (qual_isIsNull (cl->squal)
 400              || qual_isNotNull (cl->squal)) {
 401     return FLG_NULLSTATE;
 402   } else {
 403     BADBRANCH;
 404   }
 405
 406   BADBRANCHRET (INVALID_FLAG);
 407 }
 408
 409 flagcode stateClause_preErrorCode (stateClause cl)
 410 {
 411   llassert (cl->state == TK_BOTH || cl->state == TK_BEFORE);
 412
 413   switch (cl->kind)
 414     {
 415     case SP_USES:
 416       return FLG_USEDEF;
 417     case SP_ALLOCATES: /*@fallthrough@*/
 418     case SP_DEFINES:
 419     case SP_SETS:
 420       return FLG_MUSTFREEONLY;
 421     case SP_RELEASES:
 422       return FLG_USEDEF;
 423     case SP_GLOBAL:
 424     case SP_QUAL:
 425       return stateClause_qualErrorCode (cl);
 426     }
 427
 428   BADBRANCHRET (INVALID_FLAG);
 429 }
 430
 431 static /*@observer@*/ cstring stateClause_qualErrorString (stateClause cl, sRef sr)
 432 {
 433   if (qual_isMemoryAllocation (cl->squal)) {
 434     return alkind_capName (sRef_getAliasKind (sr));
 435   } else if (qual_isObserver (cl->squal)) {
 436     return cstring_makeLiteralTemp ("Non-observer");
 437   } else if (qual_isExposed (cl->squal)) {
 438     if (sRef_isObserver (sr))
 439       {
 440         return cstring_makeLiteralTemp ("Observer");
 441       }
 442     else
 443       {
 444         return cstring_makeLiteralTemp ("Non-exposed");
 445       }
 446   } else if (qual_isNotNull (cl->squal)) {
 447     if (sRef_isDefinitelyNull (sr))
 448       {
 449         return cstring_makeLiteralTemp ("Null");
 450       }
 451     else
 452       {
 453         return cstring_makeLiteralTemp ("Possibly null");
 454       }
 455   } else if (qual_isIsNull (cl->squal)) {
 456     return cstring_makeLiteralTemp ("Non-null");
 457   } else {
 458     BADBRANCH;
 459   }
 460
 461   BADBRANCHRET (cstring_undefined);
 462 }
 463
 464 cstring stateClause_preErrorString (stateClause cl, sRef sr)
 465 {
 466   llassert (cl->state == TK_BOTH || cl->state == TK_BEFORE);
 467
 468   switch (cl->kind)
 469     {
 470     case SP_USES:
 471       if (sRef_isDead (sr))
 472         return cstring_makeLiteralTemp ("Dead");
 473       else
 474         return cstring_makeLiteralTemp ("Undefined");
 475     case SP_ALLOCATES: /*@fallthrough@*/
 476     case SP_DEFINES:
 477     case SP_SETS:
 478       return cstring_makeLiteralTemp ("Allocated");
 479     case SP_RELEASES:
 480       if (sRef_isDead (sr))
 481         {
 482           return cstring_makeLiteralTemp ("Dead");
 483         }
 484       else if (sRef_isDependent (sr)
 485                || sRef_isShared (sr))
 486         {
 487           return alkind_unparse (sRef_getAliasKind (sr));
 488         }
 489       else if (sRef_isObserver (sr) || sRef_isExposed (sr))
 490         {
 491           return exkind_unparse (sRef_getExKind (sr));
 492         }
 493       else
 494         {
 495           return cstring_makeLiteralTemp ("Undefined");
 496         }
 497     case SP_GLOBAL:
 498       BADBRANCH;
 499     case SP_QUAL:
 500       return stateClause_qualErrorString (cl, sr);
 501     }
 502
 503   BADEXIT;
 504 }
 505
 506 flagcode stateClause_postErrorCode (stateClause cl)
 507 {
 508   llassert (cl->state == TK_BOTH || cl->state == TK_AFTER);
 509
 510   switch (cl->kind)
 511     {
 512     case SP_USES:
 513       BADBRANCHCONT;
 514       return INVALID_FLAG;
 515     case SP_ALLOCATES:
 516     case SP_DEFINES:
 517     case SP_SETS:
 518       return FLG_COMPDEF;
 519     case SP_RELEASES:
 520       return FLG_MUSTFREEONLY;
 521     case SP_GLOBAL:
 522       BADBRANCH;
 523     case SP_QUAL:
 524       return stateClause_qualErrorCode (cl);
 525     }
 526
 527   BADBRANCHRET (INVALID_FLAG);
 528 }
 529
 530 cstring stateClause_postErrorString (stateClause cl, sRef sr)
 531 {
 532   llassert (cl->state == TK_BOTH || cl->state == TK_AFTER);
 533
 534   switch (cl->kind)
 535     {
 536     case SP_USES:
 537       BADBRANCHCONT;
 538       return cstring_makeLiteralTemp ("<ERROR>");
 539     case SP_ALLOCATES:
 540       return cstring_makeLiteralTemp ("Unallocated");
 541     case SP_DEFINES:
 542     case SP_SETS:
 543       return cstring_makeLiteralTemp ("Undefined");
 544     case SP_RELEASES:
 545       return cstring_makeLiteralTemp ("Unreleased");
 546     case SP_GLOBAL:
 547       BADBRANCH;
 548     case SP_QUAL:
 549       return stateClause_qualErrorString (cl, sr);
 550     }
 551
 552   BADEXIT;
 553 }
 554
 555 cstring stateClause_dump (stateClause s)
 556 {
 557   return (message ("%d.%d.%q.%q",
 558                    (int) s->state,
 559                    (int) s->kind,
 560                    qual_dump (s->squal),
 561                    sRefSet_dump (s->refs)));
 562 }
 563
 564 stateClause stateClause_undump (char **s)
 565 {
 566   stateClause ret = (stateClause) dmalloc (sizeof (*ret));
 567
 568   ret->loc = fileloc_undefined;
 569   ret->state = (stateConstraint) reader_getInt (s);
 570   reader_checkChar (s, '.');
 571   ret->kind = (stateClauseKind) reader_getInt (s);
 572   reader_checkChar (s, '.');
 573   ret->squal = qual_undump (s);
 574   reader_checkChar (s, '.');
 575   ret->refs = sRefSet_undump (s);
 576
 577   return ret;
 578 }
 579
 580 stateClause stateClause_copy (stateClause s)
 581 {
 582   stateClause ret = (stateClause) dmalloc (sizeof (*ret));
 583
 584   ret->state = s->state;
 585   ret->kind = s->kind;
 586   ret->squal = s->squal;
 587   ret->refs = sRefSet_newCopy (s->refs);
 588   ret->loc = fileloc_copy (s->loc);
 589
 590   return ret;
 591 }
 592
 593 bool stateClause_sameKind (stateClause s1, stateClause s2)
 594 {
 595   return (s1->state == s2->state
 596           && s1->kind == s2->kind
 597           && qual_match (s1->squal, s2->squal));
 598 }
 599
 600 void stateClause_free (stateClause s)
 601 {
 602   sRefSet_free (s->refs);
 603   fileloc_free (s->loc);
 604   sfree (s);
 605 }
 606
 607 static /*@observer@*/ cstring
 608   stateClauseKind_unparse (stateClause s)
 609 {
 610   switch (s->kind)
 611     {
 612     case SP_USES:
 613       return cstring_makeLiteralTemp ("uses");
 614     case SP_DEFINES:
 615       return cstring_makeLiteralTemp ("defines");
 616     case SP_ALLOCATES:
 617       return cstring_makeLiteralTemp ("allocates");
 618     case SP_RELEASES:
 619       return cstring_makeLiteralTemp ("releases");
 620     case SP_SETS:
 621       return cstring_makeLiteralTemp ("sets");
 622     case SP_GLOBAL:
 623       return qual_unparse (s->squal);
 624     case SP_QUAL:
 625       return qual_unparse (s->squal);
 626     }
 627
 628   BADEXIT;
 629 }
 630
 631 cstring stateClause_unparseKind (stateClause s)
 632 {
 633   return
 634     (message ("%s%s",
 635               cstring_makeLiteralTemp (s->state == TK_BEFORE
 636                                        ? "requires "
 637                                        : (s->state == TK_AFTER
 638                                           ? "ensures " : "")),
 639               stateClauseKind_unparse (s)));
 640 }
 641
 642 cstring stateClause_unparse (stateClause s)
 643 {
 644   return (message ("%q %q",
 645                    stateClause_unparseKind (s), sRefSet_unparsePlain (s->refs)));
 646 }
 647
 648 stateClause stateClause_createDefines (sRefSet s)
 649 {
 650   return (stateClause_createRaw (TK_BOTH, SP_DEFINES, s));
 651 }
 652
 653 stateClause stateClause_createUses (sRefSet s)
 654 {
 655   return (stateClause_createRaw (TK_BOTH, SP_USES, s));
 656 }
 657
 658 stateClause stateClause_createSets (sRefSet s)
 659 {
 660   return (stateClause_createRaw (TK_BOTH, SP_SETS, s));
 661 }
 662
 663 stateClause stateClause_createReleases (sRefSet s)
 664 {
 665   return (stateClause_createRaw (TK_BOTH, SP_RELEASES, s));
 666 }
 667
 668 stateClause stateClause_createPlain (lltok tok, sRefSet s)
 669 {
 670   switch (lltok_getTok (tok))
 671     {
 672     case QUSES:
 673       return stateClause_createUses (s);
 674     case QDEFINES:
 675       return stateClause_createDefines (s);
 676     case QALLOCATES:
 677       return stateClause_createAllocates (s);
 678     case QSETS:
 679       return stateClause_createSets (s);
 680     case QRELEASES:
 681       return stateClause_createReleases (s);
 682     default:
 683       sRefSet_free (s);
 684       BADBRANCH;
 685     }
 686
 687   BADBRANCHRET (stateClause_createUses (sRefSet_undefined));
 688 }
 689
 690 stateClause stateClause_createAllocates (sRefSet s)
 691 {
 692   return (stateClause_createRaw (TK_BOTH, SP_ALLOCATES, s));
 693 }
 694
 695 bool stateClause_matchKind (stateClause s1, stateClause s2)
 696 {
 697   return (s1->state == s2->state && s1->kind == s2->kind
 698           && qual_match (s1->squal, s2->squal));
 699 }
 700
 701 bool stateClause_hasEnsures (stateClause cl)
 702 {
 703   return (cl->state == TK_AFTER && (cl->kind == SP_QUAL || cl->kind == SP_GLOBAL));
 704 }
 705
 706 bool stateClause_hasRequires (stateClause cl)
 707 {
 708   return (cl->state == TK_BEFORE && (cl->kind == SP_QUAL || cl->kind == SP_GLOBAL));
 709 }
 710
 711 bool stateClause_setsMetaState (stateClause cl)
 712 {
 713   return ((cl->kind == SP_QUAL || cl->kind == SP_GLOBAL)
 714           && qual_isMetaState (cl->squal));
 715 }
 716
 717 qual stateClause_getMetaQual (stateClause cl)
 718 {
 719   llassert (cl->kind == SP_QUAL || cl->kind == SP_GLOBAL);
 720   return cl->squal;
 721 }
 722
 723 static sRefModVal stateClause_getStateFunction (stateClause cl)
 724 {
 725   qual sq;
 726
 727   llassert (cl->kind == SP_QUAL || cl->kind == SP_GLOBAL);
 728
 729   sq = cl->squal;
 730
 731   /*@+enumint@*/
 732
 733   if (qual_isNullStateQual (sq))
 734     {
 735       return (sRefModVal) sRef_setNullState;
 736     }
 737   else if (qual_isExQual (sq))
 738     {
 739       return (sRefModVal) sRef_setExKind;
 740     }
 741   else if (qual_isAliasQual (sq))
 742     {
 743       return (sRefModVal) sRef_setAliasKind; /*@i23 complete? @*/
 744     }
 745   else
 746     {
 747       DPRINTF (("Unhandled ensures qual: %s", qual_unparse (sq)));
 748       BADBRANCH;
 749     }
 750   /*@=enumint@*/
 751   BADBRANCHRET (NULL);
 752 }
 753
 754 int stateClause_getStateParameter (stateClause cl)
 755 {
 756   qual sq;
 757
 758   llassert (cl->kind == SP_QUAL || cl->kind == SP_GLOBAL);
 759
 760   sq = cl->squal;
 761
 762   /*@+relaxtypes@*/ /*@i523 this is wrong, remove the enumint@*/
 763   /*@+enumint@*/
 764
 765   if (qual_isNotNull (sq))
 766     {
 767       return NS_MNOTNULL;
 768     }
 769   else if (qual_isIsNull (sq))
 770     {
 771       return NS_DEFNULL;
 772     }
 773   else if (qual_isNull (sq))
 774     {
 775       return NS_POSNULL;
 776     }
 777   else if (qual_isRelNull (sq))
 778     {
 779       return NS_RELNULL;
 780     }
 781   else if (qual_isExposed (sq))
 782     {
 783       return XO_EXPOSED;
 784     }
 785   else if (qual_isObserver (sq))
 786     {
 787       return XO_OBSERVER;
 788     }
 789   else if (qual_isAliasQual (sq))
 790     {
 791       if (qual_isOnly (sq)) return AK_ONLY;
 792       if (qual_isImpOnly (sq)) return AK_IMPONLY;
 793       if (qual_isTemp (sq)) return AK_TEMP;
 794       if (qual_isOwned (sq)) return AK_OWNED;
 795       if (qual_isShared (sq)) return AK_SHARED;
 796       if (qual_isUnique (sq)) return AK_UNIQUE;
 797       if (qual_isDependent (sq)) return AK_DEPENDENT;
 798       if (qual_isKeep (sq)) return AK_KEEP;
 799       if (qual_isKept (sq)) return AK_KEPT;
 800       BADBRANCH;
 801     }
 802   else
 803     {
 804       DPRINTF (("Unhandled ensures qual: %s", qual_unparse (sq)));
 805       BADBRANCH;
 806     }
 807
 808   /*@=enumint@*/
 809   /*@=relaxtypes@*/
 810   BADBRANCHRET (0);
 811 }
 812
 813 sRefModVal stateClause_getEnsuresFunction (stateClause cl)
 814 {
 815   llassertprint (cl->state == TK_AFTER, ("Not after: %s", stateClause_unparse (cl)));
 816   llassert (cl->kind == SP_QUAL || cl->kind == SP_GLOBAL);
 817   return stateClause_getStateFunction (cl);
 818 }
 819
 820 sRefModVal stateClause_getRequiresBodyFunction (stateClause cl)
 821 {
 822   llassertprint (cl->state == TK_BEFORE, ("Not before: %s", stateClause_unparse (cl)));
 823   llassert (cl->kind == SP_QUAL || cl->kind == SP_GLOBAL);
 824   return stateClause_getStateFunction (cl);
 825 }
 826
 827 /*@observer@*/ fileloc stateClause_loc (stateClause s)
 828 {
 829   return s->loc;
 830 }
 831