[splint.git] / src / stateClause.c

/*
** Splint - annotation-assisted static program checker
** Copyright (C) 1994-2002 University of Virginia,
**         Massachusetts Institute of Technology
**
** This program is free software; you can redistribute it and/or modify it
** under the terms of the GNU General Public License as published by the
** Free Software Foundation; either version 2 of the License, or (at your
** option) any later version.
** 
** This program is distributed in the hope that it will be useful, but
** WITHOUT ANY WARRANTY; without even the implied warranty of
** MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
** General Public License for more details.
** 
** The GNU General Public License is available from http://www.gnu.org/ or
** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston,
** MA 02111-1307, USA.
**
** For information on lclint: lclint-request@cs.virginia.edu
** To report a bug: lclint-bug@cs.virginia.edu
** For more information: http://www.splint.org
*/
/*
** stateClause.c
*/

# include "lclintMacros.nf"
# include "basic.h"
# include "cgrammar.h"
# include "cgrammar_tokens.h"

static stateClause 
stateClause_createRaw (stateConstraint st, stateClauseKind sk, /*@only@*/ sRefSet s) 
{
  stateClause ret = (stateClause) dmalloc (sizeof (*ret));

  ret->state = st;
  ret->kind = sk;
  ret->squal = qual_createUnknown ();
  ret->refs = s;
  ret->loc = fileloc_undefined;
  return ret;
}

stateClause 
stateClause_create (lltok tok, qual q, sRefSet s) 
{
  stateClause ret = (stateClause) dmalloc (sizeof (*ret));

  if (lltok_getTok (tok) == QPRECLAUSE) 
    {
      ret->state = TK_BEFORE;
    }
  else if (lltok_getTok (tok) == QPOSTCLAUSE)
    {
      ret->state = TK_AFTER;
    }
  else
    {
      BADBRANCH;
    }

  ret->loc = fileloc_copy (lltok_getLoc (tok));

  ret->squal = q;
  ret->refs = s;

  if (sRefSet_isDefined (s))
    {
      ret->kind = SP_QUAL;
    }
  else
    {
      ret->kind = SP_GLOBAL;
    }

  return ret;
}

bool stateClause_isBeforeOnly (stateClause cl)
{
  return (cl->state == TK_BEFORE);
}

bool stateClause_isBefore (stateClause cl)
{
  return (cl->state == TK_BEFORE || cl->state == TK_BOTH);
}

bool stateClause_isAfter (stateClause cl)
{
  return (cl->state == TK_AFTER || cl->state == TK_BOTH);
}

bool stateClause_isEnsures (stateClause cl)
{
  return (cl->state == TK_AFTER);
}

bool stateClause_isQual (stateClause cl)
{
  return (cl->kind == SP_QUAL);
}

bool stateClause_isMemoryAllocation (stateClause cl)
{
  switch (cl->kind)
    {
    case SP_ALLOCATES:
    case SP_RELEASES:
      return TRUE;
    case SP_USES:
    case SP_DEFINES:
    case SP_SETS:
      return FALSE;
    case SP_GLOBAL:
      return FALSE;
    case SP_QUAL:
      return (qual_isMemoryAllocation (cl->squal)
	      || qual_isSharing (cl->squal));
    }
  
  BADEXIT;
}

/*
** An error is reported if the test is NOT true.
*/

sRefTest stateClause_getPreTestFunction (stateClause cl)
{
  switch (cl->kind)
    {
    case SP_USES:
      return sRef_isStrictReadable;
    case SP_ALLOCATES:
      return sRef_hasNoStorage; 
    case SP_DEFINES:
      return sRef_hasNoStorage;
    case SP_SETS:
      return sRef_isNotUndefined;
    case SP_RELEASES:
      return sRef_isNotUndefined;
    case SP_GLOBAL:
      BADBRANCH;
    case SP_QUAL:
      {
	if (qual_isOnly (cl->squal)) {
	  return sRef_isOnly;
	} else if (qual_isShared (cl->squal)) {
	  return sRef_isShared;
	} else if (qual_isDependent (cl->squal)) {
	  return sRef_isDependent;
	} else if (qual_isOwned (cl->squal)) {
	  return sRef_isOwned;
	} else if (qual_isObserver (cl->squal)) {
	  return sRef_isObserver;
	} else if (qual_isExposed (cl->squal)) {
	  return sRef_isExposed;
	} else if (qual_isNotNull (cl->squal)) {
	  return sRef_isNotNull;
	} else if (qual_isIsNull (cl->squal)) {
	  return sRef_isDefinitelyNull;
	} else {
	  BADBRANCH;
	}
      }
  }

  BADEXIT;
}

