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