[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;
}
/*end drl added*/

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