sRefTest stateClause_getPostTestFunction (stateClause cl)
{
  llassert (stateClause_isAfter (cl));

  switch (cl->kind)
    {
    case SP_USES:
      return NULL;
    case SP_ALLOCATES:
      return sRef_isAllocated;
    case SP_DEFINES:
      return sRef_isReallyDefined;
    case SP_SETS:
      return sRef_isReallyDefined;
    case SP_RELEASES:
      return sRef_isDeadStorage;
    case SP_GLOBAL:
      BADBRANCH;
    case SP_QUAL:
      if (qual_isOnly (cl->squal)) {
	return sRef_isOnly;
      } else if (qual_isShared (cl->squal)) {
	return sRef_isShared;
      } else if (qual_isDependent (cl->squal)) {
	return sRef_isDependent;
      } else if (qual_isOwned (cl->squal)) {
	return sRef_isOwned;
      } else if (qual_isObserver (cl->squal)) {
	return sRef_isObserver;
      } else if (qual_isExposed (cl->squal)) {
	return sRef_isExposed;
      } else if (qual_isNotNull (cl->squal)) {
	return sRef_isNotNull;
      } else if (qual_isIsNull (cl->squal)) {
	return sRef_isDefinitelyNull;
      } else {
	BADBRANCH;
      }
    }
  
  BADEXIT;
}

sRefShower stateClause_getPostTestShower (stateClause cl)
{
  switch (cl->kind)
    {
    case SP_USES:
    case SP_ALLOCATES:
      return NULL;
    case SP_DEFINES:
    case SP_SETS:
      return sRef_showNotReallyDefined;
    case SP_RELEASES:
      return NULL;
    case SP_GLOBAL:
      BADBRANCH;
    case SP_QUAL:
      if (qual_isMemoryAllocation (cl->squal)) {
	return sRef_showAliasInfo;
      } else if (qual_isSharing (cl->squal)) {
	return sRef_showExpInfo;
      } else if (qual_isIsNull (cl->squal) || qual_isNotNull (cl->squal)) {
	return sRef_showNullInfo;
      } else {
	BADBRANCH;
      }
    }

  BADEXIT;
}

sRefMod stateClause_getEntryFunction (stateClause cl)
{
  if (cl->state == TK_BEFORE || cl->state == TK_BOTH)
    {
      switch (cl->kind)
	{
	case SP_USES:
	  return sRef_setDefinedComplete;
	case SP_ALLOCATES:
	  return sRef_setUndefined; /* evans 2002-01-01 */
	case SP_DEFINES:
	  return sRef_setUndefined; /* evans 2002-01-01 */
	case SP_SETS:
	  return sRef_setAllocatedComplete;
	case SP_RELEASES:
	  return sRef_setDefinedComplete;
	case SP_GLOBAL:
	  BADBRANCH;
	case SP_QUAL:
	  if (qual_isOnly (cl->squal)) {
	    return sRef_setOnly;
	  } else if (qual_isShared (cl->squal)) {
	    return sRef_setShared;
	  } else if (qual_isDependent (cl->squal)) {
	    return sRef_setDependent;
	  } else if (qual_isOwned (cl->squal)) {
	    return sRef_setOwned;
	  } else if (qual_isObserver (cl->squal)) {
	    return sRef_setObserver;
	  } else if (qual_isExposed (cl->squal)) {
	    return sRef_setExposed;
	  } else if (qual_isNotNull (cl->squal)) {
	    return sRef_setNotNull;
	  } else if (qual_isIsNull (cl->squal)) {
	    return sRef_setDefNull;
	  } else {
	    DPRINTF (("Here we are: %s", 
		      qual_unparse (cl->squal)));
	    BADBRANCH;
	  }
	}
      
      BADBRANCH;
    }
  else
    {
      return NULL;
    }

  BADBRANCHNULL;
}

