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