src/specialClauses.c

   1 /*
   2 ** Splint - annotation-assisted static program checker
   3 ** Copyright (C) 1994-2000 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://www.splint.org
  23 */
  24 /*
  25 ** specialClauses.c
  26 */
  27
  28 # include "lclintMacros.nf"
  29 # include "basic.h"
  30
  31 static bool specialClause_isMemoryAllocation (specialClause p_cl) /*@*/ ;
  32 static void specialClause_free (/*@only@*/ specialClause p_s) ;
  33 static cstring specialClause_dump (specialClause p_s) /*@*/ ;
  34 static specialClause specialClause_undump (char **p_s) /*@modifies *p_s@*/ ;
  35 static specialClause specialClause_copy (specialClause p_s) /*@*/ ;
  36 static bool specialClause_sameKind (specialClause p_s1, specialClause p_s2) /*@*/ ;
  37
  38 specialClause
  39   specialClause_create (stateConstraint st, specialClauseKind k, sRefSet s)
  40 {
  41   specialClause ret = (specialClause) dmalloc (sizeof (*ret));
  42
  43   ret->state = st;
  44   ret->kind = k;
  45   ret->refs = s;
  46
  47   return ret;
  48 }
  49
  50 bool specialClause_isBefore (specialClause cl)
  51 {
  52   return (cl->state == TK_BEFORE || cl->state == TK_BOTH);
  53 }
  54
  55 bool specialClause_isAfter (specialClause cl)
  56 {
  57   return (cl->state == TK_AFTER || cl->state == TK_BOTH);
  58 }
  59
  60 bool specialClause_isMemoryAllocation (specialClause cl)
  61 {
  62   switch (cl->kind)
  63     {
  64     case SP_ALLOCATES:
  65     case SP_RELEASES:
  66     case SP_ISONLY:
  67     case SP_ISSHARED:
  68     case SP_ISDEPENDENT:
  69     case SP_ISOWNED:
  70     case SP_ISOBSERVER:
  71     case SP_ISEXPOSED:
  72       return TRUE;
  73     case SP_USES:
  74     case SP_DEFINES:
  75     case SP_SETS:
  76     case SP_ISNULL:
  77     case SP_ISNOTNULL:
  78       return FALSE;
  79   }
  80
  81   BADEXIT;
  82 }
  83
  84 /*
  85 ** An error is reported if the test is NOT true.
  86 */
  87
  88 sRefTest specialClause_getPreTestFunction (specialClause cl)
  89 {
  90   switch (cl->kind)
  91     {
  92     case SP_USES:
  93       return sRef_isStrictReadable;
  94     case SP_ALLOCATES:
  95       return sRef_hasNoStorage;
  96     case SP_DEFINES:
  97       return sRef_hasNoStorage;
  98     case SP_SETS:
  99       return sRef_isNotUndefined;
 100     case SP_RELEASES:
 101       return sRef_isNotUndefined;
 102     case SP_ISONLY:
 103       return sRef_isOnly;
 104     case SP_ISSHARED:
 105       return sRef_isShared;
 106     case SP_ISDEPENDENT:
 107       return sRef_isDependent;
 108     case SP_ISOWNED:
 109       return sRef_isOwned;
 110     case SP_ISOBSERVER:
 111       return sRef_isObserver;
 112     case SP_ISEXPOSED:
 113       return sRef_isExposed;
 114     case SP_ISNOTNULL:
 115       return sRef_isNotNull;
 116     case SP_ISNULL:
 117       return sRef_isDefinitelyNull;
 118   }
 119
 120   BADEXIT;
 121 }
 122
 123 sRefTest specialClause_getPostTestFunction (specialClause cl)
 124 {
 125   llassert (specialClause_isAfter (cl));
 126
 127   switch (cl->kind)
 128     {
 129     case SP_USES:
 130       return NULL;
 131     case SP_ALLOCATES:
 132       return sRef_isAllocated;
 133     case SP_DEFINES:
 134       return sRef_isReallyDefined;
 135     case SP_SETS:
 136       return sRef_isReallyDefined;
 137     case SP_RELEASES:
 138       return sRef_isDeadStorage;
 139     case SP_ISONLY:
 140       return sRef_isOnly;
 141     case SP_ISSHARED:
 142       return sRef_isShared;
 143     case SP_ISDEPENDENT:
 144       return sRef_isDependent;
 145     case SP_ISOWNED:
 146       return sRef_isOwned;
 147     case SP_ISOBSERVER:
 148       return sRef_isObserver;
 149     case SP_ISEXPOSED:
 150       return sRef_isExposed;
 151     case SP_ISNOTNULL:
 152       return sRef_isNotNull;
 153     case SP_ISNULL:
 154       return sRef_isDefinitelyNull;
 155   }
 156
 157   BADEXIT;
 158 }
 159
 160 sRefShower specialClause_getPostTestShower (specialClause cl)
 161 {
 162   switch (cl->kind)
 163     {
 164     case SP_USES:
 165     case SP_ALLOCATES:
 166       return NULL;
 167     case SP_DEFINES:
 168     case SP_SETS:
 169       return sRef_showNotReallyDefined;
 170     case SP_RELEASES:
 171       return NULL;
 172     case SP_ISONLY:
 173     case SP_ISSHARED:
 174     case SP_ISDEPENDENT:
 175     case SP_ISOWNED:
 176       return sRef_showAliasInfo;
 177     case SP_ISOBSERVER:
 178     case SP_ISEXPOSED:
 179       return sRef_showExpInfo;
 180     case SP_ISNOTNULL:
 181     case SP_ISNULL:
 182       return sRef_showNullInfo;
 183   }
 184
 185   BADEXIT;
 186 }
 187
 188 sRefMod specialClause_getEntryFunction (specialClause cl)
 189 {
 190   if (cl->state == TK_BEFORE || cl->state == TK_BOTH)
 191     {
 192       switch (cl->kind)
 193         {
 194         case SP_USES:
 195           return sRef_setDefinedComplete;
 196         case SP_ALLOCATES:
 197           return NULL;
 198         case SP_DEFINES:
 199           return NULL;
 200         case SP_SETS:
 201           return sRef_setAllocatedComplete;
 202         case SP_RELEASES:
 203           return sRef_setDefinedComplete;
 204         case SP_ISONLY:
 205           return sRef_setOnly;
 206         case SP_ISSHARED:
 207           return sRef_setShared;
 208         case SP_ISDEPENDENT:
 209           return sRef_setDependent;
 210         case SP_ISOWNED:
 211           return sRef_setOwned;
 212         case SP_ISOBSERVER:
 213           return sRef_setObserver;
 214         case SP_ISEXPOSED:
 215           return sRef_setExposed;
 216         case SP_ISNOTNULL:
 217           return sRef_setNotNull;
 218         case SP_ISNULL:
 219           return sRef_setDefNull;
 220         }
 221
 222       BADBRANCH;
 223     }
 224   else
 225     {
 226       return NULL;
 227     }
 228 }
 229
 230 sRefMod specialClause_getEffectFunction (specialClause cl)
 231 {
 232   if (cl->state == TK_AFTER || cl->state == TK_BOTH)
 233     {
 234       switch (cl->kind)
 235         {
 236         case SP_USES:
 237           return NULL;
 238         case SP_ALLOCATES:
 239           return sRef_setAllocatedComplete;
 240         case SP_DEFINES:
 241           return sRef_setDefinedNCComplete;
 242         case SP_SETS:
 243           return sRef_setDefinedNCComplete;
 244         case SP_RELEASES:
 245           return sRef_killComplete;
 246         case SP_ISONLY:
 247           return sRef_setOnly;
 248         case SP_ISSHARED:
 249           return sRef_setShared;
 250         case SP_ISDEPENDENT:
 251           return sRef_setDependent;
 252         case SP_ISOWNED:
 253           return sRef_setOwned;
 254         case SP_ISOBSERVER:
 255           return sRef_setObserver;
 256         case SP_ISEXPOSED:
 257           return sRef_setExposed;
 258         case SP_ISNOTNULL:
 259           return sRef_setNotNull;
 260         case SP_ISNULL:
 261           return sRef_setDefNull;
 262         }
 263
 264       BADBRANCH;
 265     }
 266   else
 267     {
 268       return NULL;
 269     }
 270 }
 271
 272 sRefMod specialClause_getReturnEffectFunction (specialClause cl)
 273 {
 274   if (cl->state == TK_AFTER || cl->state == TK_BOTH)
 275     {
 276       switch (cl->kind)
 277         {
 278         case SP_USES:
 279         case SP_ALLOCATES:
 280         case SP_DEFINES:
 281         case SP_SETS:
 282         case SP_RELEASES:
 283           return NULL;
 284         case SP_ISONLY:
 285           return sRef_killComplete;
 286         case SP_ISSHARED:
 287         case SP_ISDEPENDENT:
 288         case SP_ISOWNED:
 289         case SP_ISOBSERVER:
 290         case SP_ISEXPOSED:
 291         case SP_ISNULL:
 292         case SP_ISNOTNULL:
 293           return NULL;
 294         }
 295
 296       BADBRANCH;
 297     }
 298   else
 299     {
 300       return NULL;
 301     }
 302 }
 303
 304 flagcode specialClause_preErrorCode (specialClause cl)
 305 {
 306   llassert (cl->state == TK_BOTH || cl->state == TK_BEFORE);
 307
 308   switch (cl->kind)
 309     {
 310     case SP_USES:
 311       return FLG_USEDEF;
 312     case SP_ALLOCATES: /*@fallthrough@*/
 313     case SP_DEFINES:
 314     case SP_SETS:
 315       return FLG_MUSTFREE;
 316     case SP_RELEASES:
 317       return FLG_USEDEF;
 318     case SP_ISONLY:
 319       return FLG_ONLYTRANS;
 320     case SP_ISSHARED:
 321       return FLG_SHAREDTRANS;
 322     case SP_ISDEPENDENT:
 323       return FLG_DEPENDENTTRANS;
 324     case SP_ISOWNED:
 325       return FLG_OWNEDTRANS;
 326     case SP_ISOBSERVER:
 327       return FLG_OBSERVERTRANS;
 328     case SP_ISEXPOSED:
 329       return FLG_EXPOSETRANS;
 330     case SP_ISNULL:
 331     case SP_ISNOTNULL:
 332       return FLG_NULLSTATE;
 333   }
 334
 335   BADBRANCH;
 336 }
 337
 338 cstring specialClause_preErrorString (specialClause cl, sRef sr)
 339 {
 340   llassert (cl->state == TK_BOTH || cl->state == TK_BEFORE);
 341
 342   switch (cl->kind)
 343     {
 344     case SP_USES:
 345       if (sRef_isDead (sr))
 346         return cstring_makeLiteralTemp ("Dead");
 347       else
 348         return cstring_makeLiteralTemp ("Undefined");
 349     case SP_ALLOCATES: /*@fallthrough@*/
 350     case SP_DEFINES:
 351     case SP_SETS:
 352       return cstring_makeLiteralTemp ("Allocated");
 353     case SP_RELEASES:
 354       if (sRef_isDead (sr))
 355         {
 356           return cstring_makeLiteralTemp ("Dead");
 357         }
 358       else if (sRef_isDependent (sr)
 359                || sRef_isShared (sr))
 360         {
 361           return alkind_unparse (sRef_getAliasKind (sr));
 362         }
 363       else if (sRef_isObserver (sr) || sRef_isExposed (sr))
 364         {
 365           return exkind_unparse (sRef_getExKind (sr));
 366         }
 367       else
 368         {
 369           return cstring_makeLiteralTemp ("Undefined");
 370         }
 371     case SP_ISONLY:
 372     case SP_ISSHARED:
 373     case SP_ISDEPENDENT:
 374     case SP_ISOWNED:
 375       return alkind_capName (sRef_getAliasKind (sr));
 376     case SP_ISOBSERVER:
 377       return cstring_makeLiteralTemp ("Non-observer");
 378     case SP_ISEXPOSED:
 379       if (sRef_isObserver (sr))
 380         {
 381           return cstring_makeLiteralTemp ("Observer");
 382         }
 383       else
 384         {
 385           return cstring_makeLiteralTemp ("Non-exposed");
 386         }
 387     case SP_ISNOTNULL:
 388       if (sRef_isDefinitelyNull (sr))
 389         {
 390           return cstring_makeLiteralTemp ("Null");
 391         }
 392       else
 393         {
 394           return cstring_makeLiteralTemp ("Possibly null");
 395         }
 396     case SP_ISNULL:
 397       return cstring_makeLiteralTemp ("Non-null");
 398   }
 399
 400   BADEXIT;
 401 }
 402
 403 flagcode specialClause_postErrorCode (specialClause cl)
 404 {
 405   llassert (cl->state == TK_BOTH || cl->state == TK_AFTER);
 406
 407   switch (cl->kind)
 408     {
 409     case SP_USES:
 410       BADBRANCHCONT;
 411       return INVALID_FLAG;
 412     case SP_ALLOCATES:
 413     case SP_DEFINES:
 414     case SP_SETS:
 415       return FLG_COMPDEF;
 416     case SP_RELEASES:
 417       return FLG_MUSTFREE;
 418     case SP_ISONLY:
 419       return FLG_ONLYTRANS;
 420     case SP_ISSHARED:
 421       return FLG_SHAREDTRANS;
 422     case SP_ISDEPENDENT:
 423       return FLG_DEPENDENTTRANS;
 424     case SP_ISOWNED:
 425       return FLG_OWNEDTRANS;
 426     case SP_ISOBSERVER:
 427       return FLG_OBSERVERTRANS;
 428     case SP_ISEXPOSED:
 429       return FLG_EXPOSETRANS;
 430     case SP_ISNULL:
 431     case SP_ISNOTNULL:
 432       return FLG_NULLSTATE;
 433   }
 434
 435   BADBRANCH;
 436 }
 437
 438 cstring specialClause_postErrorString (specialClause cl, sRef sr)
 439 {
 440   llassert (cl->state == TK_BOTH || cl->state == TK_AFTER);
 441
 442   switch (cl->kind)
 443     {
 444     case SP_USES:
 445       BADBRANCHCONT;
 446       return cstring_makeLiteralTemp ("<ERROR>");
 447     case SP_ALLOCATES:
 448       return cstring_makeLiteralTemp ("Unallocated");
 449     case SP_DEFINES:
 450     case SP_SETS:
 451       return cstring_makeLiteralTemp ("Undefined");
 452     case SP_RELEASES:
 453       return cstring_makeLiteralTemp ("Unreleased");
 454     case SP_ISONLY:
 455     case SP_ISSHARED:
 456     case SP_ISOWNED:
 457     case SP_ISDEPENDENT:
 458       return alkind_capName (sRef_getAliasKind (sr));
 459     case SP_ISOBSERVER:
 460       return cstring_makeLiteralTemp ("Non-observer");
 461     case SP_ISEXPOSED:
 462       if (sRef_isObserver (sr))
 463         {
 464           return cstring_makeLiteralTemp ("Observer");
 465         }
 466       else
 467         {
 468           return cstring_makeLiteralTemp ("Non-exposed");
 469         }
 470     case SP_ISNULL:
 471       return cstring_makeLiteralTemp ("Non-null");
 472     case SP_ISNOTNULL:
 473       if (sRef_isDefinitelyNull (sr))
 474         {
 475           return cstring_makeLiteralTemp ("Null");
 476         }
 477       else
 478         {
 479           return cstring_makeLiteralTemp ("Possibly null");
 480         }
 481   }
 482
 483   BADEXIT;
 484 }
 485
 486 cstring specialClause_dump (specialClause s)
 487 {
 488   return (message ("%d.%d.%q",
 489                    (int) s->state,
 490                    (int) s->kind,
 491                    sRefSet_dump (s->refs)));
 492 }
 493
 494 specialClause specialClause_undump (char **s)
 495 {
 496   specialClause ret = (specialClause) dmalloc (sizeof (*ret));
 497
 498   ret->state = (stateConstraint) reader_getInt (s);
 499   reader_checkChar (s, '.');
 500   ret->kind = (specialClauseKind) reader_getInt (s);
 501   reader_checkChar (s, '.');
 502   ret->refs = sRefSet_undump (s);
 503
 504   return ret;
 505 }
 506
 507 specialClause specialClause_copy (specialClause s)
 508 {
 509   specialClause ret = (specialClause) dmalloc (sizeof (*ret));
 510
 511   ret->state = s->state;
 512   ret->kind = s->kind;
 513   ret->refs = sRefSet_newCopy (s->refs);
 514
 515   return ret;
 516 }
 517
 518 bool specialClause_sameKind (specialClause s1, specialClause s2)
 519 {
 520   return (s1->state == s2->state && s1->kind == s2->kind);
 521 }
 522
 523 void specialClause_free (specialClause s)
 524 {
 525   sRefSet_free (s->refs);
 526   sfree (s);
 527 }
 528
 529 static /*@observer@*/ cstring
 530   specialClauseKind_unparse (specialClauseKind k)
 531 {
 532   switch (k)
 533     {
 534     case SP_USES:
 535       return cstring_makeLiteralTemp ("uses");
 536     case SP_DEFINES:
 537       return cstring_makeLiteralTemp ("defines");
 538     case SP_ALLOCATES:
 539       return cstring_makeLiteralTemp ("allocates");
 540     case SP_RELEASES:
 541       return cstring_makeLiteralTemp ("releases");
 542     case SP_SETS:
 543       return cstring_makeLiteralTemp ("sets");
 544     case SP_ISNULL:
 545       return cstring_makeLiteralTemp ("isnull");
 546     case SP_ISNOTNULL:
 547       return cstring_makeLiteralTemp ("notnull");
 548     case SP_ISONLY:
 549       return cstring_makeLiteralTemp ("only");
 550     case SP_ISSHARED:
 551       return cstring_makeLiteralTemp ("shared");
 552     case SP_ISDEPENDENT:
 553       return cstring_makeLiteralTemp ("dependent");
 554     case SP_ISOWNED:
 555       return cstring_makeLiteralTemp ("owned");
 556     case SP_ISOBSERVER:
 557       return cstring_makeLiteralTemp ("observer");
 558     case SP_ISEXPOSED:
 559       return cstring_makeLiteralTemp ("exposed");
 560     }
 561
 562   BADEXIT;
 563 }
 564
 565 cstring specialClause_unparseKind (specialClause s)
 566 {
 567   return (message ("%s%s",
 568                    cstring_makeLiteralTemp (s->state == TK_BEFORE
 569                                             ? "pre:"
 570                                             : (s->state == TK_AFTER
 571                                                ? "post:" : "")),
 572                    specialClauseKind_unparse (s->kind)));
 573 }
 574
 575 cstring specialClause_unparse (specialClause s)
 576 {
 577   return (message ("%q %q",
 578                    specialClause_unparseKind (s), sRefSet_unparse (s->refs)));
 579 }
 580
 581 specialClause specialClause_createDefines (sRefSet s)
 582 {
 583   return (specialClause_create (TK_BOTH, SP_DEFINES, s));
 584 }
 585
 586 specialClause specialClause_createUses (sRefSet s)
 587 {
 588   return (specialClause_create (TK_BOTH, SP_USES, s));
 589 }
 590
 591 specialClause specialClause_createSets (sRefSet s)
 592 {
 593   return (specialClause_create (TK_BOTH, SP_SETS, s));
 594 }
 595
 596 specialClause specialClause_createReleases (sRefSet s)
 597 {
 598   return (specialClause_create (TK_BOTH, SP_RELEASES, s));
 599 }
 600
 601 specialClause specialClause_createAllocates (sRefSet s)
 602 {
 603   return (specialClause_create (TK_BOTH, SP_ALLOCATES, s));
 604 }
 605
 606 static /*@notnull@*/ specialClauses specialClauses_new (void)
 607 {
 608   specialClauses s = (specialClauses) dmalloc (sizeof (*s));
 609
 610   s->nelements = 0;
 611   s->nspace = specialClausesBASESIZE;
 612   s->elements = (specialClause *)
 613     dmalloc (sizeof (*s->elements) * specialClausesBASESIZE);
 614
 615   return (s);
 616 }
 617
 618 static void
 619 specialClauses_grow (specialClauses s)
 620 {
 621   int i;
 622   specialClause *newelements;
 623
 624   llassert (specialClauses_isDefined (s));
 625
 626   s->nspace += specialClausesBASESIZE;
 627
 628   newelements = (specialClause *)
 629     dmalloc (sizeof (*newelements) * (s->nelements + s->nspace));
 630
 631   for (i = 0; i < s->nelements; i++)
 632     {
 633       newelements[i] = s->elements[i];
 634     }
 635
 636   sfree (s->elements);
 637   s->elements = newelements;
 638 }
 639
 640 specialClauses specialClauses_add (specialClauses s, specialClause el)
 641 {
 642   if (specialClauses_isUndefined (s))
 643     {
 644       s = specialClauses_new ();
 645     }
 646   else
 647     {
 648       specialClauses_elements (s, cl)
 649         {
 650           if (specialClause_sameKind (cl, el))
 651             {
 652               voptgenerror
 653                 (FLG_SYNTAX,
 654                  message ("Multiple %q clauses for one function (using union)",
 655                           specialClause_unparseKind (cl)),
 656                  g_currentloc);
 657
 658               cl->refs = sRefSet_union (cl->refs, el->refs);
 659               specialClause_free (el);
 660               return s;
 661             }
 662         } end_specialClauses_elements ;
 663     }
 664
 665   if (s->nspace <= 0)
 666     {
 667       specialClauses_grow (s);
 668     }
 669
 670   s->nspace--;
 671   s->elements[s->nelements] = el;
 672   s->nelements++;
 673
 674   return s;
 675 }
 676
 677 cstring specialClauses_unparse (specialClauses s)
 678 {
 679   cstring st = cstring_undefined;
 680   int i;
 681
 682   if (specialClauses_isDefined (s))
 683     {
 684       for (i = 0; i < specialClauses_size (s); i++)
 685         {
 686           if (i == 0)
 687             {
 688               st = message ("%q;", specialClause_unparse (s->elements[i]));
 689             }
 690           else
 691             st = message ("%q %q;", st, specialClause_unparse (s->elements[i]));
 692         }
 693     }
 694
 695   return (st);
 696 }
 697
 698 specialClauses specialClauses_copy (specialClauses s)
 699 {
 700   if (specialClauses_isDefined (s))
 701     {
 702       specialClauses t = (specialClauses) dmalloc (sizeof (*t));
 703       int i;
 704
 705       t->nelements = s->nelements;
 706       t->nspace = 0;
 707
 708       if (s->nelements > 0)
 709         {
 710           t->elements = (specialClause *) dmalloc (sizeof (*t->elements) * t->nelements);
 711           for (i = 0; i < s->nelements; i++)
 712             {
 713               t->elements[i] = specialClause_copy (s->elements[i]);
 714             }
 715         }
 716       else
 717         {
 718           t->elements = NULL;
 719         }
 720
 721       return t;
 722     }
 723   else
 724     {
 725       return specialClauses_undefined;
 726     }
 727 }
 728
 729 void
 730 specialClauses_free (specialClauses s)
 731 {
 732   if (!specialClauses_isUndefined (s))
 733     {
 734       int i;
 735
 736       for (i = 0; i < s->nelements; i++)
 737         {
 738           specialClause_free (s->elements[i]);
 739         }
 740
 741       sfree (s->elements);
 742       sfree (s);
 743     }
 744 }
 745
 746 cstring specialClauses_dump (specialClauses s)
 747 {
 748   cstring st = cstring_undefined;
 749
 750   if (specialClauses_isUndefined (s)) return st;
 751
 752   specialClauses_elements (s, current)
 753     {
 754       st = message ("%q%q$", st, specialClause_dump (current));
 755     } end_specialClauses_elements;
 756
 757   return st;
 758 }
 759
 760 specialClauses specialClauses_undump (char **s)
 761 {
 762   char c;
 763   specialClauses pn = specialClauses_new ();
 764   int paramno = 0;
 765
 766   c = **s;
 767
 768   while (c != '#' && c != '@')
 769     {
 770       specialClause sc = specialClause_undump (s);
 771
 772       pn = specialClauses_add (pn, sc);
 773       reader_checkChar (s, '$');
 774       c = **s;
 775       paramno++;
 776     }
 777
 778   return pn;
 779 }
 780
 781 static /*@exposed@*/ sRefSet
 782   specialClauses_getClause (specialClauses s, stateConstraint st,
 783                             specialClauseKind k)
 784 {
 785   specialClauses_elements (s, el)
 786     {
 787       if (el->state == st && el->kind == k)
 788         {
 789           return el->refs;
 790         }
 791     } end_specialClauses_elements ;
 792
 793   return sRefSet_undefined;
 794 }
 795
 796 void specialClauses_checkAll (uentry ue)
 797 {
 798   specialClauses clauses = uentry_getSpecialClauses (ue);
 799   sRef res = uentry_getSref (ue);
 800   bool specialResult = FALSE;
 801
 802   specialClauses_elements (clauses, cl)
 803     {
 804       bool isPre = (cl->state == TK_BEFORE);
 805       sRefSet refs = cl->refs;
 806
 807       sRefSet_allElements (refs, el)
 808         {
 809           sRef rb = sRef_getRootBase (el);
 810
 811           if (sRef_isResult (rb))
 812             {
 813               if (isPre)
 814                 {
 815                   voptgenerror
 816                     (FLG_INCONDEFS,
 817                      message ("Function result is used in %q clause of %q "
 818                               "(%q applies to the state before function is "
 819                               "called, so should not use result): %q",
 820                               specialClause_unparseKind (cl),
 821                               uentry_getName (ue),
 822                               specialClause_unparseKind (cl),
 823                               sRef_unparse (el)),
 824                      uentry_whereLast (ue));
 825                 }
 826               else
 827                 {
 828                   if (!sRef_isStateSpecial (res))
 829                     {
 830                       if (!specialResult)
 831                         {
 832                           voptgenerror
 833                             (FLG_INCONDEFS,
 834                              message ("Function result is used in %q clause of %q "
 835                                       "but not annotated with special: %q",
 836                                       specialClause_unparseKind (cl),
 837                                       uentry_getName (ue),
 838                                       sRef_unparse (el)),
 839                              uentry_whereLast (ue));
 840
 841                           specialResult = TRUE;
 842                         }
 843                     }
 844
 845                   (void) sRef_fixResultType (el, sRef_getType (res), ue);
 846                 }
 847             }
 848           else if (sRef_isParam (rb))
 849             {
 850               if (!sRef_isStateSpecial (rb))
 851                 {
 852                   voptgenerror
 853                     (FLG_INCONDEFS,
 854                      message ("Reference %q used in %q clause of %q, "
 855                               "but not annotated with special: %q",
 856                               sRef_unparse (rb),
 857                               specialClause_unparseKind (cl),
 858                               uentry_getName (ue),
 859                               sRef_unparse (el)),
 860                      uentry_whereLast (ue));
 861                 }
 862             }
 863           else if (sRef_isInvalid (rb))
 864             {
 865               /*@innercontinue@*/ continue;
 866             }
 867           else
 868             {
 869               BADBRANCHCONT;
 870               /*@innercontinue@*/ continue;
 871             }
 872
 873           if (specialClause_isMemoryAllocation (cl))
 874             {
 875               if (!ctype_isVisiblySharable (sRef_getType (el)))
 876                 {
 877                   llerror
 878                     (FLG_SYNTAX,
 879                      message ("Special clause %q includes %q of "
 880                               "non-dynamically allocatated type %s",
 881                               specialClause_unparseKind (cl),
 882                               sRef_unparse (el),
 883                               ctype_unparse (sRef_getType (el))));
 884                 }
 885             }
 886
 887         } end_sRefSet_allElements ;
 888     } end_specialClauses_elements ;
 889 }
 890
 891 void specialClauses_checkEqual (uentry old, uentry unew)
 892 {
 893   specialClauses oldClauses = uentry_getSpecialClauses (old);
 894   specialClauses newClauses = uentry_getSpecialClauses (unew);
 895
 896   if (specialClauses_isDefined (newClauses))
 897     {
 898       specialClauses_elements (newClauses, cl)
 899         {
 900           sRefSet sc = specialClauses_getClause (oldClauses, cl->state, cl->kind);
 901
 902           if (!sRefSet_equal (sc, cl->refs))
 903             {
 904               if (optgenerror
 905                   (FLG_INCONDEFS,
 906                    message ("Function %q %rdeclared with inconsistent %q clause: %q",
 907                             uentry_getName (old),
 908                             uentry_isDeclared (old),
 909                             specialClause_unparseKind (cl),
 910                             sRefSet_unparsePlain (cl->refs)),
 911                    g_currentloc))
 912                 {
 913                   uentry_showWhereLastExtra (old, sRefSet_unparsePlain (sc));
 914                 }
 915             }
 916         } end_specialClauses_elements ;
 917
 918       specialClauses_elements (oldClauses, cl)
 919         {
 920           sRefSet sc = specialClauses_getClause (newClauses, cl->state, cl->kind);
 921
 922           if (sRefSet_isUndefined (sc) && !sRefSet_isEmpty (cl->refs))
 923             {
 924               if (optgenerror
 925                   (FLG_INCONDEFS,
 926                    message ("Function %q %rdeclared without %q clause (either "
 927                             "use no special clauses in redeclaration, or "
 928                             "they must match exactly: %q",
 929                             uentry_getName (old),
 930                             uentry_isDeclared (old),
 931                             specialClause_unparseKind (cl),
 932                             sRefSet_unparsePlain (cl->refs)),
 933                    g_currentloc))
 934                 {
 935                   uentry_showWhereLastExtra (old, sRefSet_unparsePlain (sc));
 936                 }
 937             }
 938         } end_specialClauses_elements ;
 939
 940     }
 941 }
 942
 943
 944