sRefMod stateClause_getEffectFunction (stateClause cl)
{
  if (cl->state == TK_AFTER || cl->state == TK_BOTH)
    {
      switch (cl->kind)
	{
	case SP_USES:
	  return NULL;
	case SP_ALLOCATES:
	  return sRef_setAllocatedComplete;
	case SP_DEFINES:
	  return sRef_setDefinedNCComplete;
	case SP_SETS:
	  return sRef_setDefinedNCComplete;
	case SP_RELEASES:
	  return sRef_killComplete;
	case SP_GLOBAL:
	  BADBRANCH;
	case SP_QUAL:
	  if (qual_isOnly (cl->squal)) {
	    return sRef_setOnly;
	  } else if (qual_isShared (cl->squal)) {
	    return sRef_setShared;
	  } else if (qual_isDependent (cl->squal)) {
	    return sRef_setDependent;
	  } else if (qual_isOwned (cl->squal)) {
	    return sRef_setOwned;
	  } else if (qual_isObserver (cl->squal)) {
	    return sRef_setObserver;
	  } else if (qual_isExposed (cl->squal)) {
	    return sRef_setExposed;
	  } else if (qual_isNotNull (cl->squal)) {
	    return sRef_setNotNull;
	  } else if (qual_isIsNull (cl->squal)) {
	    return sRef_setDefNull;
	  } else {
	    BADBRANCH;
	  }
	}

      BADBRANCH;
    }
  else
    {
      return NULL;
    }

  BADBRANCHNULL;
}

sRefMod stateClause_getReturnEffectFunction (stateClause cl)
{
  if (cl->state == TK_AFTER || cl->state == TK_BOTH)
    {
      switch (cl->kind)
	{
	case SP_USES:
	case SP_ALLOCATES:
	case SP_DEFINES:
	case SP_SETS:
	case SP_RELEASES:
	  return NULL;
	case SP_GLOBAL:
	  BADBRANCH;
	case SP_QUAL:
	  if (qual_isOnly (cl->squal)) {
	    return sRef_killComplete;
	  } else {
	    return NULL;
	  }
	}

      BADBRANCH;
    }
  else
    {
      return NULL;
    }

  BADBRANCHNULL;
}

static flagcode stateClause_qualErrorCode (stateClause cl)
{
  if (qual_isOnly (cl->squal)) {
    return FLG_ONLYTRANS;
  } else if (qual_isShared (cl->squal)) {
    return FLG_SHAREDTRANS;
  } else if (qual_isDependent (cl->squal)) {
    return FLG_DEPENDENTTRANS;
  } else if (qual_isOwned (cl->squal)) {
    return FLG_OWNEDTRANS;
  } else if (qual_isObserver (cl->squal)) {
    return FLG_OBSERVERTRANS;
  } else if (qual_isExposed (cl->squal)) {
    return FLG_EXPOSETRANS;
  } else if (qual_isIsNull (cl->squal)
	     || qual_isNotNull (cl->squal)) {
    return FLG_NULLSTATE;
  } else {
    BADBRANCH;
  }

  BADBRANCHRET (INVALID_FLAG);
}

flagcode stateClause_preErrorCode (stateClause cl)
{
  llassert (cl->state == TK_BOTH || cl->state == TK_BEFORE);

  switch (cl->kind)
    {
    case SP_USES:
      return FLG_USEDEF;
    case SP_ALLOCATES: /*@fallthrough@*/ 
    case SP_DEFINES:
    case SP_SETS:
      return FLG_MUSTFREE;
    case SP_RELEASES:
      return FLG_USEDEF;
    case SP_GLOBAL:
    case SP_QUAL:
      return stateClause_qualErrorCode (cl);
    }

  BADBRANCHRET (INVALID_FLAG);
}

static /*@observer@*/ cstring stateClause_qualErrorString (stateClause cl, sRef sr)
{
  if (qual_isMemoryAllocation (cl->squal)) {
    return alkind_capName (sRef_getAliasKind (sr));
  } else if (qual_isObserver (cl->squal)) {
    return cstring_makeLiteralTemp ("Non-observer");
  } else if (qual_isExposed (cl->squal)) {
    if (sRef_isObserver (sr))
      {
	return cstring_makeLiteralTemp ("Observer");
      }
    else
      {
	return cstring_makeLiteralTemp ("Non-exposed");
      }
  } else if (qual_isNotNull (cl->squal)) {
    if (sRef_isDefinitelyNull (sr))
      {
	return cstring_makeLiteralTemp ("Null");
      }
    else
      {
	return cstring_makeLiteralTemp ("Possibly null");
      }
  } else if (qual_isIsNull (cl->squal)) {
    return cstring_makeLiteralTemp ("Non-null");
  } else {
    BADBRANCH;
  }
  
  BADBRANCHRET (cstring_undefined);
}

