src/stateClause.c

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