[splint.git] / src / stateClause.c

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