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   BADBRANCH;
 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   BADBRANCH;
 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   BADBRANCH;
 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
 397 flagcode stateClause_preErrorCode (stateClause cl)
 398 {
 399   llassert (cl->state == TK_BOTH || cl->state == TK_BEFORE);
 400
 401   switch (cl->kind)
 402     {
 403     case SP_USES:
 404       return FLG_USEDEF;
 405     case SP_ALLOCATES: /*@fallthrough@*/
 406     case SP_DEFINES:
 407     case SP_SETS:
 408       return FLG_MUSTFREE;
 409     case SP_RELEASES:
 410       return FLG_USEDEF;
 411     case SP_GLOBAL:
 412     case SP_QUAL:
 413       return stateClause_qualErrorCode (cl);
 414     }
 415
 416   BADBRANCH;
 417 }
 418
 419 static /*@observer@*/ cstring stateClause_qualErrorString (stateClause cl, sRef sr)
 420 {
 421   if (qual_isMemoryAllocation (cl->squal)) {
 422     return alkind_capName (sRef_getAliasKind (sr));
 423   } else if (qual_isObserver (cl->squal)) {
 424     return cstring_makeLiteralTemp ("Non-observer");
 425   } else if (qual_isExposed (cl->squal)) {
 426     if (sRef_isObserver (sr))
 427       {
 428         return cstring_makeLiteralTemp ("Observer");
 429       }
 430     else
 431       {
 432         return cstring_makeLiteralTemp ("Non-exposed");
 433       }
 434   } else if (qual_isNotNull (cl->squal)) {
 435     if (sRef_isDefinitelyNull (sr))
 436       {
 437         return cstring_makeLiteralTemp ("Null");
 438       }
 439     else
 440       {
 441         return cstring_makeLiteralTemp ("Possibly null");
 442       }
 443   } else if (qual_isIsNull (cl->squal)) {
 444     return cstring_makeLiteralTemp ("Non-null");
 445   } else {
 446     BADBRANCH;
 447   }
 448
 449   BADBRANCH;
 450 }
 451
 452 cstring stateClause_preErrorString (stateClause cl, sRef sr)
 453 {
 454   llassert (cl->state == TK_BOTH || cl->state == TK_BEFORE);
 455
 456   switch (cl->kind)
 457     {
 458     case SP_USES:
 459       if (sRef_isDead (sr))
 460         return cstring_makeLiteralTemp ("Dead");
 461       else
 462         return cstring_makeLiteralTemp ("Undefined");
 463     case SP_ALLOCATES: /*@fallthrough@*/
 464     case SP_DEFINES:
 465     case SP_SETS:
 466       return cstring_makeLiteralTemp ("Allocated");
 467     case SP_RELEASES:
 468       if (sRef_isDead (sr))
 469         {
 470           return cstring_makeLiteralTemp ("Dead");
 471         }
 472       else if (sRef_isDependent (sr)
 473                || sRef_isShared (sr))
 474         {
 475           return alkind_unparse (sRef_getAliasKind (sr));
 476         }
 477       else if (sRef_isObserver (sr) || sRef_isExposed (sr))
 478         {
 479           return exkind_unparse (sRef_getExKind (sr));
 480         }
 481       else
 482         {
 483           return cstring_makeLiteralTemp ("Undefined");
 484         }
 485     case SP_GLOBAL:
 486       BADBRANCH;
 487     case SP_QUAL:
 488       return stateClause_qualErrorString (cl, sr);
 489     }
 490
 491   BADEXIT;
 492 }
 493
 494 flagcode stateClause_postErrorCode (stateClause cl)
 495 {
 496   llassert (cl->state == TK_BOTH || cl->state == TK_AFTER);
 497
 498   switch (cl->kind)
 499     {
 500     case SP_USES:
 501       BADBRANCHCONT;
 502       return INVALID_FLAG;
 503     case SP_ALLOCATES:
 504     case SP_DEFINES:
 505     case SP_SETS:
 506       return FLG_COMPDEF;
 507     case SP_RELEASES:
 508       return FLG_MUSTFREE;
 509     case SP_GLOBAL:
 510       BADBRANCH;
 511     case SP_QUAL:
 512       return stateClause_qualErrorCode (cl);
 513     }
 514
 515   BADBRANCH;
 516 }
 517
 518 cstring stateClause_postErrorString (stateClause cl, sRef sr)
 519 {
 520   llassert (cl->state == TK_BOTH || cl->state == TK_AFTER);
 521
 522   switch (cl->kind)
 523     {
 524     case SP_USES:
 525       BADBRANCHCONT;
 526       return cstring_makeLiteralTemp ("<ERROR>");
 527     case SP_ALLOCATES:
 528       return cstring_makeLiteralTemp ("Unallocated");
 529     case SP_DEFINES:
 530     case SP_SETS:
 531       return cstring_makeLiteralTemp ("Undefined");
 532     case SP_RELEASES:
 533       return cstring_makeLiteralTemp ("Unreleased");
 534     case SP_GLOBAL:
 535       BADBRANCH;
 536     case SP_QUAL:
 537       return stateClause_qualErrorString (cl, sr);
 538     }
 539
 540   BADEXIT;
 541 }
 542
 543 cstring stateClause_dump (stateClause s)
 544 {
 545   return (message ("%d.%d.%q.%q",
 546                    (int) s->state,
 547                    (int) s->kind,
 548                    qual_dump (s->squal),
 549                    sRefSet_dump (s->refs)));
 550 }
 551
 552 stateClause stateClause_undump (char **s)
 553 {
 554   stateClause ret = (stateClause) dmalloc (sizeof (*ret));
 555
 556   ret->loc = fileloc_undefined;
 557   ret->state = (stateConstraint) reader_getInt (s);
 558   reader_checkChar (s, '.');
 559   ret->kind = (stateClauseKind) reader_getInt (s);
 560   reader_checkChar (s, '.');
 561   ret->squal = qual_undump (s);
 562   reader_checkChar (s, '.');
 563   ret->refs = sRefSet_undump (s);
 564
 565   return ret;
 566 }
 567
 568 stateClause stateClause_copy (stateClause s)
 569 {
 570   stateClause ret = (stateClause) dmalloc (sizeof (*ret));
 571
 572   ret->state = s->state;
 573   ret->kind = s->kind;
 574   ret->squal = s->squal;
 575   ret->refs = sRefSet_newCopy (s->refs);
 576   ret->loc = fileloc_copy (s->loc);
 577
 578   return ret;
 579 }
 580
 581 bool stateClause_sameKind (stateClause s1, stateClause s2)
 582 {
 583   return (s1->state == s2->state
 584           && s1->kind == s2->kind
 585           && qual_match (s1->squal, s2->squal));
 586 }
 587
 588 void stateClause_free (stateClause s)
 589 {
 590   sRefSet_free (s->refs);
 591   fileloc_free (s->loc);
 592   sfree (s);
 593 }
 594
 595 static /*@observer@*/ cstring
 596   stateClauseKind_unparse (stateClause s)
 597 {
 598   switch (s->kind)
 599     {
 600     case SP_USES:
 601       return cstring_makeLiteralTemp ("uses");
 602     case SP_DEFINES:
 603       return cstring_makeLiteralTemp ("defines");
 604     case SP_ALLOCATES:
 605       return cstring_makeLiteralTemp ("allocates");
 606     case SP_RELEASES:
 607       return cstring_makeLiteralTemp ("releases");
 608     case SP_SETS:
 609       return cstring_makeLiteralTemp ("sets");
 610     case SP_GLOBAL:
 611       return qual_unparse (s->squal);
 612     case SP_QUAL:
 613       return qual_unparse (s->squal);
 614     }
 615
 616   BADEXIT;
 617 }
 618
 619 cstring stateClause_unparseKind (stateClause s)
 620 {
 621   return
 622     (message ("%s%s",
 623               cstring_makeLiteralTemp (s->state == TK_BEFORE
 624                                        ? "requires "
 625                                        : (s->state == TK_AFTER
 626                                           ? "ensures " : "")),
 627               stateClauseKind_unparse (s)));
 628 }
 629
 630 cstring stateClause_unparse (stateClause s)
 631 {
 632   return (message ("%q %q",
 633                    stateClause_unparseKind (s), sRefSet_unparsePlain (s->refs)));
 634 }
 635
 636 stateClause stateClause_createDefines (sRefSet s)
 637 {
 638   return (stateClause_createRaw (TK_BOTH, SP_DEFINES, s));
 639 }
 640
 641 stateClause stateClause_createUses (sRefSet s)
 642 {
 643   return (stateClause_createRaw (TK_BOTH, SP_USES, s));
 644 }
 645
 646 stateClause stateClause_createSets (sRefSet s)
 647 {
 648   return (stateClause_createRaw (TK_BOTH, SP_SETS, s));
 649 }
 650
 651 stateClause stateClause_createReleases (sRefSet s)
 652 {
 653   return (stateClause_createRaw (TK_BOTH, SP_RELEASES, s));
 654 }
 655
 656 stateClause stateClause_createPlain (lltok tok, sRefSet s)
 657 {
 658   switch (lltok_getTok (tok))
 659     {
 660     case QUSES:
 661       return stateClause_createUses (s);
 662     case QDEFINES:
 663       return stateClause_createDefines (s);
 664     case QALLOCATES:
 665       return stateClause_createAllocates (s);
 666     case QSETS:
 667       return stateClause_createSets (s);
 668     case QRELEASES:
 669       return stateClause_createReleases (s);
 670     default:
 671       sRefSet_free (s);
 672       BADBRANCH;
 673     }
 674 }
 675
 676 stateClause stateClause_createAllocates (sRefSet s)
 677 {
 678   return (stateClause_createRaw (TK_BOTH, SP_ALLOCATES, s));
 679 }
 680
 681 bool stateClause_matchKind (stateClause s1, stateClause s2)
 682 {
 683   return (s1->state == s2->state && s1->kind == s2->kind
 684           && qual_match (s1->squal, s2->squal));
 685 }
 686
 687 bool stateClause_hasEnsures (stateClause cl)
 688 {
 689   return (cl->state == TK_AFTER && (cl->kind == SP_QUAL || cl->kind == SP_GLOBAL));
 690 }
 691
 692 bool stateClause_hasRequires (stateClause cl)
 693 {
 694   return (cl->state == TK_BEFORE && (cl->kind == SP_QUAL || cl->kind == SP_GLOBAL));
 695 }
 696
 697 bool stateClause_setsMetaState (stateClause cl)
 698 {
 699   return ((cl->kind == SP_QUAL || cl->kind == SP_GLOBAL)
 700           && qual_isMetaState (cl->squal));
 701 }
 702
 703 qual stateClause_getMetaQual (stateClause cl)
 704 {
 705   llassert (cl->kind == SP_QUAL || cl->kind == SP_GLOBAL);
 706   return cl->squal;
 707 }
 708
 709 static sRefModVal stateClause_getStateFunction (stateClause cl)
 710 {
 711   qual sq;
 712
 713   llassert (cl->kind == SP_QUAL || cl->kind == SP_GLOBAL);
 714
 715   sq = cl->squal;
 716
 717   /*@+enumint@*/
 718
 719   if (qual_isNullStateQual (sq))
 720     {
 721       return (sRefModVal) sRef_setNullState;
 722     }
 723   else if (qual_isExQual (sq))
 724     {
 725       return (sRefModVal) sRef_setExKind;
 726     }
 727   else if (qual_isAliasQual (sq))
 728     {
 729       return (sRefModVal) sRef_setAliasKind; /*@i23 complete? @*/
 730     }
 731   else
 732     {
 733       DPRINTF (("Unhandled ensures qual: %s", qual_unparse (sq)));
 734       BADBRANCH;
 735     }
 736   /*@=enumint@*/
 737 }
 738
 739 int stateClause_getStateParameter (stateClause cl)
 740 {
 741   qual sq;
 742
 743   llassert (cl->kind == SP_QUAL || cl->kind == SP_GLOBAL);
 744
 745   sq = cl->squal;
 746
 747   /*@+relaxtypes@*/ /*@i523 this is wrong, remove the enumint@*/
 748   /*@+enumint@*/
 749
 750   if (qual_isNotNull (sq))
 751     {
 752       return NS_MNOTNULL;
 753     }
 754   else if (qual_isIsNull (sq))
 755     {
 756       return NS_DEFNULL;
 757     }
 758   else if (qual_isNull (sq))
 759     {
 760       return NS_POSNULL;
 761     }
 762   else if (qual_isRelNull (sq))
 763     {
 764       return NS_RELNULL;
 765     }
 766   else if (qual_isExposed (sq))
 767     {
 768       return XO_EXPOSED;
 769     }
 770   else if (qual_isObserver (sq))
 771     {
 772       return XO_OBSERVER;
 773     }
 774   else if (qual_isAliasQual (sq))
 775     {
 776       if (qual_isOnly (sq)) return AK_ONLY;
 777       if (qual_isImpOnly (sq)) return AK_IMPONLY;
 778       if (qual_isTemp (sq)) return AK_TEMP;
 779       if (qual_isOwned (sq)) return AK_OWNED;
 780       if (qual_isShared (sq)) return AK_SHARED;
 781       if (qual_isUnique (sq)) return AK_UNIQUE;
 782       if (qual_isDependent (sq)) return AK_DEPENDENT;
 783       if (qual_isKeep (sq)) return AK_KEEP;
 784       if (qual_isKept (sq)) return AK_KEPT;
 785       BADBRANCH;
 786     }
 787   else
 788     {
 789       DPRINTF (("Unhandled ensures qual: %s", qual_unparse (sq)));
 790       BADBRANCH;
 791     }
 792
 793   /*@=enumint@*/
 794   /*@=relaxtypes@*/
 795 }
 796
 797 sRefModVal stateClause_getEnsuresFunction (stateClause cl)
 798 {
 799   llassertprint (cl->state == TK_AFTER, ("Not after: %s", stateClause_unparse (cl)));
 800   llassert (cl->kind == SP_QUAL || cl->kind == SP_GLOBAL);
 801   return stateClause_getStateFunction (cl);
 802 }
 803
 804 sRefModVal stateClause_getRequiresBodyFunction (stateClause cl)
 805 {
 806   llassertprint (cl->state == TK_BEFORE, ("Not before: %s", stateClause_unparse (cl)));
 807   llassert (cl->kind == SP_QUAL || cl->kind == SP_GLOBAL);
 808   return stateClause_getStateFunction (cl);
 809 }
 810
 811 /*@observer@*/ fileloc stateClause_loc (stateClause s)
 812 {
 813   return s->loc;
 814 }
 815