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