cstring stateClause_preErrorString (stateClause cl, sRef sr)
{
  llassert (cl->state == TK_BOTH || cl->state == TK_BEFORE);

  switch (cl->kind)
    {
    case SP_USES:
      if (sRef_isDead (sr)) 
	return cstring_makeLiteralTemp ("Dead");
      else
	return cstring_makeLiteralTemp ("Undefined");
    case SP_ALLOCATES: /*@fallthrough@*/ 
    case SP_DEFINES:
    case SP_SETS:
      return cstring_makeLiteralTemp ("Allocated");
    case SP_RELEASES:
      if (sRef_isDead (sr)) 
	{
	  return cstring_makeLiteralTemp ("Dead");
	}
      else if (sRef_isDependent (sr) 
	       || sRef_isShared (sr))
	{
	  return alkind_unparse (sRef_getAliasKind (sr));
	}
      else if (sRef_isObserver (sr) || sRef_isExposed (sr))
	{
	  return exkind_unparse (sRef_getExKind (sr));
	}
      else
	{
	  return cstring_makeLiteralTemp ("Undefined");
	}
    case SP_GLOBAL:
      BADBRANCH;
    case SP_QUAL:
      return stateClause_qualErrorString (cl, sr);
    }
  
  BADEXIT;
}

flagcode stateClause_postErrorCode (stateClause cl)
{
  llassert (cl->state == TK_BOTH || cl->state == TK_AFTER);

  switch (cl->kind)
    {
    case SP_USES:
      BADBRANCHCONT;
      return INVALID_FLAG;
    case SP_ALLOCATES: 
    case SP_DEFINES:  
    case SP_SETS:     
      return FLG_COMPDEF;
    case SP_RELEASES:
      return FLG_MUSTFREE;
    case SP_GLOBAL:
      BADBRANCH;
    case SP_QUAL:
      return stateClause_qualErrorCode (cl);
    }

  BADBRANCHRET (INVALID_FLAG);
}

cstring stateClause_postErrorString (stateClause cl, sRef sr)
{
  llassert (cl->state == TK_BOTH || cl->state == TK_AFTER);
  
  switch (cl->kind)
    {
    case SP_USES:
      BADBRANCHCONT;
      return cstring_makeLiteralTemp ("<ERROR>");
    case SP_ALLOCATES: 
      return cstring_makeLiteralTemp ("Unallocated");
    case SP_DEFINES:
    case SP_SETS:
      return cstring_makeLiteralTemp ("Undefined");
    case SP_RELEASES:
      return cstring_makeLiteralTemp ("Unreleased");
    case SP_GLOBAL:
      BADBRANCH;
    case SP_QUAL:
      return stateClause_qualErrorString (cl, sr);
    }

  BADEXIT;
}

cstring stateClause_dump (stateClause s)
{
  return (message ("%d.%d.%q.%q",
		   (int) s->state,
		   (int) s->kind,
		   qual_dump (s->squal),
		   sRefSet_dump (s->refs)));
}

stateClause stateClause_undump (char **s)
{
  stateClause ret = (stateClause) dmalloc (sizeof (*ret));

  ret->loc = fileloc_undefined;
  ret->state = (stateConstraint) reader_getInt (s);
  reader_checkChar (s, '.');
  ret->kind = (stateClauseKind) reader_getInt (s);
  reader_checkChar (s, '.');
  ret->squal = qual_undump (s);
  reader_checkChar (s, '.');
  ret->refs = sRefSet_undump (s);

  return ret;
}

stateClause stateClause_copy (stateClause s) 
{
  stateClause ret = (stateClause) dmalloc (sizeof (*ret));
  
  ret->state = s->state;
  ret->kind = s->kind;
  ret->squal = s->squal;
  ret->refs = sRefSet_newCopy (s->refs);
  ret->loc = fileloc_copy (s->loc);

  return ret;
}

bool stateClause_sameKind (stateClause s1, stateClause s2)
{
  return (s1->state == s2->state 
	  && s1->kind == s2->kind
	  && qual_match (s1->squal, s2->squal));
}

void stateClause_free (stateClause s)
{
  sRefSet_free (s->refs);
  fileloc_free (s->loc);
  sfree (s);
}

