specialClauses.c Source File

00001 /*
00002 ** LCLint - annotation-assisted static program checker
00003 ** Copyright (C) 1994-2000 University of Virginia,
00004 **         Massachusetts Institute of Technology
00005 **
00006 ** This program is free software; you can redistribute it and/or modify it
00007 ** under the terms of the GNU General Public License as published by the
00008 ** Free Software Foundation; either version 2 of the License, or (at your
00009 ** option) any later version.
00010 ** 
00011 ** This program is distributed in the hope that it will be useful, but
00012 ** WITHOUT ANY WARRANTY; without even the implied warranty of
00013 ** MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
00014 ** General Public License for more details.
00015 ** 
00016 ** The GNU General Public License is available from http://www.gnu.org/ or
00017 ** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston,
00018 ** MA 02111-1307, USA.
00019 **
00020 ** For information on lclint: lclint-request@cs.virginia.edu
00021 ** To report a bug: lclint-bug@cs.virginia.edu
00022 ** For more information: http://lclint.cs.virginia.edu
00023 */
00024 /*
00025 ** specialClauses.c
00026 */
00027 
00028 # include "lclintMacros.nf"
00029 # include "basic.h"
00030 
00031 static bool specialClause_isMemoryAllocation (specialClause p_cl) /*@*/ ;
00032 static void specialClause_free (/*@only@*/ specialClause p_s) ;
00033 static cstring specialClause_dump (specialClause p_s) /*@*/ ;
00034 static specialClause specialClause_undump (char **p_s) /*@modifies *p_s@*/ ;
00035 static specialClause specialClause_copy (specialClause p_s) /*@*/ ;
00036 static bool specialClause_sameKind (specialClause p_s1, specialClause p_s2) /*@*/ ;
00037 
00038 specialClause 
00039   specialClause_create (stateConstraint st, specialClauseKind k, sRefSet s) 
00040 {
00041   specialClause ret = (specialClause) dmalloc (sizeof (*ret));
00042 
00043   ret->state = st;
00044   ret->kind = k;
00045   ret->refs = s;
00046 
00047   return ret;
00048 }
00049 
00050 bool specialClause_isBefore (specialClause cl)
00051 {
00052   return (cl->state == TK_BEFORE || cl->state == TK_BOTH);
00053 }
00054 
00055 bool specialClause_isAfter (specialClause cl)
00056 {
00057   return (cl->state == TK_AFTER || cl->state == TK_BOTH);
00058 }
00059 
00060 bool specialClause_isMemoryAllocation (specialClause cl)
00061 {
00062   switch (cl->kind)
00063     {
00064     case SP_ALLOCATES:
00065     case SP_RELEASES:
00066     case SP_ISONLY:
00067     case SP_ISSHARED:
00068     case SP_ISDEPENDENT:
00069     case SP_ISOWNED:
00070     case SP_ISOBSERVER:
00071     case SP_ISEXPOSED:
00072       return TRUE;
00073     case SP_USES:
00074     case SP_DEFINES:
00075     case SP_SETS:
00076     case SP_ISNULL:
00077     case SP_ISNOTNULL:
00078       return FALSE;
00079   }
00080 
00081   BADEXIT;
00082 }
00083 
00084 /*
00085 ** An error is reported if the test is NOT true.
00086 */
00087 
00088 sRefTest specialClause_getPreTestFunction (specialClause cl)
00089 {
00090   switch (cl->kind)
00091     {
00092     case SP_USES:
00093       return sRef_isStrictReadable;
00094     case SP_ALLOCATES:
00095       return sRef_hasNoStorage; 
00096     case SP_DEFINES:
00097       return sRef_hasNoStorage;
00098     case SP_SETS:
00099       return sRef_isNotUndefined;
00100     case SP_RELEASES:
00101       return sRef_isNotUndefined;
00102     case SP_ISONLY:
00103       return sRef_isOnly;
00104     case SP_ISSHARED:
00105       return sRef_isShared;
00106     case SP_ISDEPENDENT:
00107       return sRef_isDependent;
00108     case SP_ISOWNED:
00109       return sRef_isOwned;
00110     case SP_ISOBSERVER:
00111       return sRef_isObserver;
00112     case SP_ISEXPOSED:
00113       return sRef_isExposed;
00114     case SP_ISNOTNULL:
00115       return sRef_isNotNull;
00116     case SP_ISNULL:
00117       return sRef_isDefinitelyNull;
00118   }
00119 
00120   BADEXIT;
00121 }
00122 
00123 sRefTest specialClause_getPostTestFunction (specialClause cl)
00124 {
00125   llassert (specialClause_isAfter (cl));
00126 
00127   switch (cl->kind)
00128     {
00129     case SP_USES:
00130       return NULL;
00131     case SP_ALLOCATES:
00132       return sRef_isAllocated;
00133     case SP_DEFINES:
00134       return sRef_isReallyDefined;
00135     case SP_SETS:
00136       return sRef_isReallyDefined;
00137     case SP_RELEASES:
00138       return sRef_isDeadStorage;
00139     case SP_ISONLY:
00140       return sRef_isOnly;
00141     case SP_ISSHARED:
00142       return sRef_isShared;
00143     case SP_ISDEPENDENT:
00144       return sRef_isDependent;
00145     case SP_ISOWNED:
00146       return sRef_isOwned;
00147     case SP_ISOBSERVER:
00148       return sRef_isObserver;
00149     case SP_ISEXPOSED:
00150       return sRef_isExposed;
00151     case SP_ISNOTNULL:
00152       return sRef_isNotNull;
00153     case SP_ISNULL:
00154       return sRef_isDefinitelyNull;
00155   }
00156 
00157   BADEXIT;
00158 }
00159 
00160 sRefShower specialClause_getPostTestShower (specialClause cl)
00161 {
00162   switch (cl->kind)
00163     {
00164     case SP_USES:
00165     case SP_ALLOCATES:
00166       return NULL;
00167     case SP_DEFINES:
00168     case SP_SETS:
00169       return sRef_showNotReallyDefined;
00170     case SP_RELEASES:
00171       return NULL;
00172     case SP_ISONLY:
00173     case SP_ISSHARED:
00174     case SP_ISDEPENDENT:
00175     case SP_ISOWNED:
00176       return sRef_showAliasInfo;
00177     case SP_ISOBSERVER:
00178     case SP_ISEXPOSED:
00179       return sRef_showExpInfo;
00180     case SP_ISNOTNULL:
00181     case SP_ISNULL:
00182       return sRef_showNullInfo;
00183   }
00184 
00185   BADEXIT;
00186 }
00187 
00188 sRefMod specialClause_getEntryFunction (specialClause cl)
00189 {
00190   if (cl->state == TK_BEFORE || cl->state == TK_BOTH)
00191     {
00192       switch (cl->kind)
00193         {
00194         case SP_USES:
00195           return sRef_setDefinedComplete;
00196         case SP_ALLOCATES:
00197           return NULL;
00198         case SP_DEFINES:
00199           return NULL;
00200         case SP_SETS:
00201           return sRef_setAllocatedComplete;
00202         case SP_RELEASES:
00203           return sRef_setDefinedComplete;
00204         case SP_ISONLY:
00205           return sRef_setOnly;
00206         case SP_ISSHARED:
00207           return sRef_setShared;
00208         case SP_ISDEPENDENT:
00209           return sRef_setDependent;
00210         case SP_ISOWNED:
00211           return sRef_setOwned;
00212         case SP_ISOBSERVER:
00213           return sRef_setObserver;
00214         case SP_ISEXPOSED:
00215           return sRef_setExposed;
00216         case SP_ISNOTNULL:
00217           return sRef_setNotNull;
00218         case SP_ISNULL:
00219           return sRef_setDefNull;
00220         }
00221 
00222       BADBRANCH;
00223     }
00224   else
00225     {
00226       return NULL;
00227     }
00228 }
00229 
00230 sRefMod specialClause_getEffectFunction (specialClause cl)
00231 {
00232   if (cl->state == TK_AFTER || cl->state == TK_BOTH)
00233     {
00234       switch (cl->kind)
00235         {
00236         case SP_USES:
00237           return NULL;
00238         case SP_ALLOCATES:
00239           return sRef_setAllocatedComplete;
00240         case SP_DEFINES:
00241           return sRef_setDefinedNCComplete;
00242         case SP_SETS:
00243           return sRef_setDefinedNCComplete;
00244         case SP_RELEASES:
00245           return sRef_killComplete;
00246         case SP_ISONLY:
00247           return sRef_setOnly;
00248         case SP_ISSHARED:
00249           return sRef_setShared;
00250         case SP_ISDEPENDENT:
00251           return sRef_setDependent;
00252         case SP_ISOWNED:
00253           return sRef_setOwned;
00254         case SP_ISOBSERVER:
00255           return sRef_setObserver;
00256         case SP_ISEXPOSED:
00257           return sRef_setExposed;
00258         case SP_ISNOTNULL:
00259           return sRef_setNotNull;
00260         case SP_ISNULL:
00261           return sRef_setDefNull;
00262         }
00263 
00264       BADBRANCH;
00265     }
00266   else
00267     {
00268       return NULL;
00269     }
00270 }
00271 
00272 sRefMod specialClause_getReturnEffectFunction (specialClause cl)
00273 {
00274   if (cl->state == TK_AFTER || cl->state == TK_BOTH)
00275     {
00276       switch (cl->kind)
00277         {
00278         case SP_USES:
00279         case SP_ALLOCATES:
00280         case SP_DEFINES:
00281         case SP_SETS:
00282         case SP_RELEASES:
00283           return NULL;
00284         case SP_ISONLY:
00285           return sRef_killComplete;
00286         case SP_ISSHARED:
00287         case SP_ISDEPENDENT:
00288         case SP_ISOWNED:
00289         case SP_ISOBSERVER:
00290         case SP_ISEXPOSED:
00291         case SP_ISNULL:
00292         case SP_ISNOTNULL:
00293           return NULL;
00294         }
00295 
00296       BADBRANCH;
00297     }
00298   else
00299     {
00300       return NULL;
00301     }
00302 }
00303 
00304 flagcode specialClause_preErrorCode (specialClause cl)
00305 {
00306   llassert (cl->state == TK_BOTH || cl->state == TK_BEFORE);
00307 
00308   switch (cl->kind)
00309     {
00310     case SP_USES:
00311       return FLG_USEDEF;
00312     case SP_ALLOCATES: /*@fallthrough@*/ 
00313     case SP_DEFINES:
00314     case SP_SETS:
00315       return FLG_MUSTFREE;
00316     case SP_RELEASES:
00317       return FLG_USEDEF;
00318     case SP_ISONLY:
00319       return FLG_ONLYTRANS;
00320     case SP_ISSHARED:
00321       return FLG_SHAREDTRANS;
00322     case SP_ISDEPENDENT:
00323       return FLG_DEPENDENTTRANS;
00324     case SP_ISOWNED:
00325       return FLG_OWNEDTRANS;
00326     case SP_ISOBSERVER:
00327       return FLG_OBSERVERTRANS;
00328     case SP_ISEXPOSED:
00329       return FLG_EXPOSETRANS;
00330     case SP_ISNULL:
00331     case SP_ISNOTNULL:
00332       return FLG_NULLSTATE;
00333   }
00334 
00335   BADBRANCH;
00336 }
00337 
00338 cstring specialClause_preErrorString (specialClause cl, sRef sr)
00339 {
00340   llassert (cl->state == TK_BOTH || cl->state == TK_BEFORE);
00341 
00342   switch (cl->kind)
00343     {
00344     case SP_USES:
00345       if (sRef_isDead (sr)) 
00346         return cstring_makeLiteralTemp ("Dead");
00347       else
00348         return cstring_makeLiteralTemp ("Undefined");
00349     case SP_ALLOCATES: /*@fallthrough@*/ 
00350     case SP_DEFINES:
00351     case SP_SETS:
00352       return cstring_makeLiteralTemp ("Allocated");
00353     case SP_RELEASES:
00354       if (sRef_isDead (sr)) 
00355         {
00356           return cstring_makeLiteralTemp ("Dead");
00357         }
00358       else if (sRef_isDependent (sr) 
00359                || sRef_isShared (sr))
00360         {
00361           return alkind_unparse (sRef_getAliasKind (sr));
00362         }
00363       else if (sRef_isObserver (sr) || sRef_isExposed (sr))
00364         {
00365           return exkind_unparse (sRef_getExKind (sr));
00366         }
00367       else
00368         {
00369           return cstring_makeLiteralTemp ("Undefined");
00370         }
00371     case SP_ISONLY:
00372     case SP_ISSHARED:
00373     case SP_ISDEPENDENT:
00374     case SP_ISOWNED:
00375       return alkind_capName (sRef_getAliasKind (sr));
00376     case SP_ISOBSERVER:
00377       return cstring_makeLiteralTemp ("Non-observer");
00378     case SP_ISEXPOSED:
00379       if (sRef_isObserver (sr))
00380         {
00381           return cstring_makeLiteralTemp ("Observer");
00382         }
00383       else
00384         {
00385           return cstring_makeLiteralTemp ("Non-exposed");
00386         }
00387     case SP_ISNOTNULL:
00388       if (sRef_isDefinitelyNull (sr))
00389         {
00390           return cstring_makeLiteralTemp ("Null");
00391         }
00392       else
00393         {
00394           return cstring_makeLiteralTemp ("Possibly null");
00395         }
00396     case SP_ISNULL:
00397       return cstring_makeLiteralTemp ("Non-null");
00398   }
00399 
00400   BADEXIT;
00401 }
00402 
00403 flagcode specialClause_postErrorCode (specialClause cl)
00404 {
00405   llassert (cl->state == TK_BOTH || cl->state == TK_AFTER);
00406 
00407   switch (cl->kind)
00408     {
00409     case SP_USES:
00410       BADBRANCHCONT;
00411       return INVALID_FLAG;
00412     case SP_ALLOCATES: 
00413     case SP_DEFINES:  
00414     case SP_SETS:     
00415       return FLG_COMPDEF;
00416     case SP_RELEASES:
00417       return FLG_MUSTFREE;
00418     case SP_ISONLY:
00419       return FLG_ONLYTRANS;
00420     case SP_ISSHARED:
00421       return FLG_SHAREDTRANS;
00422     case SP_ISDEPENDENT:
00423       return FLG_DEPENDENTTRANS;
00424     case SP_ISOWNED:
00425       return FLG_OWNEDTRANS;
00426     case SP_ISOBSERVER:
00427       return FLG_OBSERVERTRANS;
00428     case SP_ISEXPOSED:
00429       return FLG_EXPOSETRANS;
00430     case SP_ISNULL:
00431     case SP_ISNOTNULL:
00432       return FLG_NULLSTATE;
00433   }
00434 
00435   BADBRANCH;
00436 }
00437 
00438 cstring specialClause_postErrorString (specialClause cl, sRef sr)
00439 {
00440   llassert (cl->state == TK_BOTH || cl->state == TK_AFTER);
00441 
00442   switch (cl->kind)
00443     {
00444     case SP_USES:
00445       BADBRANCHCONT;
00446       return cstring_makeLiteralTemp ("<ERROR>");
00447     case SP_ALLOCATES: 
00448       return cstring_makeLiteralTemp ("Unallocated");
00449     case SP_DEFINES:
00450     case SP_SETS:
00451       return cstring_makeLiteralTemp ("Undefined");
00452     case SP_RELEASES:
00453       return cstring_makeLiteralTemp ("Unreleased");
00454     case SP_ISONLY:
00455     case SP_ISSHARED:
00456     case SP_ISOWNED:
00457     case SP_ISDEPENDENT:
00458       return alkind_capName (sRef_getAliasKind (sr));
00459     case SP_ISOBSERVER:
00460       return cstring_makeLiteralTemp ("Non-observer");
00461     case SP_ISEXPOSED:
00462       if (sRef_isObserver (sr))
00463         {
00464           return cstring_makeLiteralTemp ("Observer");
00465         }
00466       else
00467         {
00468           return cstring_makeLiteralTemp ("Non-exposed");
00469         }
00470     case SP_ISNULL:
00471       return cstring_makeLiteralTemp ("Non-null");
00472     case SP_ISNOTNULL:
00473       if (sRef_isDefinitelyNull (sr))
00474         {
00475           return cstring_makeLiteralTemp ("Null");
00476         }
00477       else
00478         {
00479           return cstring_makeLiteralTemp ("Possibly null");
00480         }
00481   }
00482 
00483   BADEXIT;
00484 }
00485 
00486 cstring specialClause_dump (specialClause s)
00487 {
00488   return (message ("%d.%d.%q",
00489                    (int) s->state,
00490                    (int) s->kind,
00491                    sRefSet_dump (s->refs)));
00492 }
00493 
00494 specialClause specialClause_undump (char **s)
00495 {
00496   specialClause ret = (specialClause) dmalloc (sizeof (*ret));
00497 
00498   ret->state = (stateConstraint) getInt (s);
00499   checkChar (s, '.');
00500   ret->kind = (specialClauseKind) getInt (s);
00501   checkChar (s, '.');
00502   ret->refs = sRefSet_undump (s);
00503 
00504   return ret;
00505 }
00506 
00507 specialClause specialClause_copy (specialClause s) 
00508 {
00509   specialClause ret = (specialClause) dmalloc (sizeof (*ret));
00510   
00511   ret->state = s->state;
00512   ret->kind = s->kind;
00513   ret->refs = sRefSet_newCopy (s->refs);
00514   
00515   return ret;
00516 }
00517 
00518 bool specialClause_sameKind (specialClause s1, specialClause s2)
00519 {
00520   return (s1->state == s2->state && s1->kind == s2->kind);
00521 }
00522 
00523 void specialClause_free (specialClause s)
00524 {
00525   sRefSet_free (s->refs);
00526   sfree (s);
00527 }
00528 
00529 static /*@observer@*/ cstring 
00530   specialClauseKind_unparse (specialClauseKind k) 
00531 {
00532   switch (k)
00533     {
00534     case SP_USES: 
00535       return cstring_makeLiteralTemp ("uses");
00536     case SP_DEFINES:
00537       return cstring_makeLiteralTemp ("defines");
00538     case SP_ALLOCATES:
00539       return cstring_makeLiteralTemp ("allocates");
00540     case SP_RELEASES:
00541       return cstring_makeLiteralTemp ("releases");
00542     case SP_SETS:
00543       return cstring_makeLiteralTemp ("sets");
00544     case SP_ISNULL:
00545       return cstring_makeLiteralTemp ("isnull");
00546     case SP_ISNOTNULL:
00547       return cstring_makeLiteralTemp ("notnull");
00548     case SP_ISONLY:
00549       return cstring_makeLiteralTemp ("only");
00550     case SP_ISSHARED:
00551       return cstring_makeLiteralTemp ("shared");
00552     case SP_ISDEPENDENT:
00553       return cstring_makeLiteralTemp ("dependent");
00554     case SP_ISOWNED:
00555       return cstring_makeLiteralTemp ("owned");
00556     case SP_ISOBSERVER:
00557       return cstring_makeLiteralTemp ("observer");
00558     case SP_ISEXPOSED:
00559       return cstring_makeLiteralTemp ("exposed");
00560     }
00561 
00562   BADEXIT;
00563 }
00564 
00565 cstring specialClause_unparseKind (specialClause s)
00566 {
00567   return (message ("%s%s",
00568                    cstring_makeLiteralTemp (s->state == TK_BEFORE 
00569                                             ? "pre:"
00570                                             : (s->state == TK_AFTER
00571                                                ? "post:" : "")),
00572                    specialClauseKind_unparse (s->kind)));
00573 }
00574 
00575 cstring specialClause_unparse (specialClause s)
00576 {
00577   return (message ("%q %q", 
00578                    specialClause_unparseKind (s), sRefSet_unparse (s->refs)));
00579 }
00580 
00581 specialClause specialClause_createDefines (sRefSet s)
00582 {
00583   return (specialClause_create (TK_BOTH, SP_DEFINES, s));
00584 }
00585 
00586 specialClause specialClause_createUses (sRefSet s)
00587 {
00588   return (specialClause_create (TK_BOTH, SP_USES, s));
00589 }
00590 
00591 specialClause specialClause_createSets (sRefSet s)
00592 {
00593   return (specialClause_create (TK_BOTH, SP_SETS, s));
00594 }
00595 
00596 specialClause specialClause_createReleases (sRefSet s)
00597 {
00598   return (specialClause_create (TK_BOTH, SP_RELEASES, s));
00599 }
00600 
00601 specialClause specialClause_createAllocates (sRefSet s)
00602 {
00603   return (specialClause_create (TK_BOTH, SP_ALLOCATES, s));
00604 }
00605 
00606 static /*@notnull@*/ specialClauses specialClauses_new (void)
00607 {
00608   specialClauses s = (specialClauses) dmalloc (sizeof (*s));
00609   
00610   s->nelements = 0;
00611   s->nspace = specialClausesBASESIZE;
00612   s->elements = (specialClause *) 
00613     dmalloc (sizeof (*s->elements) * specialClausesBASESIZE);
00614 
00615   return (s);
00616 }
00617 
00618 static void
00619 specialClauses_grow (specialClauses s)
00620 {
00621   int i;
00622   specialClause *newelements;
00623 
00624   llassert (specialClauses_isDefined (s));
00625 
00626   s->nspace += specialClausesBASESIZE; 
00627   
00628   newelements = (specialClause *) 
00629     dmalloc (sizeof (*newelements) * (s->nelements + s->nspace));
00630   
00631   for (i = 0; i < s->nelements; i++)
00632     {
00633       newelements[i] = s->elements[i];
00634     }
00635   
00636   sfree (s->elements);
00637   s->elements = newelements;
00638 }
00639 
00640 specialClauses specialClauses_add (specialClauses s, specialClause el)
00641 {
00642   if (specialClauses_isUndefined (s))
00643     {
00644       s = specialClauses_new ();
00645     }
00646   else
00647     {
00648       specialClauses_elements (s, cl)
00649         {
00650           if (specialClause_sameKind (cl, el))
00651             {
00652               voptgenerror
00653                 (FLG_SYNTAX,
00654                  message ("Multiple %q clauses for one function (using union)",
00655                           specialClause_unparseKind (cl)),
00656                  g_currentloc);
00657 
00658               cl->refs = sRefSet_union (cl->refs, el->refs);
00659               specialClause_free (el);
00660               return s;
00661             }
00662         } end_specialClauses_elements ;
00663     }
00664 
00665   if (s->nspace <= 0)
00666     {
00667       specialClauses_grow (s);
00668     }
00669   
00670   s->nspace--;
00671   s->elements[s->nelements] = el;
00672   s->nelements++;
00673 
00674   return s;
00675 }
00676 
00677 cstring specialClauses_unparse (specialClauses s)
00678 {
00679   cstring st = cstring_undefined;
00680   int i;
00681   
00682   if (specialClauses_isDefined (s))
00683     {
00684       for (i = 0; i < specialClauses_size (s); i++)
00685         {
00686           if (i == 0)
00687             {
00688               st = message ("%q;", specialClause_unparse (s->elements[i]));
00689             }
00690           else
00691             st = message ("%q %q;", st, specialClause_unparse (s->elements[i]));
00692         }
00693     }
00694   
00695   return (st);
00696 }
00697 
00698 specialClauses specialClauses_copy (specialClauses s)
00699 {
00700   if (specialClauses_isDefined (s))
00701     {
00702       specialClauses t = (specialClauses) dmalloc (sizeof (*t));
00703       int i;
00704       
00705       t->nelements = s->nelements;
00706       t->nspace = 0;
00707       
00708       if (s->nelements > 0)
00709         {
00710           t->elements = (specialClause *) dmalloc (sizeof (*t->elements) * t->nelements);
00711           for (i = 0; i < s->nelements; i++) 
00712             {
00713               t->elements[i] = specialClause_copy (s->elements[i]); 
00714             }
00715         }
00716       else
00717         {
00718           t->elements = NULL;
00719         }
00720 
00721       return t;
00722     }
00723   else
00724     {
00725       return specialClauses_undefined;
00726     }
00727 }
00728 
00729 void
00730 specialClauses_free (specialClauses s)
00731 {
00732   if (!specialClauses_isUndefined (s)) 
00733     {
00734       int i;
00735 
00736       for (i = 0; i < s->nelements; i++)
00737         {
00738           specialClause_free (s->elements[i]);  
00739         }
00740 
00741       sfree (s->elements);
00742       sfree (s);
00743     }
00744 }
00745 
00746 cstring specialClauses_dump (specialClauses s)
00747 {
00748   cstring st = cstring_undefined;
00749 
00750   if (specialClauses_isUndefined (s)) return st;
00751   
00752   specialClauses_elements (s, current)
00753     {
00754       st = message ("%q%q$", st, specialClause_dump (current));
00755     } end_specialClauses_elements;
00756 
00757   return st;
00758 }
00759 
00760 specialClauses specialClauses_undump (char **s)
00761 {
00762   char c;
00763   specialClauses pn = specialClauses_new ();
00764   int paramno = 0;
00765 
00766   c = **s;
00767 
00768   while (c != '#' && c != '@')
00769     {
00770       specialClause sc = specialClause_undump (s);
00771       
00772       pn = specialClauses_add (pn, sc);
00773       checkChar (s, '$');
00774       c = **s;
00775       paramno++;
00776     }
00777 
00778   return pn;
00779 }
00780 
00781 static /*@exposed@*/ sRefSet
00782   specialClauses_getClause (specialClauses s, stateConstraint st, 
00783                             specialClauseKind k)
00784 {
00785   specialClauses_elements (s, el)
00786     {
00787       if (el->state == st && el->kind == k)
00788         {
00789           return el->refs;
00790         }
00791     } end_specialClauses_elements ;
00792 
00793   return sRefSet_undefined;
00794 }
00795 
00796 void specialClauses_checkAll (uentry ue)
00797 {
00798   specialClauses clauses = uentry_getSpecialClauses (ue);
00799   sRef res = uentry_getSref (ue);                 
00800   bool specialResult = FALSE;
00801 
00802   specialClauses_elements (clauses, cl)
00803     {
00804       bool isPre = (cl->state == TK_BEFORE);
00805       sRefSet refs = cl->refs;
00806 
00807       sRefSet_allElements (refs, el)
00808         {
00809           sRef rb = sRef_getRootBase (el);
00810 
00811           if (sRef_isResult (rb))
00812             {
00813               if (isPre)
00814                 {
00815                   voptgenerror
00816                     (FLG_INCONDEFS,
00817                      message ("Function result is used in %q clause of %q "
00818                               "(%q applies to the state before function is "
00819                               "called, so should not use result): %q",
00820                               specialClause_unparseKind (cl),
00821                               uentry_getName (ue),
00822                               specialClause_unparseKind (cl),
00823                               sRef_unparse (el)),
00824                      uentry_whereLast (ue));
00825                 }
00826               else
00827                 {
00828                   if (!sRef_isStateSpecial (res))
00829                     {
00830                       if (!specialResult)
00831                         {
00832                           voptgenerror
00833                             (FLG_INCONDEFS,
00834                              message ("Function result is used in %q clause of %q "
00835                                       "but not annotated with special: %q",
00836                                       specialClause_unparseKind (cl),
00837                                       uentry_getName (ue),
00838                                       sRef_unparse (el)),
00839                              uentry_whereLast (ue));
00840 
00841                           specialResult = TRUE;
00842                         }
00843                     }
00844 
00845                   (void) sRef_fixResultType (el, sRef_getType (res), ue);
00846                 }
00847             }
00848           else if (sRef_isParam (rb))
00849             {
00850               if (!sRef_isStateSpecial (rb))
00851                 {
00852                   voptgenerror 
00853                     (FLG_INCONDEFS,
00854                      message ("Reference %q used in %q clause of %q, "
00855                               "but not annotated with special: %q",
00856                               sRef_unparse (rb),
00857                               specialClause_unparseKind (cl),
00858                               uentry_getName (ue),
00859                               sRef_unparse (el)),
00860                      uentry_whereLast (ue));
00861                 }
00862             }
00863           else if (sRef_isInvalid (rb))
00864             {
00865               /*@innercontinue@*/ continue;
00866             }
00867           else 
00868             {
00869               BADBRANCHCONT;
00870               /*@innercontinue@*/ continue;
00871             }
00872 
00873           if (specialClause_isMemoryAllocation (cl))
00874             {
00875               if (!ctype_isVisiblySharable (sRef_getType (el)))
00876                 {
00877                   llerror 
00878                     (FLG_SYNTAX, 
00879                      message ("Special clause %q includes %q of "
00880                               "non-dynamically allocatated type %s",
00881                               specialClause_unparseKind (cl),
00882                               sRef_unparse (el), 
00883                               ctype_unparse (sRef_getType (el))));
00884                 }
00885             }
00886 
00887         } end_sRefSet_allElements ;
00888     } end_specialClauses_elements ;
00889 }
00890   
00891 void specialClauses_checkEqual (uentry old, uentry unew)
00892 {
00893   specialClauses oldClauses = uentry_getSpecialClauses (old);
00894   specialClauses newClauses = uentry_getSpecialClauses (unew);
00895 
00896   if (specialClauses_isDefined (newClauses))
00897     {
00898       specialClauses_elements (newClauses, cl)
00899         {
00900           sRefSet sc = specialClauses_getClause (oldClauses, cl->state, cl->kind);
00901 
00902           if (!sRefSet_equal (sc, cl->refs))
00903             {
00904               if (optgenerror
00905                   (FLG_INCONDEFS,
00906                    message ("Function %q %rdeclared with inconsistent %q clause: %q",
00907                             uentry_getName (old),
00908                             uentry_isDeclared (old),
00909                             specialClause_unparseKind (cl),
00910                             sRefSet_unparsePlain (cl->refs)),
00911                    g_currentloc))
00912                 {
00913                   uentry_showWhereLastExtra (old, sRefSet_unparsePlain (sc));
00914                 }
00915             }
00916         } end_specialClauses_elements ;
00917 
00918       specialClauses_elements (oldClauses, cl)
00919         {
00920           sRefSet sc = specialClauses_getClause (newClauses, cl->state, cl->kind);
00921 
00922           if (sRefSet_isUndefined (sc) && !sRefSet_isEmpty (cl->refs))
00923             {
00924               if (optgenerror
00925                   (FLG_INCONDEFS,
00926                    message ("Function %q %rdeclared without %q clause (either "
00927                             "use no special clauses in redeclaration, or "
00928                             "they must match exactly: %q",
00929                             uentry_getName (old),
00930                             uentry_isDeclared (old),
00931                             specialClause_unparseKind (cl),
00932                             sRefSet_unparsePlain (cl->refs)),
00933                    g_currentloc))
00934                 {
00935                   uentry_showWhereLastExtra (old, sRefSet_unparsePlain (sc));
00936                 }
00937             }
00938         } end_specialClauses_elements ;
00939 
00940     }
00941 }
00942 
00943 
00944