src/stateClause.c

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