static /*@observer@*/ cstring 
  stateClauseKind_unparse (stateClause s) 
{
  switch (s->kind)
    {
    case SP_USES: 
      return cstring_makeLiteralTemp ("uses");
    case SP_DEFINES:
      return cstring_makeLiteralTemp ("defines");
    case SP_ALLOCATES:
      return cstring_makeLiteralTemp ("allocates");
    case SP_RELEASES:
      return cstring_makeLiteralTemp ("releases");
    case SP_SETS:
      return cstring_makeLiteralTemp ("sets");
    case SP_GLOBAL:
      return qual_unparse (s->squal);
    case SP_QUAL:
      return qual_unparse (s->squal);
    }

  BADEXIT;
}

cstring stateClause_unparseKind (stateClause s)
{
  return 
    (message ("%s%s",
	      cstring_makeLiteralTemp (s->state == TK_BEFORE 
				       ? "requires "
				       : (s->state == TK_AFTER
					  ? "ensures " : "")),
	      stateClauseKind_unparse (s)));
}

cstring stateClause_unparse (stateClause s)
{
  return (message ("%q %q", 
		   stateClause_unparseKind (s), sRefSet_unparsePlain (s->refs)));
}

stateClause stateClause_createDefines (sRefSet s)
{
  return (stateClause_createRaw (TK_BOTH, SP_DEFINES, s));
}

stateClause stateClause_createUses (sRefSet s)
{
  return (stateClause_createRaw (TK_BOTH, SP_USES, s));
}

stateClause stateClause_createSets (sRefSet s)
{
  return (stateClause_createRaw (TK_BOTH, SP_SETS, s));
}

stateClause stateClause_createReleases (sRefSet s)
{
  return (stateClause_createRaw (TK_BOTH, SP_RELEASES, s));
}

stateClause stateClause_createPlain (lltok tok, sRefSet s)
{
  switch (lltok_getTok (tok))
    {
    case QUSES:
      return stateClause_createUses (s);
    case QDEFINES:
      return stateClause_createDefines (s);
    case QALLOCATES:
      return stateClause_createAllocates (s);
    case QSETS:
      return stateClause_createSets (s);
    case QRELEASES:
      return stateClause_createReleases (s);
    default:
      sRefSet_free (s);
      BADBRANCH;
    }

  BADBRANCHRET (stateClause_createUses (sRefSet_undefined));
}

stateClause stateClause_createAllocates (sRefSet s)
{
  return (stateClause_createRaw (TK_BOTH, SP_ALLOCATES, s));
}

bool stateClause_matchKind (stateClause s1, stateClause s2)
{
  return (s1->state == s2->state && s1->kind == s2->kind
	  && qual_match (s1->squal, s2->squal));
}

bool stateClause_hasEnsures (stateClause cl)
{
  return (cl->state == TK_AFTER && (cl->kind == SP_QUAL || cl->kind == SP_GLOBAL));
}

bool stateClause_hasRequires (stateClause cl)
{
  return (cl->state == TK_BEFORE && (cl->kind == SP_QUAL || cl->kind == SP_GLOBAL));
}

bool stateClause_setsMetaState (stateClause cl)
{
  return ((cl->kind == SP_QUAL || cl->kind == SP_GLOBAL)
	  && qual_isMetaState (cl->squal));
}

qual stateClause_getMetaQual (stateClause cl)
{
  llassert (cl->kind == SP_QUAL || cl->kind == SP_GLOBAL);
  return cl->squal;
}

static sRefModVal stateClause_getStateFunction (stateClause cl)
{
  qual sq;

  llassert (cl->kind == SP_QUAL || cl->kind == SP_GLOBAL);

  sq = cl->squal;

  /*@+enumint@*/

  if (qual_isNullStateQual (sq))
    {
      return (sRefModVal) sRef_setNullState;
    }
  else if (qual_isExQual (sq))
    {
      return (sRefModVal) sRef_setExKind;
    }
  else if (qual_isAliasQual (sq))
    {
      return (sRefModVal) sRef_setAliasKind; /*@i23 complete? @*/
    }
  else
    {
      DPRINTF (("Unhandled ensures qual: %s", qual_unparse (sq)));
      BADBRANCH;
    }
  /*@=enumint@*/
  BADBRANCHRET (NULL);
}

