[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 splint: info@splint.org
** To report a bug: splint-bug@splint.org
** For more information: http://www.splint.org
*/
/*
** stateClause.c
*/

# include "splintMacros.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.
*/
\r
# ifdef WIN32\r
/* Microsoft doesn't believe in higher order functions... */\r
# pragma warning( disable : 4550 )\r
# endif  \r

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