[splint.git] / src / stateClause.c

/*
** Splint - annotation-assisted static program checker
** Copyright (C) 1994-2003 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;
}

/*drl added 3/7/2003*/
bool stateClause_hasEmptyReferences (stateClause s)
{
  if (sRefSet_isUndefined(s->refs) )
    return TRUE;
    else
    return FALSE;
}

bool stateClause_isMetaState (stateClause s)
{

  if (qual_isMetaState (s->squal) )
    return TRUE;
  else
    return FALSE;
}

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