int stateClause_getStateParameter (stateClause cl)
{
  qual sq;

  llassert (cl->kind == SP_QUAL || cl->kind == SP_GLOBAL);

  sq = cl->squal;

  /*@+relaxtypes@*/ /*@i523 this is wrong, remove the enumint@*/
  /*@+enumint@*/

  if (qual_isNotNull (sq))
    {
      return NS_MNOTNULL;
    }
  else if (qual_isIsNull (sq))
    {
      return NS_DEFNULL;
    }
  else if (qual_isNull (sq))
    {
      return NS_POSNULL;
    }
  else if (qual_isRelNull (sq))
    {
      return NS_RELNULL;
    }
  else if (qual_isExposed (sq))
    {
      return XO_EXPOSED;
    }
  else if (qual_isObserver (sq))
    {
      return XO_OBSERVER;
    }
  else if (qual_isAliasQual (sq))
    {
      if (qual_isOnly (sq)) return AK_ONLY;
      if (qual_isImpOnly (sq)) return AK_IMPONLY;
      if (qual_isTemp (sq)) return AK_TEMP;
      if (qual_isOwned (sq)) return AK_OWNED;
      if (qual_isShared (sq)) return AK_SHARED;
      if (qual_isUnique (sq)) return AK_UNIQUE;
      if (qual_isDependent (sq)) return AK_DEPENDENT;
      if (qual_isKeep (sq)) return AK_KEEP;
      if (qual_isKept (sq)) return AK_KEPT;
      BADBRANCH;
    }
  else
    {
      DPRINTF (("Unhandled ensures qual: %s", qual_unparse (sq)));
      BADBRANCH;
    }

  /*@=enumint@*/
  /*@=relaxtypes@*/
  BADBRANCHRET (0);
}

sRefModVal stateClause_getEnsuresFunction (stateClause cl)
{
  llassertprint (cl->state == TK_AFTER, ("Not after: %s", stateClause_unparse (cl)));
  llassert (cl->kind == SP_QUAL || cl->kind == SP_GLOBAL);
  return stateClause_getStateFunction (cl);
}

sRefModVal stateClause_getRequiresBodyFunction (stateClause cl)
{
  llassertprint (cl->state == TK_BEFORE, ("Not before: %s", stateClause_unparse (cl)));
  llassert (cl->kind == SP_QUAL || cl->kind == SP_GLOBAL);
  return stateClause_getStateFunction (cl);
}

/*@observer@*/ fileloc stateClause_loc (stateClause s)
{
  return s->loc;
}
Commit	Line	Data
28bf4b0b	1	/*
11db3170	2	** Splint - annotation-assisted static program checker
77d37419	3	** Copyright (C) 1994-2002 University of Virginia,
28bf4b0b	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
11db3170	22	** For more information: http://www.splint.org
28bf4b0b	23	*/
	24	/*
	25	** stateClause.c
	26	*/
	27
	28	# include "lclintMacros.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
3e3ec469	101	bool stateClause_isQual (stateClause cl)
	102	{
	103	return (cl->kind == SP_QUAL);
	104	}
	105
28bf4b0b	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:
3e3ec469	255	return sRef_setUndefined; /* evans 2002-01-01 */
28bf4b0b	256	case SP_DEFINES:
3e3ec469	257	return sRef_setUndefined; /* evans 2002-01-01 */
28bf4b0b	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
8250fa4a	295	BADBRANCHNULL;
28bf4b0b	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
8250fa4a	345	BADBRANCHNULL;
28bf4b0b	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
8250fa4a	377	BADBRANCHNULL;
28bf4b0b	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	}
8250fa4a	400
8250fa4a	401	BADBRANCHRET (INVALID_FLAG);
28bf4b0b	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_MUSTFREE;
	416	case SP_RELEASES:
	417	return FLG_USEDEF;
	418	case SP_GLOBAL:
	419	case SP_QUAL:
	420	return stateClause_qualErrorCode (cl);
	421	}
	422
8250fa4a	423	BADBRANCHRET (INVALID_FLAG);
28bf4b0b	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
8250fa4a	456	BADBRANCHRET (cstring_undefined);
28bf4b0b	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_MUSTFREE;
	516	case SP_GLOBAL:
	517	BADBRANCH;
	518	case SP_QUAL:
	519	return stateClause_qualErrorCode (cl);
	520	}
521
8250fa4a	522	BADBRANCHRET (INVALID_FLAG);
28bf4b0b	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	}
8250fa4a	681
8250fa4a	682	BADBRANCHRET (stateClause_createUses (sRefSet_undefined));
28bf4b0b	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@/
8250fa4a	746	BADBRANCHRET (NULL);
28bf4b0b	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@/
8250fa4a	805	BADBRANCHRET (0);
28bf4b0b	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