X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/34f0c5e711b8f61f6376414948f4c116f1c5a22c..51bc6ecce8b6e9877dccd8bda2cf220b47e6929c:/src/sRef.c

diff --git a/src/sRef.c b/src/sRef.c
index d776cc4..b750436 100644
--- a/src/sRef.c
+++ b/src/sRef.c
@@ -1,6 +1,6 @@
 /*
-** LCLint - annotation-assisted static program checker
-** Copyright (C) 1994-2000 University of Virginia,
+** 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
@@ -17,9 +17,9 @@
 ** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston,
 ** MA 02111-1307, USA.
 **
-** For information on lclint: lclint-request@cs.virginia.edu
-** To report a bug: lclint-bug@cs.virginia.edu
-** For more information: http://lclint.cs.virginia.edu
+** For information on splint: info@splint.org
+** To report a bug: splint-bug@splint.org
+** For more information: http://www.splint.org
 */
 /*
 ** storeRef.c
@@ -34,10 +34,10 @@
 **
 */
 
-# include "lclintMacros.nf"
+# include "splintMacros.nf"
 # include "basic.h"
 # include "exprChecks.h"
-# include "aliasChecks.h"
+# include "transferChecks.h"
 # include "sRefTable.h"
 # include "structNames.h"
 
@@ -51,17 +51,18 @@
 /*@notfunction@*/
 # define AND(a,b) (a ? b : (b, FALSE))
 
+static void sRef_checkValidAux (sRef p_s, sRefSet p_checkedsofar) /*@modifies p_checkedsofar@*/ ;
+
 static bool sRef_isDerived (sRef p_s) /*@*/ ;
 
 static /*@exposed@*/ sRef sRef_fixDirectBase (sRef p_s, sRef p_base) 
    /*@modifies p_base@*/ ;
 
+static void sRef_updateNullState (sRef p_res, sRef p_other) /*@modifies p_res@*/ ;
+
 static bool sRef_isAllocatedStorage (sRef p_s) /*@*/ ;
 static void sRef_setNullErrorLoc (sRef p_s, fileloc) /*@*/ ;
-
-static void
-  sRef_aliasSetComplete (void (p_predf) (sRef, fileloc), sRef p_s, fileloc p_loc)
-  /*@modifies p_s@*/ ;
+static void sRef_setNullStateN (sRef p_s, nstate p_n) /*@modifies p_s@*/ ;
 
 static int sRef_depth (sRef p_s) /*@*/ ;
 
@@ -71,21 +72,104 @@ static void
   /*@modifies p_s@*/ ;
 
 static void
-  sRef_innerAliasSetCompleteParam (void (p_predf) (sRef, sRef), sRef p_s, sRef p_t)
-  /*@modifies p_s@*/ ;
-
-static void
-  sRef_aliasSetCompleteParam (void (p_predf) (sRef, alkind, fileloc), sRef p_s, 
-			      alkind p_kind, fileloc p_loc)
-  /*@modifies p_s@*/ ;
-
+sRef_innerAliasSetCompleteParam (void (p_predf) (sRef, sRef), sRef p_s, sRef p_t)
+     /*@modifies p_s@*/ ;
+     
 static speckind speckind_fromInt (int p_i);
 static bool sRef_equivalent (sRef p_s1, sRef p_s2);
 static bool sRef_isDeepUnionField (sRef p_s);
-static void sRef_addDeriv (/*@notnull@*/ sRef p_s, /*@notnull@*/ sRef p_t);
-static sRef sRef_makeResultType (ctype p_ct) /*@*/ ;
+static void sRef_addDeriv (/*@notnull@*/ sRef p_s, /*@notnull@*/ /*@exposed@*/ sRef p_t);
 static bool sRef_checkModify (sRef p_s, sRefSet p_sl) /*@*/ ;
 
+/*
+** If s is definitely null, it has no memory state.
+*/
+
+static void sRef_resetAliasKind (/*@notnull@*/ sRef s) /*@modifies s->aliaskind@*/
+{
+  if (s->nullstate == NS_DEFNULL)
+    {
+      /* s->aliaskind = AK_ERROR; */
+    }
+}
+
+# ifdef DEBUGSPLINT
+extern void sRef_checkCompletelyReasonable (sRef s) /*@*/ 
+{
+  DPRINTF (("Check sRef: [%p] %s / %s", s, sRef_unparse (s),
+	    sRefSet_unparse (sRef_derivedFields (s))));
+
+  if (sRef_isReasonable (s))
+    {
+      sRefSet_elements (s->deriv, el)
+	{
+	  llassert (el != s);
+	  sRef_checkCompletelyReasonable (el);
+	} end_sRefSet_elements ;
+    }
+}
+# endif
+
+/*@falsewhennull@*/ bool sRef_isReasonable (sRef s) /*@*/
+{
+  if (sRef_isValid (s))
+    {
+# ifdef DEBUGSPLINT
+      if (!bool_isReasonable (s->safe)
+	  || !bool_isReasonable (s->modified)
+	  || !bool_isReasonable (s->immut))
+	{
+	  llcontbug (message ("Unreasonable sRef [%p]", s));
+	  return FALSE;
+	}
+
+      if (!sstate_isValid (s->defstate))
+	{
+	  llcontbug (message ("Unreasonable sRef [%p]", s));
+	  return FALSE;
+	}
+
+      if (!nstate_isValid (s->nullstate))
+	{
+	  llcontbug (message ("Unreasonable sRef [%p]", s));
+	  return FALSE;
+	}
+
+      if (!alkind_isValid (s->aliaskind)
+	  || !alkind_isValid (s->oaliaskind))
+	{
+	  llcontbug (message ("Unreasonable sRef [%p]", s));
+	  return FALSE;
+	}
+
+      if (!exkind_isValid (s->expkind)
+	  || !exkind_isValid (s->oexpkind))
+	{
+	  llcontbug (message ("Unreasonable sRef [%p]", s));
+	  return FALSE;
+	}
+# endif
+
+      return TRUE;
+    }
+
+  return FALSE;
+}
+
+static /*@nullwhentrue@*/ bool sRef_isUnreasonable (sRef s) /*@*/
+{
+  return (!sRef_isReasonable (s));
+}
+
+static void sRef_checkMutable (/*@unused@*/ sRef s)
+{
+  if (sRef_isReasonable (s) && s->immut)
+    {
+      llcontbug (message ("Modification to sRef marked immutable: %q", 
+			  sRef_unparseFull (s)));
+    }
+}
+
 static bool skind_isSimple (skind sk)
 {
   switch (sk)
@@ -105,8 +189,9 @@ static void sinfo_free (/*@special@*/ /*@temp@*/ /*@notnull@*/ sRef p_s)
 static /*@null@*/ sinfo sinfo_copy (/*@notnull@*/ sRef p_s) /*@*/ ;
 static void sRef_setPartsFromUentry (sRef p_s, uentry p_ue)
    /*@modifies p_s@*/ ;
-static bool checkDeadState (/*@notnull@*/ sRef p_el, bool p_tbranch, fileloc p_loc);
-static sRef sRef_constructPointerAux (/*@notnull@*/ /*@exposed@*/ sRef p_t) /*@*/ ;
+static bool checkDeadState (/*@notnull@*/ sRef p_el, /*@null@*/ sRef p_e2, 
+			    bool p_tbranch, fileloc p_loc);
+static /*@dependent@*/ sRef sRef_constructPointerAux (/*@notnull@*/ /*@exposed@*/ sRef p_t) /*@*/ ;
 
 static void 
   sRef_combineExKinds (/*@notnull@*/ sRef p_res, /*@notnull@*/ sRef p_other)
@@ -131,7 +216,6 @@ static void sRef_setStateFromAbstractUentry (sRef p_s, uentry p_ue)
 static void 
   sinfo_update (/*@notnull@*/ /*@exposed@*/ sRef p_res, 
 		/*@notnull@*/ /*@exposed@*/ sRef p_other);
-static /*@only@*/ alinfo alinfo_makeRefLoc (/*@exposed@*/ sRef p_ref, fileloc p_loc);
 static void sRef_setDefinedAux (sRef p_s, fileloc p_loc, bool p_clear)
    /*@modifies p_s@*/ ;
 static void sRef_setDefinedNoClear (sRef p_s, fileloc p_loc)
@@ -170,6 +254,7 @@ static /*@only@*/ cstring sRef_unparseWithArgs (sRef p_s, uentryList p_args);
 static /*@only@*/ cstring sRef_unparseNoArgs (sRef p_s);
 
 static /*@exposed@*/ sRef sRef_findDerivedPointer (sRef p_s);
+static /*@exposed@*/ sRef sRef_findDerivedArrayFetch (/*@notnull@*/ sRef, bool, int, bool) ;
 static /*@exposed@*/ sRef sRef_findDerivedField (/*@notnull@*/ sRef p_rec, cstring p_f);
 static /*@exposed@*/ sRef
   sRef_getDeriv (/*@notnull@*/ /*@returned@*/ sRef p_set, sRef p_guide);
@@ -187,13 +272,209 @@ static ntotrefers = 0;
 static nrefers = 0;
 # endif
 
-/*@constant null alinfo alinfo_undefined; @*/
-# define alinfo_undefined ((alinfo) NULL)
+static /*@checked@*/ bool protectDerivs = FALSE;
 
-static /*@only@*/ /*@notnull@*/ alinfo alinfo_makeLoc (fileloc p_loc);
-static /*@only@*/ alinfo alinfo_copy (alinfo p_a);
+/*
+** Result of sRef_alloc is dependent since allRefs may
+** reference it.  It is only if !inFunction.
+*/
+
+static /*@dependent@*/ /*@out@*/ /*@notnull@*/ sRef
+sRef_alloc (void)
+{
+  sRef s = (sRef) dmalloc (sizeof (*s));
+
+  s->immut = FALSE;
+
+  DPRINTF (("Alloc sref: [%p]", s));
+
+  if (inFunction)
+    {
+      allRefs = sRefTable_add (allRefs, s);
+      /*@-branchstate@*/ 
+    }
+  else
+    {
+      DPRINTF (("Not in function!"));
+    }
+
+  /*@=branchstate@*/
+
+# ifdef DEBUGREFS
+  if (nsrefs >= maxnsrefs)
+    {
+      maxnsrefs = nsrefs;
+    }
+
+  totnsrefs++;
+  nsrefs++;
+# endif
+
+  /*@-mustfree@*/ /*@-freshtrans@*/
+  return s;
+  /*@=mustfree@*/ /*@=freshtrans@*/
+}
+
+static void sRef_checkValidAux (sRef s, sRefSet checkedsofar)
+{
+  llassert (FALSE);
+
+  if (!sRef_isReasonable (s)) return;
+
+  if (sRefSet_containsSameObject (checkedsofar, s))
+    {
+      return;
+    }
+
+  /*@-temptrans@*/
+  checkedsofar = sRefSet_insert (checkedsofar, s);
+  /*@=temptrans@*/ /* checksofar will be destroyed before checkValid returns */
+
+  switch (s->kind)
+    {
+    case SK_UNCONSTRAINED:
+      llassert (cstring_length (s->info->fname) < 100);
+      break;
+
+    case SK_CVAR:
+      llassert (s->info->cvar->lexlevel >= 0);
+      /* llassert (s->info->cvar->lexlevel <= usymtab_getCurrentDepth ()); */
+      break;
+
+    case SK_PARAM:
+      llassert (s->info->paramno >= -1);
+      llassert (s->info->paramno <= 999); /* sanity check */
+      break;
+
+    case SK_ARRAYFETCH:
+      sRef_checkValidAux (s->info->arrayfetch->arr, checkedsofar);
+      break;
+
+    case SK_FIELD:
+      sRef_checkValidAux (s->info->field->rec, checkedsofar);
+      llassert (cstring_length (s->info->field->field) < 100);
+      break;
+
+    case SK_PTR:
+      sRef_checkValidAux (s->info->ref, checkedsofar);
+      break;
+ 
+   case SK_ADR:
+      sRef_checkValidAux (s->info->ref, checkedsofar);
+      break;
+
+    case SK_OBJECT:
+      /* check ctype s->info->object */
+      break;
+
+    case SK_CONJ:
+      sRef_checkValidAux (s->info->conj->a, checkedsofar);
+      sRef_checkValidAux (s->info->conj->b, checkedsofar);
+      break;
+
+    case SK_NEW:
+      llassert (cstring_length (s->info->fname) < 100);
+      break;
+
+    case SK_DERIVED:
+      sRef_checkValidAux (s->info->ref, checkedsofar);
+      break;
+
+    case SK_EXTERNAL:
+      sRef_checkValidAux (s->info->ref, checkedsofar);
+      break;
+
+    case SK_TYPE:
+    case SK_CONST:
+    case SK_RESULT:
+      /* check ctyp s->type */
+      break;
+
+    case SK_SPECIAL:
+      llassert (s->info->spec == SR_NOTHING 
+		|| s->info->spec == SR_INTERNAL
+		|| s->info->spec == SR_SPECSTATE 
+		|| s->info->spec == SR_SYSTEM);
+      break;
+
+    case SK_UNKNOWN:
+      break;
+
+      BADDEFAULT;
+    }
+  
+
+  sRefSet_elements (s->deriv, el)
+    {
+      sRef_checkValidAux (el, checkedsofar);
+    } end_sRefSet_elements ;
+}
+
+void sRef_checkValid (/*@unused@*/ sRef s)
+{
+  return;
+  /*
+  sRefSet checkedsofar = sRefSet_new ();
+  sRef_checkValidAux (s, checkedsofar);
+  */
+}
+
+static /*@dependent@*/ /*@notnull@*/ /*@special@*/ sRef
+  sRef_new (void)
+  /*@defines result@*/
+  /*@ensures isnull result->aliasinfo, result->definfo,
+                    result->expinfo, result->info, result->deriv, result->state@*/
+{
+  sRef s = sRef_alloc ();
+
+  s->kind = SK_UNKNOWN;
+  s->safe = TRUE;
+  s->modified = FALSE;
+  s->immut = FALSE;
+  s->val = multiVal_undefined;
+
+  s->type = ctype_unknown;
+  s->defstate = SS_UNKNOWN;
+
+  /* start modifications */
+  s->bufinfo.bufstate = BB_NOTNULLTERMINATED;
+  s->bufinfo.size = -1; 
+  s->bufinfo.len = -1; 
+  /* end modifications */
+
+  s->aliaskind = AK_UNKNOWN;
+  s->oaliaskind = AK_UNKNOWN;
+
+  s->nullstate = NS_UNKNOWN;
+
+  s->expkind = XO_UNKNOWN;
+  s->oexpkind = XO_UNKNOWN;
+
+  s->aliasinfo = stateInfo_undefined;
+  s->definfo = stateInfo_undefined;
+  s->nullinfo = stateInfo_undefined;
+  s->expinfo = stateInfo_undefined;
+
+  s->info = NULL;
+  s->deriv = sRefSet_undefined;
+
+  s->state = valueTable_undefined;
+
+  return s;
+}
+
+static /*@dependent@*/ /*@notnull@*/ /*@special@*/ sRef
+  sRef_newRef (void)
+  /*@defines result@*/
+  /*@ensures isnull result->aliasinfo, result->definfo,
+                    result->expinfo, result->info, result->deriv@*/
+{
+  sRef res = sRef_new ();
+  res->immut = FALSE;
+  res->state = valueTable_undefined;
+  return res;
+}
 
-static /*@checked@*/ bool protectDerivs = FALSE;
 
 void sRef_protectDerivs (void) /*@modifies protectDerivs@*/
 {
@@ -225,7 +506,7 @@ sRef_isRecursiveField (sRef s)
 	  fieldname = sRef_getField (s);
 	  base = sRef_getBase (s);
 	  
-	  while (sRef_isValid (base))
+	  while (sRef_isReasonable (base))
 	    {
 	      if (sRef_isField (base))
 		{
@@ -244,12 +525,12 @@ sRef_isRecursiveField (sRef s)
 }
 
 static void
-sRef_addDeriv (/*@notnull@*/ sRef s, /*@notnull@*/ sRef t)
+sRef_addDeriv (/*@notnull@*/ sRef s, /*@notnull@*/ /*@exposed@*/ sRef t)
 {
   if (!context_inProtectVars () 
       && !protectDerivs
-      && sRef_isValid (s)
-      && sRef_isValid (t)
+      && sRef_isReasonable (s)
+      && sRef_isReasonable (t)
       && !sRef_isConst (s))
     {
       int sd = sRef_depth (s);
@@ -260,7 +541,17 @@ sRef_addDeriv (/*@notnull@*/ sRef s, /*@notnull@*/ sRef t)
 	  return;
 	}
 
-      if (sRef_isGlobal (s))
+      /* This sometimes fails: (evans 2001-07-12)
+      if (sRef_isArrayFetch (t))
+	{
+	  DPRINTF (("Derived fetch: %s / %s / %s",
+		    sRef_unparseFull (s), sRef_unparseFull (t),
+		    sRef_unparseFull (t->info->arrayfetch->arr)));
+	  llassert (t->info->arrayfetch->arr == s);
+	}
+      */
+
+      if (sRef_isFileOrGlobalScope (s))
 	{
 	  if (context_inFunctionLike () 
 	      && ctype_isKnown (sRef_getType (s))
@@ -284,12 +575,20 @@ sRef_addDeriv (/*@notnull@*/ sRef s, /*@notnull@*/ sRef t)
 		}
 	      else
 		{
+		  DPRINTF (("Add deriv: [%p] %s / [%p] %s",
+			    s, sRef_unparse (s),
+			    t, sRef_unparse (t)));
+		  
 		  s->deriv = sRefSet_insert (s->deriv, t);
 		}
 	    }
 	}
       else
 	{
+	  DPRINTF (("Add deriv: [%p] %s / [%p] %s",
+		    s, sRef_unparse (s),
+		    t, sRef_unparse (t)));
+
 	  s->deriv = sRefSet_insert (s->deriv, t);
 	}
     }
@@ -298,11 +597,11 @@ sRef_addDeriv (/*@notnull@*/ sRef s, /*@notnull@*/ sRef t)
 bool
 sRef_deepPred (bool (predf) (sRef), sRef s)
 {
-  if (sRef_isValid (s))
+  if (sRef_isReasonable (s))
     {
       if ((*predf)(s)) return TRUE;
 
-      switch  (s->kind)
+      switch (s->kind)
 	{
 	case SK_PTR:
 	  return (sRef_deepPred (predf, s->info->ref));
@@ -328,15 +627,17 @@ bool sRef_modInFunction (void)
 
 void sRef_setStateFromType (sRef s, ctype ct)
 {
-  if (sRef_isValid (s))
+  if (sRef_isReasonable (s))
     {
       if (ctype_isUser (ct))
 	{
+	  DPRINTF (("Here we are: %s", sRef_unparseFull (s)));
 	  sRef_setStateFromUentry 
 	    (s, usymtab_getTypeEntry (ctype_typeId (ct)));
 	}
       else if (ctype_isAbstract (ct))
 	{
+	  DPRINTF (("Here we are: %s", sRef_unparseFull (s)));
 	  sRef_setStateFromAbstractUentry 
 	    (s, usymtab_getTypeEntry (ctype_typeId (ct)));
 	}
@@ -349,138 +650,68 @@ void sRef_setStateFromType (sRef s, ctype ct)
 
 static void sRef_setTypeState (sRef s)
 {
-  if (sRef_isValid (s))
+  if (sRef_isReasonable (s))
     {
       sRef_setStateFromType (s, s->type);
     }
 }
 
-static void alinfo_free (/*@only@*/ alinfo a)
-{
-  if (a != NULL)
-    {
-      fileloc_free (a->loc);
-      sfree (a);
-    }
-}
-
-static /*@only@*/ alinfo alinfo_update (/*@only@*/ alinfo old, alinfo newinfo)
-/*
-** returns an alinfo with the same value as new.  May reuse the
-** storage of old.  (i.e., same effect as copy, but more
-** efficient.)
-*/
+bool sRef_hasAliasInfoLoc (sRef s)
 {
-  if (old == NULL) 
-    {
-      old = alinfo_copy (newinfo);
-    }
-  else if (newinfo == NULL)
-    {
-      alinfo_free (old);
-      return NULL;
-    }
-  else
-    {
-      old->loc = fileloc_update (old->loc, newinfo->loc);
-      old->ref = newinfo->ref;
-      old->ue = newinfo->ue;
-    }
-
-  return old;
+  return (sRef_isReasonable (s) && (s->aliasinfo != NULL)
+	  && (fileloc_isDefined (s->aliasinfo->loc)));
 }
 
-static /*@only@*/ alinfo alinfo_updateLoc (/*@only@*/ alinfo old, fileloc loc)
+/*@falsewhennull@*/ bool sRef_hasStateInfoLoc (sRef s)
 {
-  if (old == NULL) 
-    {
-      old = alinfo_makeLoc (loc);
-    }
-  else
-    {
-      old->loc = fileloc_update (old->loc, loc);
-      old->ue = uentry_undefined;
-      old->ref = sRef_undefined;
-    }
-
-  return old;
+  return (sRef_isReasonable (s) && (s->definfo != NULL) 
+	  && (fileloc_isDefined (s->definfo->loc)));
 }
 
-static /*@only@*/ alinfo 
-  alinfo_updateRefLoc (/*@only@*/ alinfo old, /*@dependent@*/ sRef ref, fileloc loc)
+/*@falsewhennull@*/ bool sRef_hasExpInfoLoc (sRef s)
 {
-  if (old == NULL) 
-    {
-      old = alinfo_makeRefLoc (ref, loc);
-    }
-  else
-    {
-      old->loc = fileloc_update (old->loc, loc);
-      old->ue = uentry_undefined;
-      old->ref = ref;
-    }
-
-  return old;
+  return (sRef_isReasonable (s) 
+	  && (s->expinfo != NULL) && (fileloc_isDefined (s->expinfo->loc)));
 }
 
-static /*@only@*/ alinfo
-alinfo_copy (alinfo a)
+# if 0
+static /*@observer@*/ /*@unused@*/ stateInfo sRef_getInfo (sRef s, cstring key)
 {
-  if (a == NULL)
-    {
-      return NULL;
-    }
-  else
+  stateValue sv;
+  
+  if (!sRef_isReasonable (s)) {
+    return stateInfo_undefined;
+  }
+  
+  sv = valueTable_lookup (s->state, key);
+  
+  if (stateValue_isDefined (sv)) 
     {
-      alinfo ret = (alinfo) dmalloc (sizeof (*ret));
-      
-      ret->loc = fileloc_copy (a->loc); /*< should report bug without copy! >*/
-      ret->ue = a->ue;
-      ret->ref = a->ref;
-
-      return ret;
+      return stateValue_getInfo (sv);
     }
+  
+  return stateInfo_undefined;
 }
-
-static bool
-  sRef_hasAliasInfoLoc (sRef s)
-{
-  return (sRef_isValid (s) && (s->aliasinfo != NULL)
-	  && (fileloc_isDefined (s->aliasinfo->loc)));
-}
-
-static /*@falsenull@*/ bool
-sRef_hasStateInfoLoc (sRef s)
-{
-  return (sRef_isValid (s) && (s->definfo != NULL) 
-	  && (fileloc_isDefined (s->definfo->loc)));
-}
-
-static /*@falsenull@*/ bool
-sRef_hasExpInfoLoc (sRef s)
-{
-  return (sRef_isValid (s) 
-	  && (s->expinfo != NULL) && (fileloc_isDefined (s->expinfo->loc)));
-}
+# endif
 
 static bool
 sRef_hasNullInfoLoc (sRef s)
 {
-  return (sRef_isValid (s) && (s->nullinfo != NULL) 
+  return (sRef_isReasonable (s) && s->nullinfo != NULL
 	  && (fileloc_isDefined (s->nullinfo->loc)));
 }
 
 bool
 sRef_hasAliasInfoRef (sRef s)
 {
-  return (sRef_isValid (s) && (s->aliasinfo != NULL) 
-	  && (sRef_isValid (s->aliasinfo->ref)));
+  return (sRef_isReasonable (s) && (s->aliasinfo != NULL) 
+	  && (sRef_isReasonable (s->aliasinfo->ref)));
 }
 
 static /*@observer@*/ fileloc
 sRef_getAliasInfoLoc (/*@exposed@*/ sRef s)
 {
-  llassert (sRef_isValid (s) && s->aliasinfo != NULL
+  llassert (sRef_isReasonable (s) && s->aliasinfo != NULL
 	    && (fileloc_isDefined (s->aliasinfo->loc)));
   return (s->aliasinfo->loc);
 }
@@ -488,7 +719,7 @@ sRef_getAliasInfoLoc (/*@exposed@*/ sRef s)
 static /*@observer@*/ fileloc
 sRef_getStateInfoLoc (/*@exposed@*/ sRef s)
 {
-  llassert (sRef_isValid (s) && s->definfo != NULL 
+  llassert (sRef_isReasonable (s) && s->definfo != NULL 
 	    && (fileloc_isDefined (s->definfo->loc)));
   return (s->definfo->loc);
 }
@@ -496,7 +727,7 @@ sRef_getStateInfoLoc (/*@exposed@*/ sRef s)
 static /*@observer@*/ fileloc
 sRef_getExpInfoLoc (/*@exposed@*/ sRef s)
 {
-  llassert (sRef_isValid (s) && s->expinfo != NULL 
+  llassert (sRef_isReasonable (s) && s->expinfo != NULL 
 	    && (fileloc_isDefined (s->expinfo->loc)));
   return (s->expinfo->loc);
 }
@@ -504,40 +735,21 @@ sRef_getExpInfoLoc (/*@exposed@*/ sRef s)
 static /*@observer@*/ fileloc
 sRef_getNullInfoLoc (/*@exposed@*/ sRef s)
 {
-  llassert (sRef_isValid (s) && s->nullinfo != NULL 
+  llassert (sRef_isReasonable (s) && s->nullinfo != NULL 
 	    && (fileloc_isDefined (s->nullinfo->loc)));
   return (s->nullinfo->loc);
 }
 
 /*@observer@*/ sRef
-  sRef_getAliasInfoRef (/*@exposed@*/ sRef s)
+  sRef_getAliasInfoRef (/*@temp@*/ sRef s)
 {
-  llassert (sRef_isValid (s) && s->aliasinfo != NULL);
+  llassert (sRef_isReasonable (s) && s->aliasinfo != NULL);
   return (s->aliasinfo->ref);
 }
 
-static /*@only@*/ /*@notnull@*/ alinfo
-alinfo_makeLoc (fileloc loc)
+bool sRef_inGlobalScope ()
 {
-  alinfo ret = (alinfo) dmalloc (sizeof (*ret));
-
-  ret->loc = fileloc_copy (loc); /* don't need to copy! */
-  ret->ue = uentry_undefined;
-  ret->ref = sRef_undefined;
-  
-  return ret;
-}
-
-static /*@only@*/ alinfo
-alinfo_makeRefLoc (/*@exposed@*/ sRef ref, fileloc loc)
-{
-  alinfo ret = (alinfo) dmalloc (sizeof (*ret));
-
-  ret->loc = fileloc_copy (loc);
-  ret->ref = ref;
-  ret->ue  = uentry_undefined;
-  
-  return ret;
+  return !inFunction;
 }
 
 /*
@@ -549,41 +761,68 @@ alinfo_makeRefLoc (/*@exposed@*/ sRef ref, fileloc loc)
 void sRef_setGlobalScope ()
 {
   llassert (inFunction);
+  DPRINTF (("leave function"));
   inFunction = FALSE;
 }
 
 void sRef_clearGlobalScope ()
 {
   llassert (!inFunction);
+  DPRINTF (("enter function"));
   inFunction = TRUE;
 }
 
 static bool oldInFunction = FALSE;
+static int nestedScope = 0;
 
 void sRef_setGlobalScopeSafe ()
 {
-    oldInFunction = inFunction;
+  if (nestedScope == 0)
+    {
+      oldInFunction = inFunction;
+    }
+  
+  nestedScope++;
+  DPRINTF (("leave function safe"));
   inFunction = FALSE;
 }
 
 void sRef_clearGlobalScopeSafe ()
 {
-    inFunction = oldInFunction;
+  nestedScope--;
+  llassert (nestedScope >= 0);
+  
+  if (nestedScope == 0)
+    {
+      inFunction = oldInFunction;
+    }
+
+  DPRINTF (("clear function: %s", bool_unparse (inFunction)));
 }
 
 void sRef_enterFunctionScope ()
 {
+  /* evans 2001-09-09 - cleanup if we are in a macro! */
+  if (context_inMacro ())
+    {
+      if (inFunction) {
+	sRef_exitFunctionScope ();
+      }
+    }
+
   llassert (!inFunction);
   llassert (sRefTable_isEmpty (allRefs));
   inFunction = TRUE;
+  DPRINTF (("enter function"));
 }
 
 void sRef_exitFunctionScope ()
-{
-  
+{  
   if (inFunction)
     {
+      DPRINTF (("Exit function scope."));
       sRefTable_clear (allRefs);
+      DPRINTF (("Exit function scope done."));
       inFunction = FALSE;
     }
   else
@@ -601,74 +840,6 @@ void sRef_destroyMod () /*@globals killed allRefs;@*/
   sRefTable_free (allRefs);
 }
 
-/*
-** Result of sRef_alloc is dependent since allRefs may
-** reference it.  It is only if !inFunction.
-*/
-
-static /*@dependent@*/ /*@out@*/ /*@notnull@*/ sRef
-sRef_alloc (void)
-{
-  sRef s = (sRef) dmalloc (sizeof (*s));
-
-  if (inFunction)
-    {
-      allRefs = sRefTable_add (allRefs, s);
-      /*@-branchstate@*/ 
-    } 
-  /*@=branchstate@*/
-
-# ifdef DEBUGREFS
-  if (nsrefs >= maxnsrefs)
-    {
-      maxnsrefs = nsrefs;
-    }
-
-  totnsrefs++;
-  nsrefs++;
-# endif
-
-  /*@-mustfree@*/ /*@-freshtrans@*/
-  return s;
-  /*@=mustfree@*/ /*@=freshtrans@*/
-}
-
-static /*@dependent@*/ /*@notnull@*/ /*@special@*/ sRef
-  sRef_new (void)
-  /*@defines result@*/
-  /*@post:isnull result->aliasinfo, result->definfo, result->nullinfo, 
-                 result->expinfo, result->info, result->deriv@*/
-{
-  sRef s = sRef_alloc ();
-
-  s->kind = SK_UNKNOWN;
-  s->safe = TRUE;
-  s->modified = FALSE;
-  s->type = ctype_unknown;
-  s->defstate = SS_UNKNOWN;
-
-  /* start modifications */
-  s->bufinfo.bufstate = BB_NOTNULLTERMINATED;
-  /* end modifications */
-
-  s->aliaskind = AK_UNKNOWN;
-  s->oaliaskind = AK_UNKNOWN;
-
-  s->nullstate = NS_UNKNOWN;
-
-  s->expkind = XO_UNKNOWN;
-  s->oexpkind = XO_UNKNOWN;
-
-  s->aliasinfo = alinfo_undefined;
-  s->definfo = alinfo_undefined;
-  s->nullinfo = alinfo_undefined;
-  s->expinfo = alinfo_undefined;
-
-  s->info = NULL;
-  s->deriv = sRefSet_undefined;
-
-  return s;
-}
 
 static /*@notnull@*/ /*@exposed@*/ sRef
 sRef_fixConj (/*@notnull@*/ sRef s)
@@ -679,7 +850,7 @@ sRef_fixConj (/*@notnull@*/ sRef s)
 	s = sRef_getConjA (s);
       } while (sRef_isConj (s));
       
-      llassert (sRef_isValid (s));
+      llassert (sRef_isReasonable (s));
       return s; /* don't need to ref */
     }
   else
@@ -694,9 +865,9 @@ sRef_isExternallyVisibleAux (sRef s)
   bool res = FALSE;
   sRef base = sRef_getRootBase (s);
 
-  if (sRef_isValid (base))
+  if (sRef_isReasonable (base))
     {
-      res = sRef_isParam (base) || sRef_isGlobal (base) || sRef_isExternal (base);
+      res = sRef_isParam (base) || sRef_isFileOrGlobalScope (base) || sRef_isExternal (base);
     }
 
   return res;
@@ -714,12 +885,12 @@ sRef_getBaseUentry (sRef s)
   sRef base = sRef_getRootBase (s);
   uentry res = uentry_undefined;
   
-  if (sRef_isValid (base))
+  if (sRef_isReasonable (base))
     {
       switch (base->kind)
 	{
 	case SK_PARAM:
-	  res = usymtab_getRefQuiet (paramsScope, base->info->paramno);
+	  res = usymtab_getRefQuiet (paramsScope, usymId_fromInt (base->info->paramno));
 	  break;
 
 	case SK_CVAR:
@@ -747,8 +918,7 @@ sRef_updateSref (sRef s)
   sRef ret;
   sRef res;
 
-  if (!sRef_isValid (s)) return sRef_undefined;
-
+  if (!sRef_isReasonable (s)) return sRef_undefined;
   
   switch (s->kind)
     {
@@ -756,13 +926,25 @@ sRef_updateSref (sRef s)
     case SK_OBJECT:
     case SK_NEW:
     case SK_TYPE:
-    case SK_EXTERNAL:
     case SK_DERIVED:
     case SK_UNCONSTRAINED:
     case SK_CONST:
     case SK_SPECIAL:
     case SK_RESULT:
       return s; 
+    case SK_EXTERNAL:
+      {
+	sRef r = sRef_updateSref (s->info->ref);
+
+	if (r != s->info->ref)
+	  {
+	    return sRef_makeExternal (r);
+	  }
+	else
+	  {
+	    return s;
+	  }
+      }
     case SK_PARAM:
     case SK_CVAR:
       {
@@ -773,11 +955,12 @@ sRef_updateSref (sRef s)
 	
 	if (uentry_isUndefined (ue))
 	  {
-	    	    return s;
+	    return s;
 	  }
 	else
 	  {
-	    	    return (uentry_getSref (ue));
+	    DPRINTF (("Update sref: %s", uentry_unparseFull (ue)));
+	    return (uentry_getSref (ue));
 	  }
       }
     case SK_ARRAYFETCH:
@@ -865,12 +1048,12 @@ sRef_updateSref (sRef s)
 uentry
 sRef_getUentry (sRef s)
 {
-  llassert (sRef_isValid (s));
+  llassert (sRef_isReasonable (s));
 
   switch (s->kind)
     {
     case SK_PARAM:
-      return (usymtab_getRefQuiet (paramsScope, s->info->paramno));
+      return (usymtab_getRefQuiet (paramsScope, usymId_fromInt (s->info->paramno)));
     case SK_CVAR:
       return (usymtab_getRefQuiet (s->info->cvar->lexlevel, s->info->cvar->index));
     case SK_CONJ:
@@ -885,6 +1068,7 @@ sRef_getUentry (sRef s)
 	    return sRef_getUentry (s->info->conj->b);
 	  }
       }
+    case SK_FIELD: /* evans 2002-07-17: added case for SK_FIELD */
     case SK_UNKNOWN:
     case SK_SPECIAL:
       return uentry_undefined;
@@ -895,7 +1079,7 @@ sRef_getUentry (sRef s)
 int
 sRef_getParam (sRef s)
 {
-  llassert (sRef_isValid (s));
+  llassert (sRef_isReasonable (s));
   llassert (s->kind == SK_PARAM);
 
   return s->info->paramno;
@@ -904,12 +1088,12 @@ sRef_getParam (sRef s)
 bool
 sRef_isModified (sRef s)
 {
-    return (!sRef_isValid (s) || s->modified);
+    return (!sRef_isReasonable (s) || s->modified);
 }
 
 void sRef_setModified (sRef s)
 {
-  if (sRef_isValid (s))
+  if (sRef_isReasonable (s))
     {
       s->modified = TRUE;
 
@@ -917,23 +1101,20 @@ void sRef_setModified (sRef s)
       if (sRef_isRefsField (s))
 	{
 	  sRef base = sRef_getBase (s);
-
 	  
 	  llassert (s->kind == SK_FIELD);
-
 	  
 	  if (sRef_isPointer (base))
 	    {
 	      base = sRef_getBase (base);
-	      	    }
-
+	    }
+	  
 	  if (sRef_isRefCounted (base))
 	    {
 	      base->aliaskind = AK_NEWREF;
-	      	    }
+	    }
 	}
-
-          }
+    }
 }
 
 /*
@@ -957,7 +1138,6 @@ sRef_canModifyVal (sRef s, sRefSet sl)
 bool
 sRef_canModify (sRef s, sRefSet sl)
 {
-  
   if (context_getFlag (FLG_MUSTMOD))
     {
       return (sRef_doModify (s, sl));
@@ -975,6 +1155,8 @@ sRef_canModify (sRef s, sRefSet sl)
 static
 bool sRef_checkModifyVal (sRef s, sRefSet sl)
 {
+  DPRINTF (("Check modify val: %s", sRef_unparse (s)));
+
   if (sRef_isInvalid (s))
     {
       return TRUE;
@@ -986,7 +1168,9 @@ bool sRef_checkModifyVal (sRef s, sRefSet sl)
     case SK_CONST:
       return TRUE;
     case SK_CVAR:
-      if (sRef_isGlobal (s))
+      DPRINTF (("Modify var: %s", sRef_unparse (s)));
+
+      if (sRef_isFileOrGlobalScope (s))
 	{
 	  if (context_checkGlobMod (s))
 	    {
@@ -1039,6 +1223,7 @@ bool sRef_checkModifyVal (sRef s, sRefSet sl)
 	      }
 	  case SR_SPECSTATE: return TRUE;
 	  case SR_SYSTEM:    return (sRefSet_member (sl, s));
+	  case SR_GLOBALMARKER: BADBRANCH;
 	  }
       }
     case SK_RESULT: BADBRANCH;
@@ -1054,7 +1239,7 @@ bool sRef_checkModifyVal (sRef s, sRefSet sl)
 
 static bool sRef_checkModify (sRef s, sRefSet sl)
 {
-  llassert (sRef_isValid (s));
+  llassert (sRef_isReasonable (s));
 
   switch (s->kind)
     {
@@ -1062,7 +1247,7 @@ static bool sRef_checkModify (sRef s, sRefSet sl)
     case SK_CONST:
       return TRUE;
     case SK_CVAR:
-      if (sRef_isGlobal (s))
+      if (sRef_isFileOrGlobalScope (s))
 	{
 	  if (context_checkGlobMod (s))
 	    {
@@ -1128,6 +1313,7 @@ static bool sRef_checkModify (sRef s, sRefSet sl)
 	      }
 	  case SR_SPECSTATE: return TRUE;
 	  case SR_SYSTEM:    return (sRefSet_member (sl, s));
+	  case SR_GLOBALMARKER: BADBRANCH;
 	  }
       }
     case SK_RESULT: BADBRANCH;
@@ -1178,7 +1364,7 @@ cstring sRef_stateAltVerb (sRef s)
 static 
 bool sRef_doModifyVal (sRef s, sRefSet sl)
 {
-  llassert (sRef_isValid (s));
+  llassert (sRef_isReasonable (s));
 
   
   switch (s->kind)
@@ -1187,7 +1373,7 @@ bool sRef_doModifyVal (sRef s, sRefSet sl)
     case SK_CONST:
       return TRUE;
     case SK_CVAR:
-      if (sRef_isGlobal (s))
+      if (sRef_isFileOrGlobalScope (s))
 	{
 	  
 	  if (context_checkGlobMod (s))
@@ -1247,14 +1433,10 @@ bool sRef_doModifyVal (sRef s, sRefSet sl)
 		(void) sRefSet_modifyMember (sl, s);
 		return TRUE;
 	      }
-	  case SR_SPECSTATE: 
-	    {
-	      return TRUE;
-	    }
-	  case SR_SYSTEM:
-	    {
-	      return (sRefSet_modifyMember (sl, s));
-	    }
+	  case SR_SPECSTATE: return TRUE;
+	  case SR_SYSTEM:    return (sRefSet_modifyMember (sl, s));
+	  case SR_GLOBALMARKER: BADBRANCH;
+
 	  }
       }
     case SK_RESULT: BADBRANCH;
@@ -1271,7 +1453,7 @@ bool sRef_doModifyVal (sRef s, sRefSet sl)
 static 
 bool sRef_doModify (sRef s, sRefSet sl)
 {
-    llassert (sRef_isValid (s));
+  llassert (sRef_isReasonable (s));
   
   switch (s->kind)
     {
@@ -1279,7 +1461,7 @@ bool sRef_doModify (sRef s, sRefSet sl)
     case SK_CONST:
       return TRUE;
     case SK_CVAR:
-      if (sRef_isGlobal (s))
+      if (sRef_isFileOrGlobalScope (s))
 	{
 	  if (context_checkGlobMod (s))
 	    {
@@ -1340,6 +1522,7 @@ bool sRef_doModify (sRef s, sRefSet sl)
 	  case SR_INTERNAL:  return TRUE;
 	  case SR_SPECSTATE: return TRUE;
 	  case SR_SYSTEM:    return (sRefSet_modifyMember (sl, s));
+	  case SR_GLOBALMARKER: BADBRANCH;
 	  }
       }
     case SK_RESULT: BADBRANCH;
@@ -1352,8 +1535,8 @@ static /*@exposed@*/ sRef
 {
   llassert (sRef_similar (s1, s2));
   
-  if (!sRef_isValid (s1)) return s1;
-  if (!sRef_isValid (s2)) return s1;
+  if (!sRef_isReasonable (s1)) return s1;
+  if (!sRef_isReasonable (s2)) return s1;
 
   sRef_combineDefState (s1, s2);
   sRef_combineNullState (s1, s2);
@@ -1389,7 +1572,12 @@ int sRef_compare (sRef s1, sRef s2)
   INTCOMPARERETURN (s1->defstate, s2->defstate);
   INTCOMPARERETURN (s1->aliaskind, s2->aliaskind);
 
-  COMPARERETURN (nstate_compare (s1->nullstate, s2->nullstate));
+  DPRINTF (("Compare null state: %s / %s",
+	    sRef_unparseFull (s1),
+	    sRef_unparseFull (s2)));
+
+  COMPARERETURN (nstate_compare (sRef_getNullState (s1),
+				 sRef_getNullState (s2)));
 
   switch (s1->kind)
     {
@@ -1817,6 +2005,7 @@ sRef_includedBy (sRef small, sRef big)
 	case SR_INTERNAL: return (sRef_isSpecInternalState (big) ||
 				  sRef_isFileStatic (big));
 	case SR_SYSTEM: return (sRef_isSystemState (big));
+	case SR_GLOBALMARKER: BADBRANCH;
 	}
     }
   BADEXIT;
@@ -1842,8 +2031,13 @@ sRef_includedBy (sRef small, sRef big)
 bool
 sRef_realSame (sRef s1, sRef s2)
 {
-  if (s1 == s2) return TRUE;  
-  if (sRef_isInvalid (s1) || sRef_isInvalid (s2)) return FALSE;
+  if (s1 == s2) return TRUE;
+  
+  if (sRef_isUnreasonable (s1) 
+      || sRef_isUnreasonable (s2)) 
+    {
+      return FALSE;
+    }
 
   switch (s1->kind)
     {
@@ -1902,6 +2096,12 @@ sRef_realSame (sRef s1, sRef s2)
   BADEXIT;
 }
 
+bool
+sRef_sameObject (sRef s1, sRef s2)
+{
+  return (s1 == s2);
+}
+
 /*
 ** same is similar to similar, but not quite the same. 
 **
@@ -2034,9 +2234,89 @@ sRef_closeEnough (sRef s1, sRef s2)
     case SK_EXTERNAL:
     case SK_RESULT:
 
-      return FALSE;
+      return FALSE;
+    }
+  BADEXIT;
+}
+
+/*
+  drl add 12/24/2000
+  s is an sRef of a formal paramenter in a function call constraint
+  we trys to return a constraint expression derived from the actual parementer of a function call.
+*/
+
+/*@only@*/ constraintExpr sRef_fixConstraintParam (/*@observer@*/  sRef s, /*@observer@*/ /*@temp@*/ exprNodeList args)
+{
+  constraintExpr ce;
+
+  if (sRef_isInvalid (s))
+    llfatalbug((message("Invalid sRef")));
+
+  switch (s->kind)
+    {
+    case SK_RESULT:
+      {
+	ce = constraintExpr_makeTermsRef (s);
+	return ce;
+      }
+    case SK_FIELD:
+      {
+	sRef temp;
+	
+	temp = (sRef_makeField (sRef_fixBaseParam (s->info->field->rec, args),
+			      s->info->field->field));
+	ce = constraintExpr_makeTermsRef (temp);
+	return ce;
+      }
+    case SK_PTR:
+      {
+	sRef temp;
+	temp = (sRef_makePointer (sRef_fixBaseParam (s->info->ref, args)));
+	ce = constraintExpr_makeTermsRef (temp);
+	return ce;
+      }
+
+    case SK_ARRAYFETCH:
+       {
+	sRef temp;
+	temp = sRef_saveCopy(s);
+	temp = sRef_fixBaseParam (temp, args);
+	ce = constraintExpr_makeTermsRef (temp);
+
+	sRef_free(temp);
+	return ce;
+      }
+    case SK_CVAR:
+      {
+	sRef temp;
+	temp = sRef_saveCopy(s);
+	ce = constraintExpr_makeTermsRef (temp);
+	sRef_free(temp);
+	return ce;
+      }
+    case SK_PARAM:
+      {
+	exprNode e;
+	llassert (exprNodeList_size (args) > s->info->paramno);
+	e = exprNodeList_nth (args, s->info->paramno);
+	
+	llassert (!(exprNode_isError (e)));
+	ce = constraintExpr_makeExprNode (e);
+	return ce;
+      }
+
+    default:
+      {
+	sRef temp;
+	llcontbug (message ("Trying to do fixConstraintParam on nonparam, nonglobal: %q for function with arguments %q",
+			    sRef_unparse (s), exprNodeList_unparse(args)));
+      temp = sRef_saveCopy(s);
+      ce = constraintExpr_makeTermsRef (temp);
+
+      sRef_free(temp);
+      return ce;
+      }
     }
-  BADEXIT;
 }
 
 /*@exposed@*/ sRef
@@ -2081,9 +2361,14 @@ sRef_fixBaseParam (/*@returned@*/ sRef s, exprNodeList args)
 		  (sRef_fixBaseParam (s->info->arrayfetch->arr, args)));
 	}
     case SK_FIELD:
-      return (sRef_makeField (sRef_fixBaseParam (s->info->field->rec, args),
-			      s->info->field->field));
-
+      {
+	sRef res;
+	DPRINTF (("Fix field: %s", sRef_unparseFull (s)));
+	res = sRef_makeField (sRef_fixBaseParam (s->info->field->rec, args),
+			      s->info->field->field);
+	DPRINTF (("Returns: %s", sRef_unparseFull (res)));
+	return res;
+      }
     case SK_PTR:
       return (sRef_makePointer (sRef_fixBaseParam (s->info->ref, args)));
 
@@ -2118,25 +2403,25 @@ sRef_undumpGlobal (char **c)
     {
     case 'g':
       {
-	usymId uid = usymId_fromInt (getInt (c));
+	usymId uid = usymId_fromInt (reader_getInt (c));
 	sstate defstate;
 	nstate nullstate;
 	sRef ret;
 
-	checkChar (c, '@');
-	defstate = sstate_fromInt (getInt (c));
+	reader_checkChar (c, '@');
+	defstate = sstate_fromInt (reader_getInt (c));
 
-	checkChar (c, '@');
-	nullstate = nstate_fromInt (getInt (c));
+	reader_checkChar (c, '@');
+	nullstate = nstate_fromInt (reader_getInt (c));
 
-	ret = sRef_makeGlobal (uid, ctype_unknown);
-	ret->nullstate = nullstate;
+	ret = sRef_makeGlobal (uid, ctype_unknown, stateInfo_currentLoc ());
+	sRef_setNullStateN (ret, nullstate);
 	ret->defstate = defstate;
 	return ret;
       }
     case 's':
       {
-	int i = getInt (c);
+	int i = reader_getInt (c);
 	speckind sk = speckind_fromInt (i);
 
 	switch (sk)
@@ -2145,6 +2430,7 @@ sRef_undumpGlobal (char **c)
 	  case SR_INTERNAL:  return (sRef_makeInternalState ());
 	  case SR_SPECSTATE: return (sRef_makeSpecState ());
 	  case SR_SYSTEM:    return (sRef_makeSystemState ());
+	  case SR_GLOBALMARKER: BADBRANCH;
 	  }
 	BADEXIT;
       }
@@ -2161,8 +2447,7 @@ sRef_undumpGlobal (char **c)
   BADEXIT;
 }
 
-/*@exposed@*/ sRef
-sRef_undump (char **c)
+static /*@exposed@*/ sRef sRef_undumpBody (char **c)
 {
   char p = **c;
 
@@ -2171,16 +2456,18 @@ sRef_undump (char **c)
   switch (p)
     {
     case 'g':
-      return (sRef_makeGlobal (usymId_fromInt (getInt (c)), ctype_unknown));
+      return (sRef_makeGlobal (usymId_fromInt (reader_getInt (c)), 
+			       ctype_unknown, stateInfo_currentLoc ()));
     case 'p':
-      return (sRef_makeParam (getInt (c), ctype_unknown));
+      return (sRef_makeParam (reader_getInt (c), ctype_unknown, 
+			      stateInfo_makeLoc (g_currentloc, SA_DECLARED)));
     case 'r':
-      return (sRef_makeResultType (ctype_undump (c)));
+      return (sRef_makeResult (ctype_undump (c)));
     case 'a':
       {
 	if ((**c >= '0' && **c <= '9') || **c == '-')
 	  {
-	    int i = getInt (c);
+	    int i = reader_getInt (c);
 	    sRef arr = sRef_undump (c);
 	    sRef ret = sRef_buildArrayFetchKnown (arr, i);
 
@@ -2212,7 +2499,7 @@ sRef_undump (char **c)
       }
     case 's':
       {
-	int i = getInt (c);
+	int i = reader_getInt (c);
 	speckind sk = speckind_fromInt (i);
 
 	switch (sk)
@@ -2221,6 +2508,7 @@ sRef_undump (char **c)
 	  case SR_INTERNAL:  return (sRef_makeInternalState ());
 	  case SR_SPECSTATE: return (sRef_makeSpecState ());
 	  case SR_SYSTEM:    return (sRef_makeSystemState ());
+	  case SR_GLOBALMARKER: BADBRANCH;
 	  }
 	BADEXIT;
       }
@@ -2262,8 +2550,21 @@ sRef_undump (char **c)
   BADEXIT;
 }
 
-/*@only@*/ cstring
-sRef_dump (sRef s)
+/*@exposed@*/ sRef sRef_undump (char **c)
+{
+  sRef res = sRef_undumpBody (c);
+
+  if (reader_optCheckChar (c, '='))
+    {
+      multiVal mv = multiVal_undump (c);
+      sRef_setValue (res, mv);
+      reader_checkChar (c, '=');
+    }
+
+  return res;
+}
+
+static /*@only@*/ cstring sRef_dumpBody (sRef s)
 {
   if (sRef_isInvalid (s))
     {
@@ -2301,7 +2602,7 @@ sRef_dump (sRef s)
 			   sRef_dump (s->info->conj->a),
 			   sRef_dump (s->info->conj->b)));
 	case SK_CVAR:
-	  if (sRef_isGlobal (s))
+	  if (sRef_isFileOrGlobalScope (s))
 	    {
 	      return (message ("g%d", 
 			       usymtab_convertId (s->info->cvar->index)));
@@ -2331,8 +2632,22 @@ sRef_dump (sRef s)
   BADEXIT;
 }
 
+/*@only@*/ cstring sRef_dump (sRef s)
+{
+  cstring res = sRef_dumpBody (s);
+
+  if (sRef_hasValue (s))
+    {
+      res = message ("%q=%q=", res, multiVal_dump (sRef_getValue (s)));
+    }
+
+  return res;
+}
+
 cstring sRef_dumpGlobal (sRef s)
 {
+  llassert (!sRef_hasValue (s));
+
   if (sRef_isInvalid (s))
     {
       return (cstring_makeLiteral ("-"));
@@ -2342,12 +2657,12 @@ cstring sRef_dumpGlobal (sRef s)
       switch (s->kind)
 	{
 	case SK_CVAR:
-	  if (sRef_isGlobal (s))
+	  if (sRef_isFileOrGlobalScope (s))
 	    {
 	      return (message ("g%d@%d@%d", 
 			       usymtab_convertId (s->info->cvar->index),
 			       (int) s->defstate,
-			       (int) s->nullstate));
+			       (int) sRef_getNullState (s)));
 	    }
 	  else
 	    {
@@ -2382,7 +2697,14 @@ sRef_deriveType (sRef s, uentryList cl)
     case SK_UNCONSTRAINED:
       return (ctype_unknown);
     case SK_PARAM:
-      return uentry_getType (uentryList_getN (cl, s->info->paramno));
+      if (s->info->paramno >= 0) 
+	{
+	  return uentry_getType (uentryList_getN (cl, s->info->paramno));
+	}
+      else
+	{
+	  return ctype_unknown;
+	}
     case SK_ARRAYFETCH:
       {
 	ctype ca = sRef_deriveType (s->info->arrayfetch->arr, cl);
@@ -2536,6 +2858,7 @@ sRef_unparse (sRef s)
     }
   else
     {
+      DPRINTF (("Not in function like: %s", context_unparse ()));
       return (sRef_unparseNoArgs (s));
     }
 }
@@ -2557,7 +2880,8 @@ sRef_unparseWithArgs (sRef s, uentryList args)
       return (cstring_copy (s->info->fname));
     case SK_PARAM:
       {
-	if (s->info->paramno < uentryList_size (args))
+	if (s->info->paramno < uentryList_size (args)
+	    && s->info->paramno >= 0)
 	  {
 	    uentry ue = uentryList_getN (args, s->info->paramno);
 	    
@@ -2565,9 +2889,7 @@ sRef_unparseWithArgs (sRef s, uentryList args)
 	      return uentry_getName (ue);
 	  }
 
-	return (message ("<bad param: %q / args %q",
-			 sRef_unparseDebug (s),
-			 uentryList_unparse (args)));
+	return (message ("parameter %d", s->info->paramno + 1));
       }
     case SK_ARRAYFETCH:
       if (s->info->arrayfetch->indknown)
@@ -2638,12 +2960,15 @@ sRef_unparseWithArgs (sRef s, uentryList args)
     case SK_CONST:
       return (message ("<const %s>", ctype_unparse (s->type)));
     case SK_SPECIAL:
-      return (cstring_makeLiteral
-	      (s->info->spec == SR_NOTHING ? "nothing"
-	       : s->info->spec == SR_INTERNAL ? "internal state"
-	       : s->info->spec == SR_SPECSTATE ? "spec state"
-	       : s->info->spec == SR_SYSTEM ? "file system state"
-	       : "<spec error>"));
+      switch (s->info->spec)
+	{
+	case SR_NOTHING: return cstring_makeLiteral ("nothing");
+	case SR_INTERNAL: return cstring_makeLiteral ("internal state");
+	case SR_SPECSTATE: return cstring_makeLiteral ("spec state");
+	case SR_SYSTEM: return cstring_makeLiteral ("file system state");
+	case SR_GLOBALMARKER: return cstring_makeLiteral ("<global marker>");
+	}
+      BADBRANCH;
     case SK_RESULT:
       return cstring_makeLiteral ("result");
     default:
@@ -2658,7 +2983,11 @@ sRef_unparseWithArgs (sRef s, uentryList args)
 /*@only@*/ cstring
 sRef_unparseDebug (sRef s)
 {
-  if (sRef_isInvalid (s)) return (cstring_makeLiteral ("<undef>"));
+  if (sRef_isInvalid (s)) 
+    {
+      return (cstring_makeLiteral ("<undef>"));
+    }
+
 
   switch (s->kind)
     {
@@ -2703,7 +3032,17 @@ sRef_unparseDebug (sRef s)
       return (message ("%q.%s", sRef_unparseDebug (s->info->field->rec),
 		       s->info->field->field));
     case SK_PTR:
-      return (message ("*(%q)", sRef_unparseDebug (s->info->ref)));
+      if (sRef_isField (s->info->ref)) 
+	{
+	  sRef fld = s->info->ref;
+
+	  return (message ("%q->%s", sRef_unparseDebug (fld->info->field->rec),
+			   fld->info->field->field));
+	}
+      else
+	{
+	  return (message ("*(%q)", sRef_unparseDebug (s->info->ref)));
+	}
     case SK_ADR:
       return (message ("&%q", sRef_unparseDebug (s->info->ref)));
     case SK_OBJECT:
@@ -2720,7 +3059,14 @@ sRef_unparseDebug (sRef s)
     case SK_TYPE:
       return (message ("<type %s>", ctype_unparse (s->type)));
     case SK_CONST:
-      return (message ("<const %s>", ctype_unparse (s->type)));
+      if (sRef_hasValue (s))
+	{
+	  return (message ("<const %s=%q>", ctype_unparse (s->type), multiVal_unparse (sRef_getValue (s))));
+	}
+      else
+	{
+	  return (message ("<const %s>", ctype_unparse (s->type)));
+	}
     case SK_RESULT:
       return (message ("<result %s>", ctype_unparse (s->type)));
     case SK_SPECIAL:
@@ -2754,7 +3100,8 @@ sRef_unparseNoArgs (sRef s)
 
 	if (uentry_isInvalid (ce))
 	  {
-	    llcontbug (message ("sRef_unparseNoArgs: bad cvar: %q", sRef_unparseDebug (s)));
+	    llcontbug (message ("sRef_unparseNoArgs: bad cvar: %q", 
+				sRef_unparseDebug (s)));
 	    return (sRef_unparseDebug (s)); 
 	  }
 	else
@@ -2818,7 +3165,7 @@ sRef_unparseNoArgs (sRef s)
     case SK_UNKNOWN:
       return cstring_makeLiteral ("?");
     case SK_PARAM:
-       llcontbug (message ("sRef_unparseNoArgs: bad case: %q", sRef_unparseDebug (s))); 
+      /* llcontbug (message ("sRef_unparseNoArgs: bad case: %q", sRef_unparseDebug (s))); */
       return (sRef_unparseDebug (s));
     }
   BADEXIT;
@@ -2830,7 +3177,7 @@ sRef_unparseNoArgs (sRef s)
 
   s->kind = SK_UNCONSTRAINED;
   s->info = (sinfo) dmalloc (sizeof (*s->info));
-  s->info->fname = fname;
+  s->info->fname = cstring_copy (fname); /* evans 2002-07-12: this was exposed, causing memory errors */
 
   return (s);
 }
@@ -2844,15 +3191,15 @@ cstring sRef_unconstrainedName (sRef s)
 
 bool sRef_isUnconstrained (sRef s) 
 {
-  return (sRef_isValid(s) && s->kind == SK_UNCONSTRAINED);
+  return (sRef_isReasonable(s) && s->kind == SK_UNCONSTRAINED);
 }
 
 static /*@dependent@*/ /*@notnull@*/ sRef 
-  sRef_makeCvarAux (int level, usymId index, ctype ct)
+  sRef_makeCvarAux (int level, usymId index, ctype ct, /*@only@*/ stateInfo stinfo)
 {
-  sRef s = sRef_new ();
-
-    s->kind = SK_CVAR;
+  sRef s = sRef_newRef ();
+  
+  s->kind = SK_CVAR;
   s->info = (sinfo) dmalloc (sizeof (*s->info));
 
   s->info->cvar = (cref) dmalloc (sizeof (*s->info->cvar));
@@ -2887,24 +3234,27 @@ static /*@dependent@*/ /*@notnull@*/ sRef
   llassert (level >= globScope);
   llassert (usymId_isValid (index));
 
+  DPRINTF (("Made cvar: [%p] %s", s, sRef_unparseDebug (s)));
+  llassert (valueTable_isUndefined (s->state));
+  s->state = context_createValueTable (s, stinfo); 
   return s;
 }
 
-/*@dependent@*/ sRef sRef_makeCvar (int level, usymId index, ctype ct)
+/*@dependent@*/ sRef sRef_makeCvar (int level, usymId index, ctype ct, /*@only@*/ stateInfo stinfo)
 {
-  return (sRef_makeCvarAux (level, index, ct));
+  return (sRef_makeCvarAux (level, index, ct, stinfo));
 }
 
 int sRef_lexLevel (sRef s)
 {
-  if (sRef_isValid (s))
+  if (sRef_isReasonable (s))
     {
       sRef conj;
 
       conj = sRef_fixConj (s);
       s = sRef_getRootBase (conj);
       
-      if (sRef_isValid (s) && s->kind == SK_CVAR)
+      if (sRef_isReasonable (s) && s->kind == SK_CVAR)
 	{
 	  return (s->info->cvar->lexlevel);
 	}
@@ -2914,20 +3264,21 @@ int sRef_lexLevel (sRef s)
 }
 
 sRef
-sRef_makeGlobal (usymId l, ctype ct)
+sRef_makeGlobal (usymId l, ctype ct, /*@only@*/ stateInfo stinfo)
 {
-  return (sRef_makeCvar (globScope, l, ct));
+  return (sRef_makeCvar (globScope, l, ct, stinfo));
 }
 
 void
 sRef_setParamNo (sRef s, int l)
 {
-  llassert (sRef_isValid (s) && s->kind == SK_PARAM);
+  llassert (sRef_isReasonable (s) && s->kind == SK_PARAM);
   s->info->paramno = l;
+  llassert (l >= -1);
 }
 
 /*@dependent@*/ sRef
-sRef_makeParam (int l, ctype ct)
+sRef_makeParam (int l, ctype ct, stateInfo stinfo)
 {
   sRef s = sRef_new ();
 
@@ -2936,8 +3287,12 @@ sRef_makeParam (int l, ctype ct)
 
   s->info = (sinfo) dmalloc (sizeof (*s->info));
   s->info->paramno = l; 
-  s->defstate = SS_UNKNOWN; /* (probably defined, unless its an out parameter) */
+  llassert (l >= -1);
+  s->defstate = SS_UNKNOWN; 
+  /* (probably defined, unless its an out parameter) */
 
+  llassert (valueTable_isUndefined (s->state));
+  s->state = context_createValueTable (s, stinfo);
   return s;
 }
 
@@ -2946,7 +3301,7 @@ sRef_isIndexKnown (sRef arr)
 {
   bool res;
 
-  llassert (sRef_isValid (arr));
+  llassert (sRef_isReasonable (arr));
   arr = sRef_fixConj (arr);
   
   llassert (arr->kind == SK_ARRAYFETCH);  
@@ -2959,7 +3314,7 @@ sRef_getIndex (sRef arr)
 {
   int result;
 
-  llassert (sRef_isValid (arr));
+  llassert (sRef_isReasonable (arr));
   arr = sRef_fixConj (arr);
 
   llassert (arr->kind == SK_ARRAYFETCH);  
@@ -2999,12 +3354,12 @@ static bool sRef_isZerothArrayFetch (/*@notnull@*/ sRef s)
     }
   else
     {
-      sRef s = sRef_new ();
+      sRef s = sRef_newRef ();
       
       s->kind = SK_ADR;
       s->type = ctype_makePointer (t->type);
       s->info = (sinfo) dmalloc (sizeof (*s->info));
-      s->info->ref = t;
+      s->info->ref = t; 
       
       if (t->defstate == SS_UNDEFINED) 
 	/* no! it is allocated even still: && !ctype_isPointer (t->type)) */
@@ -3024,6 +3379,9 @@ static bool sRef_isZerothArrayFetch (/*@notnull@*/ sRef s)
 	    }
 	}
 
+      llassert (valueTable_isUndefined (s->state));
+      s->state = context_createValueTable (s, 
+					   stateInfo_makeLoc (g_currentloc, SA_CREATED));
       return s;
     }
 }
@@ -3032,10 +3390,10 @@ cstring sRef_getField (sRef s)
 {
   cstring res;
 
-  llassert (sRef_isValid (s));
+  llassert (sRef_isReasonable (s));
   s = sRef_fixConj (s);
 
-  llassertprint (sRef_isValid (s) && (s->kind == SK_FIELD),
+  llassertprint (sRef_isReasonable (s) && (s->kind == SK_FIELD),
 		 ("s = %s", sRef_unparseDebug (s)));
 
   res = s->info->field->field;
@@ -3118,7 +3476,7 @@ sRef_getRootBaseAux (sRef s, int depth)
 		("Warning: reference base limit exceeded for %q. "
 		 "This either means there is a variable with at least "
 		 "%d indirections from this reference, or "
-		 "there is a bug in LCLint.",
+		 "there is a bug in Splint.",
 		 sRef_unparse (s),
 		 MAXBASEDEPTH),
 		g_currentloc);
@@ -3190,38 +3548,48 @@ static int sRef_depth (sRef s)
 sRef
 sRef_makeObject (ctype o)
 {
-  sRef s = sRef_new ();
+  sRef s = sRef_newRef (); 
 
   s->kind = SK_OBJECT;
   s->info = (sinfo) dmalloc (sizeof (*s->info));
   s->info->object = o;
+  llassert (valueTable_isUndefined (s->state));
+  s->state = context_createValueTable (s, stateInfo_makeLoc (g_currentloc, SA_CREATED));
   return s;
 }
 
-sRef sRef_makeExternal (/*@exposed@*/ sRef t)
+/*
+** This is used to represent storage referenced by a parameter.
+*/
+
+sRef sRef_makeExternal (sRef t)
 {
-  sRef s = sRef_new ();
+  sRef s = sRef_newRef ();
 
-  llassert (sRef_isValid (t));
+  llassert (sRef_isReasonable (t));
 
   s->kind = SK_EXTERNAL;
   s->info = (sinfo) dmalloc (sizeof (*s->info));
   s->type = t->type;
   s->info->ref = t;
+  llassert (valueTable_isUndefined (s->state));
+  s->state = context_createValueTable (s, stateInfo_makeLoc (g_currentloc, SA_DECLARED));
   return s;
 }
 
-sRef sRef_makeDerived (/*@exposed@*/ sRef t)
+/*@dependent@*/ sRef sRef_makeDerived (/*@exposed@*/ sRef t)
 {
-  if (sRef_isValid (t))
+  if (sRef_isReasonable (t))
     {
-      sRef s = sRef_new ();
+      sRef s = sRef_newRef ();
       
       s->kind = SK_DERIVED;
       s->info = (sinfo) dmalloc (sizeof (*s->info));
       s->info->ref = t;
       
       s->type = t->type;
+      llassert (valueTable_isUndefined (s->state));
+      s->state = context_createValueTable (s, stateInfo_makeLoc (g_currentloc, SA_CREATED));
       return s;
     }
   else
@@ -3239,8 +3607,8 @@ sRef sRef_makeDerived (/*@exposed@*/ sRef t)
 void
 sRef_mergeStateQuiet (sRef res, sRef other)
 {
-  llassert (sRef_isValid (res));
-  llassert (sRef_isValid (other));
+  llassert (sRef_isReasonable (res));
+  llassert (sRef_isReasonable (other));
 
   res->modified = res->modified || other->modified;
   res->safe = res->safe && other->safe;
@@ -3248,7 +3616,7 @@ sRef_mergeStateQuiet (sRef res, sRef other)
   if (res->defstate == SS_UNKNOWN) 
     {
       res->defstate = other->defstate;
-      res->definfo = alinfo_update (res->definfo, other->definfo);
+      res->definfo = stateInfo_update (res->definfo, other->definfo);
     }
 
   if (res->aliaskind == AK_UNKNOWN || 
@@ -3256,35 +3624,34 @@ sRef_mergeStateQuiet (sRef res, sRef other)
     {
       res->aliaskind = other->aliaskind;
       res->oaliaskind = other->oaliaskind;
-      res->aliasinfo = alinfo_update (res->aliasinfo, other->aliasinfo);
+      res->aliasinfo = stateInfo_update (res->aliasinfo, other->aliasinfo);
     }
 
   if (res->expkind == XO_UNKNOWN)
     {
       res->expkind = other->expkind;
       res->oexpkind = other->oexpkind;
-      res->expinfo = alinfo_update (res->expinfo, other->expinfo);
+      res->expinfo = stateInfo_update (res->expinfo, other->expinfo);
     }
   
   /* out takes precedence over implicitly defined */
   if (res->defstate == SS_DEFINED && other->defstate != SS_UNKNOWN) 
     {
       res->defstate = other->defstate;
-      res->definfo = alinfo_update (res->definfo, other->definfo);
+      res->definfo = stateInfo_update (res->definfo, other->definfo);
     }
 
-  if (other->nullstate == NS_ERROR || res->nullstate == NS_ERROR) 
+  if (sRef_getNullState (other) == NS_ERROR || sRef_getNullState (res) == NS_ERROR) 
     {
-      res->nullstate = NS_ERROR;
+      sRef_setNullState (res, NS_ERROR, fileloc_undefined);
     }
   else
     {
-      if (other->nullstate != NS_UNKNOWN 
-	  && (res->nullstate == NS_UNKNOWN || res->nullstate == NS_NOTNULL 
-	      || res->nullstate == NS_MNOTNULL))
+      if (sRef_getNullState (other) != NS_UNKNOWN 
+	  && (sRef_getNullState (res) == NS_UNKNOWN || sRef_getNullState (res) == NS_NOTNULL 
+	      || sRef_getNullState (res) == NS_MNOTNULL))
 	{
-	  res->nullstate = other->nullstate;
-	  res->nullinfo = alinfo_update (res->nullinfo, other->nullinfo);
+	  sRef_updateNullState (res, other);
 	}
     }
 }
@@ -3296,12 +3663,13 @@ sRef_mergeStateQuiet (sRef res, sRef other)
 */
 
 void
-sRef_mergeStateQuietReverse (sRef res, sRef other)
+sRef_mergeStateQuietReverse (/*@dependent@*/ sRef res, /*@dependent@*/ sRef other)
 {
   bool changed = FALSE;
 
-  llassert (sRef_isValid (res));
-  llassert (sRef_isValid (other));
+  llassert (sRef_isReasonable (res));
+  llassert (sRef_isReasonable (other));
+  sRef_checkMutable (res);
 
   if (res->kind != other->kind)
     {
@@ -3337,14 +3705,14 @@ sRef_mergeStateQuietReverse (sRef res, sRef other)
       changed = TRUE;
       res->aliaskind = other->aliaskind;
       res->oaliaskind = other->oaliaskind;
-      res->aliasinfo = alinfo_update (res->aliasinfo, other->aliasinfo);
-          }
+      res->aliasinfo = stateInfo_update (res->aliasinfo, other->aliasinfo);
+    }
 
   if (other->expkind != XO_UNKNOWN && other->expkind != res->expkind)
     {
       changed = TRUE;
       res->expkind = other->expkind;
-      res->expinfo = alinfo_update (res->expinfo, other->expinfo);
+      res->expinfo = stateInfo_update (res->expinfo, other->expinfo);
     }
 
   if (other->oexpkind != XO_UNKNOWN)
@@ -3359,24 +3727,25 @@ sRef_mergeStateQuietReverse (sRef res, sRef other)
       if (other->defstate != SS_UNKNOWN)
 	{
 	  res->defstate = other->defstate;
+	  res->definfo = stateInfo_update (res->definfo, other->definfo);
 	}
     }
 
-  if (other->nullstate == NS_ERROR || res->nullstate == NS_ERROR)
+  if (sRef_getNullState (other) == NS_ERROR || sRef_getNullState (res) == NS_ERROR)
     {
-      if (res->nullstate != NS_ERROR)
+      if (sRef_getNullState (res) != NS_ERROR)
 	{
-	  res->nullstate = NS_ERROR;
+	  sRef_setNullStateN (res, NS_ERROR);
 	  changed = TRUE;
 	}
     }
   else
     {
-      if (other->nullstate != NS_UNKNOWN && other->nullstate != res->nullstate)
+      if (sRef_getNullState (other) != NS_UNKNOWN 
+	  && sRef_getNullState (other) != sRef_getNullState (res))
 	{
 	  changed = TRUE;
-	  res->nullstate = other->nullstate;
-	  res->nullinfo = alinfo_update (res->nullinfo, other->nullinfo);
+	  sRef_updateNullState (res, other);
 	}
     }
 
@@ -3389,7 +3758,7 @@ sRef_mergeStateQuietReverse (sRef res, sRef other)
 void 
 sRef_mergeState (sRef res, sRef other, clause cl, fileloc loc)
 {
-  if (sRef_isValid (res) && sRef_isValid (other))
+  if (sRef_isReasonable (res) && sRef_isReasonable (other))
     {
       sRef_mergeStateAux (res, other, cl, FALSE, loc, TRUE);
     }
@@ -3411,7 +3780,7 @@ sRef_mergeState (sRef res, sRef other, clause cl, fileloc loc)
 void 
 sRef_mergeOptState (sRef res, sRef other, clause cl, fileloc loc)
 {
-  if (sRef_isValid (res) && sRef_isValid (other))
+  if (sRef_isReasonable (res) && sRef_isReasonable (other))
     {
       sRef_mergeStateAux (res, other, cl, TRUE, loc, TRUE);
     }
@@ -3436,9 +3805,16 @@ sRef_mergeStateAux (/*@notnull@*/ sRef res, /*@notnull@*/ sRef other,
 		    bool doDerivs)
    /*@modifies res@*/ 
 {
-  llassertfatal (sRef_isValid (res));
-  llassertfatal (sRef_isValid (other));
+  llassertfatal (sRef_isReasonable (res));
+  llassertfatal (sRef_isReasonable (other));
   
+  DPRINTF (("Merge aux: %s / %s",
+	    sRef_unparseFull (res),
+	    sRef_unparseFull (other)));
+
+  sRef_checkMutable (res);
+  sRef_checkMutable (other);
+
   res->modified = res->modified || other->modified;
 
   if (res->kind == other->kind 
@@ -3446,7 +3822,7 @@ sRef_mergeStateAux (/*@notnull@*/ sRef res, /*@notnull@*/ sRef other,
     {
       sstate odef = other->defstate;
       sstate rdef = res->defstate;
-      nstate onull = other->nullstate;
+      nstate onull = sRef_getNullState (other);
       
       /*
       ** yucky stuff to handle 
@@ -3469,7 +3845,7 @@ sRef_mergeStateAux (/*@notnull@*/ sRef res, /*@notnull@*/ sRef other,
 	      res->defstate = SS_DEAD;
 	    }
 
-	  res->definfo = alinfo_update (res->definfo, other->definfo);
+	  res->definfo = stateInfo_update (res->definfo, other->definfo);
 	  sRef_clearDerived (other);
 	  sRef_clearDerived (res);
 	}
@@ -3488,6 +3864,7 @@ sRef_mergeStateAux (/*@notnull@*/ sRef res, /*@notnull@*/ sRef other,
 	      res->defstate = SS_DEAD;
 	    }
 	  
+	  res->definfo = stateInfo_update (res->definfo, other->definfo);
 	  sRef_clearDerived (other);
 	  sRef_clearDerived (res);
 	}
@@ -3501,7 +3878,7 @@ sRef_mergeStateAux (/*@notnull@*/ sRef res, /*@notnull@*/ sRef other,
 	       && (res->defstate == SS_ALLOCATED && sRef_definitelyNull (res)))
 	{
 	  res->defstate = SS_DEFINED;
-	  res->definfo = alinfo_update (res->definfo, other->definfo);
+	  res->definfo = stateInfo_update (res->definfo, other->definfo);
 	}
       else
 	{
@@ -3538,8 +3915,8 @@ sRef_mergeStateAux (/*@notnull@*/ sRef res, /*@notnull@*/ sRef other,
 	  other->defstate = SS_DEAD;
 	  sRef_clearDerived (res);
 	  sRef_clearDerived (other);
-	  	}
-
+	}
+      
       if (alkind_isDependent (res->aliaskind) && other->defstate == SS_DEAD)
 	{
 	  res->aliaskind = AK_UNKNOWN;
@@ -3563,13 +3940,11 @@ sRef_mergeStateAux (/*@notnull@*/ sRef res, /*@notnull@*/ sRef other,
 	    {
 	      if (onull == NS_DEFNULL || onull == NS_CONSTNULL)
 		{
-		  res->deriv = sRefSet_copy (res->deriv, other->deriv);
-		}
-
-	      	      	      ; 
+		  res->deriv = sRefSet_copyInto (res->deriv, other->deriv);
+		  DPRINTF (("Copy derivs: %s", sRef_unparseFull (res)));
+		}	      	      	      
 	    }
-	  else if (odef == SS_ALLOCATED
-		   || odef == SS_SPECIAL)
+	  else if (odef == SS_ALLOCATED || odef == SS_SPECIAL)
 	    {
 	      
 	      if (doDerivs)
@@ -3579,11 +3954,13 @@ sRef_mergeStateAux (/*@notnull@*/ sRef res, /*@notnull@*/ sRef other,
 		      res->deriv = sRef_mergeUnionDerivs (res->deriv, 
 							  other->deriv, 
 							  opt, cl, loc);
+		      DPRINTF (("Copy derivs: %s", sRef_unparseFull (res)));
 		    }
 		  else
 		    {
-		      		      res->deriv = sRef_mergeDerivs (res->deriv, other->deriv, 
+		      res->deriv = sRef_mergeDerivs (res->deriv, other->deriv, 
 						     opt, cl, loc);
+		      DPRINTF (("Copy derivs: %s", sRef_unparseFull (res)));
 		    }
 		}
 	    }
@@ -3591,12 +3968,14 @@ sRef_mergeStateAux (/*@notnull@*/ sRef res, /*@notnull@*/ sRef other,
 	    {
 	      if (doDerivs)
 		{
-		  		  res->deriv = sRef_mergeDerivs (res->deriv, other->deriv, 
+		  res->deriv = sRef_mergeDerivs (res->deriv, other->deriv, 
 						 opt, cl, loc);
+		  DPRINTF (("Copy derivs: %s", sRef_unparseFull (res)));
 		}
 	      else
 		{
-		  		}
+		  ;
+		}
 	    }
 	}
       else
@@ -3604,30 +3983,32 @@ sRef_mergeStateAux (/*@notnull@*/ sRef res, /*@notnull@*/ sRef other,
 	  if (rdef == SS_PDEFINED
 	      || (rdef == SS_DEFINED && odef == SS_PDEFINED))
 	    {
-	      if (doDerivs)
-		{
-		  		  res->deriv = sRef_mergePdefinedDerivs (res->deriv, other->deriv, 
-							 opt, cl, loc);
-		}
+		if (doDerivs)
+		    {
+		      res->deriv = sRef_mergePdefinedDerivs (res->deriv, other->deriv, 
+							     opt, cl, loc);
+		      DPRINTF (("Copy derivs: %s", sRef_unparseFull (res)));
+		    }
 	    }
 	  else
 	    {
 	      if ((rdef == SS_DEFINED  || rdef == SS_UNKNOWN)
 		  && res->defstate == SS_ALLOCATED)
 		{
-		  		  res->deriv = sRefSet_copy (res->deriv, other->deriv);
+		  res->deriv = sRefSet_copyInto (res->deriv, other->deriv);
 		}
 	      else
 		{
 		  if (doDerivs)
 		    {
-		      		      res->deriv = sRef_mergeDerivs (res->deriv, other->deriv, 
+		      res->deriv = sRef_mergeDerivs (res->deriv, other->deriv, 
 						     opt, cl, loc);
+		      DPRINTF (("Copy derivs: %s", sRef_unparseFull (res)));
 		    }
 		}
 	    }
 	}
-
+      
       
       sRef_combineExKinds (res, other);
     }
@@ -3644,7 +4025,7 @@ sRef_mergeStateAux (/*@notnull@*/ sRef res, /*@notnull@*/ sRef other,
 	{
 	  sRef nother = sRef_buildPointer (sRef_getBase (other));
 
-	  if (sRef_isValid (nother))
+	  if (sRef_isReasonable (nother))
 	    {
 	      sRef_copyState (nother, other);
 	      sRef_mergeStateAux (res, nother, cl, opt, loc, doDerivs);
@@ -3657,8 +4038,41 @@ sRef_mergeStateAux (/*@notnull@*/ sRef res, /*@notnull@*/ sRef other,
 	  
 	}
     }
-  
-  }
+
+  /* 
+  ** Merge value table states
+  */
+
+# if 0
+  /*
+  ** This doesn't do anything.  And its broken too...
+  */
+
+  valueTable_elements (res->state, key, sv) 
+    {
+      stateValue os = valueTable_lookup (other->state, key);
+      /*@unused@*/ int val;
+      /*@unused@*/ char *msg;
+
+      llassert (stateValue_isDefined (os));
+      
+      DPRINTF (("Merge state: %s / %s", 
+		cstring_toCharsSafe (stateValue_unparse (sv)), 
+		cstring_toCharsSafe (stateValue_unparse (os))));
+      /*
+	val = valueMatix_lookup (key, 
+	stateValue_getValue (os),
+	stateValue_getValue (sv), 
+	&msg);
+	DPRINTF (("Val: %d / %s", val, msg));
+      */
+  } end_valueTable_elements ; 
+# endif
+
+  DPRINTF (("Merge aux: %s / %s",
+	    sRef_unparseFull (res),
+	    sRef_unparseFull (other)));
+}
 
 static sRefSet
 sRef_mergeUnionDerivs (/*@only@*/ sRefSet res, 
@@ -3667,17 +4081,17 @@ sRef_mergeUnionDerivs (/*@only@*/ sRefSet res,
 {
   if (sRefSet_isEmpty (res))
     {
-      return sRefSet_copy (res, other);
+      return sRefSet_copyInto (res, other);
     }
   else
     {
       sRefSet_allElements (other, el)
 	{
-	  if (sRef_isValid (el))
+	  if (sRef_isReasonable (el))
 	    {
 	      sRef e2 = sRefSet_lookupMember (other, el);
 	      
-	      if (sRef_isValid (e2))
+	      if (sRef_isReasonable (e2))
 		{
 		  sRef_mergeStateAux (el, e2, cl, opt, loc, FALSE);
 		}
@@ -3697,15 +4111,14 @@ sRef_mergeDerivs (/*@only@*/ sRefSet res, sRefSet other,
 		  bool opt, clause cl, fileloc loc)
 {
   sRefSet ret = sRefSet_new ();
-  
-    
+
   sRefSet_allElements (res, el)
     {
-      if (sRef_isValid (el))
+      if (sRef_isReasonable (el))
 	{
 	  sRef e2 = sRefSet_lookupMember (other, el);
 
-	  if (sRef_isValid (e2))
+	  if (sRef_isReasonable (e2))
 	    {
 	      if (el->defstate == SS_ALLOCATED &&
 		  e2->defstate == SS_PDEFINED)
@@ -3716,13 +4129,16 @@ sRef_mergeDerivs (/*@only@*/ sRefSet res, sRefSet other,
 		       el->defstate == SS_PDEFINED)
 		{
 		  el->defstate = SS_ALLOCATED;
+		  el->definfo = stateInfo_update (el->definfo, e2->definfo);
 		  sRef_clearDerived (el);
 		}
 	      else if ((el->defstate == SS_DEAD || sRef_isKept (el)) &&
 		       (e2->defstate == SS_DEFINED && !sRef_isKept (e2)))
 		{
-		  
-		  if (checkDeadState (el, TRUE, loc))
+		  DPRINTF (("Checking dead: %s / %s", sRef_unparseFull (el),
+			    sRef_unparseFull (e2)));
+
+		  if (checkDeadState (el, e2, TRUE, loc))
 		    {
 		      if (sRef_isThroughArrayFetch (el))
 			{
@@ -3734,8 +4150,10 @@ sRef_mergeDerivs (/*@only@*/ sRefSet res, sRefSet other,
 	      else if ((e2->defstate == SS_DEAD || sRef_isKept (e2)) &&
 		       (el->defstate == SS_DEFINED && !sRef_isKept (el)))
 		{
-		  
-		  if (checkDeadState (e2, FALSE, loc))
+		  DPRINTF (("Checking dead: %s / %s", sRef_unparseFull (el),
+			    sRef_unparseFull (e2)));
+
+		  if (checkDeadState (e2, el, FALSE, loc))
 		    {
 		      if (sRef_isThroughArrayFetch (el))
 			{
@@ -3747,12 +4165,16 @@ sRef_mergeDerivs (/*@only@*/ sRefSet res, sRefSet other,
 	      else if (el->defstate == SS_DEFINED &&
 		       e2->defstate == SS_PDEFINED)
 		{
+		  DPRINTF (("set pdefined: %s", sRef_unparseFull (el)));
 		  el->defstate = SS_PDEFINED;
+		  el->definfo = stateInfo_update (el->definfo, e2->definfo);
 		}
 	      else if (e2->defstate == SS_DEFINED &&
 		       el->defstate == SS_PDEFINED)
 		{
+		  DPRINTF (("set pdefined: %s", sRef_unparseFull (e2)));
 		  e2->defstate = SS_PDEFINED;
+		  e2->definfo = stateInfo_update (e2->definfo, el->definfo);
 		}
 	      else
 		{
@@ -3771,13 +4193,13 @@ sRef_mergeDerivs (/*@only@*/ sRefSet res, sRefSet other,
 	      
 	      if (sRef_equivalent (el, e2))
 		{
-		  		  ret = sRefSet_insert (ret, el);
+		  ret = sRefSet_insert (ret, el);
 		}
 	      else
 		{
 		  sRef sr = sRef_leastCommon (el, e2);
 
-		  if (sRef_isValid (sr))
+		  if (sRef_isReasonable (sr))
 		    {
 		      ret = sRefSet_insert (ret, sr);
 		    }
@@ -3791,19 +4213,21 @@ sRef_mergeDerivs (/*@only@*/ sRefSet res, sRefSet other,
 	    }
 	  else /* not defined */
 	    {
-	      	      (void) checkDeadState (el, TRUE, loc);
+	      DPRINTF (("Checking dead: %s", sRef_unparseFull (el)));
+	      (void) checkDeadState (el, e2, TRUE, loc);
 	    }
 	}
     } end_sRefSet_allElements;
 
   sRefSet_allElements (other, el)
     {
-      if (sRef_isValid (el))
+      if (sRef_isReasonable (el))
 	{
-	  (void) checkDeadState (el, FALSE, loc);
+	  DPRINTF (("Checking dead: %s", sRef_unparseFull (el)));
+	  (void) checkDeadState (el, sRef_undefined, FALSE, loc);
 	}
     } end_sRefSet_allElements;
-  
+    
   sRefSet_free (res); 
   return (ret);
 }
@@ -3812,7 +4236,7 @@ sRef_mergeDerivs (/*@only@*/ sRefSet res, sRefSet other,
 ** Returns TRUE is there is an error.
 */
 
-static bool checkDeadState (/*@notnull@*/ sRef el, bool tbranch, fileloc loc)
+static bool checkDeadState (/*@notnull@*/ sRef el, sRef e2, bool tbranch, fileloc loc)
 {
   /*
   ** usymtab_isGuarded --- the utab should still be in the
@@ -3829,24 +4253,25 @@ static bool checkDeadState (/*@notnull@*/ sRef el, bool tbranch, fileloc loc)
 
   
   if ((sRef_isDead (el) || sRef_isKept (el))
-      && !sRef_isDeepUnionField (el) && !sRef_isThroughArrayFetch (el))
+      && !sRef_isDeepUnionField (el) 
+      && !sRef_isThroughArrayFetch (el))
     {
        
       if (!tbranch)
 	{
-	  if (usymtab_isProbableDeepNull (el))
+	  if (usymtab_isDefinitelyNullDeep (el))
 	    {
-	      	      return TRUE;
+	      return TRUE;
 	    }
 	}
       else
 	{
-	  if (usymtab_isAltProbablyDeepNull (el))
+	  if (usymtab_isAltDefinitelyNullDeep (el))
 	    {
-	      	      return TRUE;
+	      return TRUE;
 	    }
 	}
-
+      
       if (optgenerror
 	  (FLG_BRANCHSTATE,
 	   message ("Storage %q is %q in one path, but live in another.",
@@ -3855,7 +4280,6 @@ static bool checkDeadState (/*@notnull@*/ sRef el, bool tbranch, fileloc loc)
 					 ? "kept" : "released")),
 	   loc))
 	{
-	  	  
 	  if (sRef_isKept (el))
 	    {
 	      sRef_showAliasInfo (el);      
@@ -3865,10 +4289,21 @@ static bool checkDeadState (/*@notnull@*/ sRef el, bool tbranch, fileloc loc)
 	      sRef_showStateInfo (el);
 	    }
 
+	  if (sRef_isValid (e2))
+	    {
+	      if (sRef_isKept (e2))
+		{
+		  sRef_showAliasInfo (e2);      
+		}
+	      else
+		{
+		  sRef_showStateInfo (e2);
+		}
+	    }
+
 	  /* prevent further errors */
 	  el->defstate = SS_UNKNOWN; 
-	  sRef_setAliasKind (el, AK_ERROR, fileloc_undefined);
-	  
+	  sRef_setAliasKind (el, AK_ERROR, fileloc_undefined);	  
 	  return FALSE;
 	}
     }
@@ -3879,14 +4314,13 @@ static bool checkDeadState (/*@notnull@*/ sRef el, bool tbranch, fileloc loc)
 static void 
 checkDerivDeadState (/*@notnull@*/ sRef el, bool tbranch, fileloc loc)
 {
-  
-  if (checkDeadState (el, tbranch, loc))
+  if (checkDeadState (el, sRef_undefined, tbranch, loc))
     {
       sRefSet_allElements (el->deriv, t)
 	{
-	  if (sRef_isValid (t))
+	  if (sRef_isReasonable (t))
 	    {
-	      	      checkDerivDeadState (t, tbranch, loc);
+	      checkDerivDeadState (t, tbranch, loc);
 	    }
 	} end_sRefSet_allElements;
     }
@@ -3900,11 +4334,11 @@ static sRefSet
 
   sRefSet_allElements (res, el)
     {
-      if (sRef_isValid (el))
+      if (sRef_isReasonable (el))
 	{
 	  sRef e2 = sRefSet_lookupMember (other, el);
 	  
-	  if (sRef_isValid (e2))
+	  if (sRef_isReasonable (e2))
 	    {
 	      if (sRef_isAllocated (el) && !sRef_isAllocated (e2))
 		{
@@ -3912,7 +4346,7 @@ static sRefSet
 		}
 	      else if (sRef_isAllocated (e2) && !sRef_isAllocated (el))
 		{
-		  el->deriv = sRefSet_copy (el->deriv, e2->deriv); 
+		  el->deriv = sRefSet_copyInto (el->deriv, e2->deriv); 
 		}
 	      else
 		{
@@ -3929,7 +4363,7 @@ static sRefSet
 	    {
 	      if (!opt)
 		{
-		  		  checkDerivDeadState (el, (cl == FALSECLAUSE), loc);
+		  checkDerivDeadState (el, (cl == FALSECLAUSE), loc);
 		}
 
 	      ret = sRefSet_insert (ret, el);
@@ -3939,7 +4373,7 @@ static sRefSet
   
   sRefSet_allElements (other, el)
     {
-      if (sRef_isValid (el))
+      if (sRef_isReasonable (el))
 	{
 	  if (!sRefSet_member (ret, el))
 	    {
@@ -3962,12 +4396,12 @@ static sRefSet
 
 sRef sRef_makeConj (/*@exposed@*/ /*@returned@*/ sRef a, /*@exposed@*/ sRef b)
 {
-  llassert (sRef_isValid (a));
-  llassert (sRef_isValid (b));
+  llassert (sRef_isReasonable (a));
+  llassert (sRef_isReasonable (b));
       
   if (!sRef_equivalent (a, b))
     {
-      sRef s = sRef_new ();
+      sRef s = sRef_newRef ();
       
       s->kind = SK_CONJ;
       s->info = (sinfo) dmalloc (sizeof (*s->info));
@@ -3981,17 +4415,21 @@ sRef sRef_makeConj (/*@exposed@*/ /*@returned@*/ sRef a, /*@exposed@*/ sRef b)
       if (a->defstate == b->defstate)
 	{
 	  s->defstate = a->defstate;
+	  s->definfo = stateInfo_update (s->definfo, a->definfo);
+	  s->definfo = stateInfo_update (s->definfo, b->definfo);
 	}
       else
 	{
 	  s->defstate = SS_UNKNOWN; 
 	}
       
-      s->nullstate = NS_UNKNOWN;
+      sRef_setNullStateN (s, NS_UNKNOWN);
       
       s->safe = a->safe && b->safe;
       s->aliaskind = alkind_resolve (a->aliaskind, b->aliaskind);
 
+      llassert (valueTable_isUndefined (s->state));
+      s->state = context_createValueTable (s, stateInfo_makeLoc (g_currentloc, SA_MERGED));
       return s;
     }
   else
@@ -4000,7 +4438,7 @@ sRef sRef_makeConj (/*@exposed@*/ /*@returned@*/ sRef a, /*@exposed@*/ sRef b)
     }
 }
 
-sRef
+/*@dependent@*/ sRef
 sRef_makeUnknown ()
 {
   sRef s = sRef_new ();
@@ -4009,7 +4447,7 @@ sRef_makeUnknown ()
   return s;
 }
 
-static sRef
+static /*@owned@*/ /*@notnull@*/ sRef
 sRef_makeSpecial (speckind sk) /*@*/
 {
   sRef s = sRef_new ();
@@ -4017,15 +4455,17 @@ sRef_makeSpecial (speckind sk) /*@*/
   s->kind = SK_SPECIAL;
   s->info = (sinfo) dmalloc (sizeof (*s->info));
   s->info->spec = sk;
+  /*@-dependenttrans@*/
   return s;
+  /*@=dependenttrans@*/
 }
 
-static sRef srnothing = sRef_undefined;
-static sRef srinternal = sRef_undefined;
-static sRef srsystem = sRef_undefined;
-static sRef srspec = sRef_undefined;
+static /*@owned@*/ sRef srnothing = sRef_undefined;
+static /*@owned@*/ sRef srinternal = sRef_undefined;
+static /*@owned@*/ sRef srsystem = sRef_undefined;
+static /*@owned@*/ sRef srspec = sRef_undefined;
 
-sRef
+/*@dependent@*/ sRef
 sRef_makeNothing (void)
 {
   if (sRef_isInvalid (srnothing))
@@ -4033,9 +4473,7 @@ sRef_makeNothing (void)
       srnothing = sRef_makeSpecial (SR_NOTHING);
     }
 
-  /*@-retalias@*/
   return srnothing;
-  /*@=retalias@*/
 }
 
 sRef
@@ -4046,9 +4484,7 @@ sRef_makeInternalState (void)
       srinternal = sRef_makeSpecial (SR_INTERNAL);
     }
 
-  /*@-retalias@*/
   return srinternal;
-  /*@=retalias@*/
 }
 
 sRef
@@ -4059,9 +4495,7 @@ sRef_makeSpecState (void)
       srspec = sRef_makeSpecial (SR_SPECSTATE);
     }
 
-  /*@-retalias@*/
   return srspec;
-  /*@=retalias@*/
 }
 
 sRef
@@ -4072,31 +4506,32 @@ sRef_makeSystemState (void)
       srsystem = sRef_makeSpecial (SR_SYSTEM);
     }
 
-  /*@-retalias@*/
-  return (srsystem);
-  /*@=retalias@*/
+  return srsystem;
 }
 
-static sRef
-sRef_makeResultType (ctype ct)
+sRef
+sRef_makeGlobalMarker (void)
 {
-  sRef res = sRef_makeResult ();
-
-  res->type = ct;
-  return res;
+  sRef s = sRef_makeSpecial (SR_GLOBALMARKER);
+  llassert (valueTable_isUndefined (s->state));
+  s->state = context_createGlobalMarkerValueTable (stateInfo_undefined);
+  return s;
 }
 
 sRef
-sRef_makeResult ()
+sRef_makeResult (ctype c)
 {
-  sRef s = sRef_new ();
+  sRef s = sRef_newRef ();
   
   s->kind = SK_RESULT;
-  s->type = ctype_unknown;
+  s->type = c;
   s->defstate = SS_UNKNOWN; 
   s->aliaskind = AK_UNKNOWN;
-  s->nullstate = NS_UNKNOWN;
-  
+  sRef_setNullStateN (s, NS_UNKNOWN);
+  llassert (valueTable_isUndefined (s->state));
+  s->state = context_createValueTable (s, stateInfo_makeLoc (g_currentloc, SA_DECLARED));
+
+  DPRINTF (("Result: [%p] %s", s, sRef_unparseFull (s)));
   return s;
 }
 
@@ -4129,7 +4564,7 @@ sRef_isSpecState (sRef s)
 bool
 sRef_isResult (sRef s)
 {
-  return (sRef_isValid (s) && s->kind == SK_RESULT);
+  return (sRef_isReasonable (s) && s->kind == SK_RESULT);
 }
 
 bool
@@ -4138,10 +4573,16 @@ sRef_isSystemState (sRef s)
   return (sRef_isKindSpecial (s) && s->info->spec == SR_SYSTEM);
 }
 
+bool
+sRef_isGlobalMarker (sRef s)
+{
+  return (sRef_isKindSpecial (s) && s->info->spec == SR_GLOBALMARKER);
+}
+
 usymId
 sRef_getScopeIndex (sRef s)
 {
-  llassert (sRef_isValid (s));
+  llassert (sRef_isReasonable (s));
   llassert (sRef_isCvar (s));
 
   return (s->info->cvar->index);
@@ -4150,7 +4591,7 @@ sRef_getScopeIndex (sRef s)
 void
 sRef_makeSafe (sRef s)
 {
-  if (sRef_isValid (s)) 
+  if (sRef_isReasonable (s)) 
     {
       s->safe = TRUE;
     }
@@ -4159,7 +4600,7 @@ sRef_makeSafe (sRef s)
 void
 sRef_makeUnsafe (sRef s)
 {
-  if (sRef_isValid (s)) 
+  if (sRef_isReasonable (s)) 
     {
       s->safe = FALSE;
     }
@@ -4173,12 +4614,14 @@ sRef_makeUnsafe (sRef s)
 {
   if (sRef_isInvalid (s)) return (cstring_undefined);
 
-  return (message ("[%d] %q - %q [%s] { %q }", 
-		   (int) s,
+  return (message ("[%p] %q - %q { %q } [%s] { %q } < %q >", 
+		   s,
 		   sRef_unparseDebug (s), 
 		   sRef_unparseState (s),
+		   stateInfo_unparse (s->definfo),
 		   exkind_unparse (s->oexpkind),
-		   sRefSet_unparseDebug (s->deriv)));
+		   sRefSet_unparseDebug (s->deriv),
+		   valueTable_unparse (s->state)));
 }
 
 /*@unused@*/ cstring sRef_unparseDeep (sRef s)
@@ -4187,7 +4630,7 @@ sRef_makeUnsafe (sRef s)
 
   st = message ("%q:", sRef_unparseFull (s));
 
-  if (sRef_isValid (s))
+  if (sRef_isReasonable (s))
     {
       sRefSet_allElements (s->deriv, el)
 	{
@@ -4214,7 +4657,7 @@ sRef_makeUnsafe (sRef s)
 
   return (message ("%s.%s.%s.%s", 
 		   alkind_unparse (s->aliaskind), 
-		   nstate_unparse (s->nullstate),
+		   nstate_unparse (sRef_getNullState (s)),
 		   exkind_unparse (s->expkind),
 		   sstate_unparse (s->defstate)));
 }
@@ -4261,10 +4704,17 @@ bool sRef_hasNoStorage (sRef s)
 
 bool sRef_isStrictReadable (sRef s)
 {
-  return (ynm_toBoolStrict (sRef_isReadable (s)));
+  return (ynm_toBoolStrict (sRef_isValidLvalue (s)));
 }
 
-ynm sRef_isReadable (sRef s)
+/*
+** Is this what is does?
+** Returns YES if s can be used as an rvalue,
+**         MAYBE if its not clear
+**         NO if s cannot be safely used as an rvalue.
+*/
+
+ynm sRef_isValidLvalue (sRef s)
 {
   sstate ss;
 
@@ -4274,9 +4724,9 @@ ynm sRef_isReadable (sRef s)
   
   if (sRef_isConj (s) && s->defstate == SS_UNKNOWN)
     {
-      if (ynm_toBoolStrict (sRef_isReadable (sRef_getConjA (s))))
+      if (ynm_toBoolStrict (sRef_isValidLvalue (sRef_getConjA (s))))
 	{
-	  if (ynm_toBoolStrict (sRef_isReadable (sRef_getConjB (s))))
+	  if (ynm_toBoolStrict (sRef_isValidLvalue (sRef_getConjB (s))))
 	    {
 	      return YES;
 	    }
@@ -4284,7 +4734,7 @@ ynm sRef_isReadable (sRef s)
 	}
       else
 	{
-	  if (ynm_toBoolStrict (sRef_isReadable (sRef_getConjB (s))))
+	  if (ynm_toBoolStrict (sRef_isValidLvalue (sRef_getConjB (s))))
 	    {
 	      return MAYBE;
 	    }
@@ -4308,9 +4758,10 @@ ynm sRef_isReadable (sRef s)
 			    || ss == SS_FIXED 
 			    || ss == SS_RELDEF 
 			    || ss == SS_PDEFINED 
-			    || ss == SS_PARTIAL
+			    || ss == SS_PARTIAL 
 			    || ss == SS_SPECIAL
-			    || ss == SS_ALLOCATED
+			    || ss == SS_ALLOCATED 
+			    || ss == SS_KILLED /* evans 2001-05-26: added this for killed globals */
 			    || ss == SS_UNKNOWN));
     }
 }
@@ -4326,7 +4777,7 @@ static /*@exposed@*/ sRef whatUndefined (/*@exposed@*/ sRef fref, int depth)
 		("Warning: check definition limit exceeded, checking %q. "
 		 "This either means there is a variable with at least "
 		 "%d indirections apparent in the program text, or "
-		 "there is a bug in LCLint.",
+		 "there is a bug in Splint.",
 		 sRef_unparse (fref),
 		 MAXDEPTH),
 		g_currentloc);
@@ -4388,7 +4839,7 @@ static /*@exposed@*/ sRef whatUndefined (/*@exposed@*/ sRef fref, int depth)
 		    {
 		      sRef wdef = whatUndefined (fldref, depth + 1);
 
-		      if (sRef_isValid (wdef))
+		      if (sRef_isReasonable (wdef))
 			{
 			  return wdef;
 			}
@@ -4445,14 +4896,16 @@ static /*@exposed@*/ sRef whatUndefined (/*@exposed@*/ sRef fref, int depth)
   return sRef_undefined;
 }
 
-static bool checkDefined (sRef sr)
+static bool checkDefined (/*@temp@*/ sRef sr)
 {
+  /*@-temptrans@*/ /* the result from whatUndefined is lost */
   return (sRef_isInvalid (whatUndefined (sr, 0)));
+  /*@=temptrans@*/ 
 }
 
 bool sRef_isReallyDefined (sRef s)
 {
-  if (sRef_isValid (s))
+  if (sRef_isReasonable (s))
     {
       if (sRef_isAnyDefined (s))
 	{
@@ -4478,7 +4931,7 @@ bool sRef_isReallyDefined (sRef s)
 
 void sRef_showNotReallyDefined (sRef s)
 {
-  if (sRef_isValid (s))
+  if (sRef_isReasonable (s))
     {
       if (sRef_isAnyDefined (s))
 	{
@@ -4488,9 +4941,10 @@ void sRef_showNotReallyDefined (sRef s)
 	{
 	  if (sRef_isAllocated (s) || sRef_isPdefined (s))
 	    {
+	      /*@-temptrans@*/ /* the result of whatUndefined is lost */
 	      sRef ref = whatUndefined (s, 0);
 
-	      llassert (sRef_isValid (ref));
+	      llassert (sRef_isReasonable (ref));
 
 	      if (ref != s)
 		{
@@ -4520,34 +4974,40 @@ sstate sRef_getDefState (sRef s)
 
 void sRef_setDefState (sRef s, sstate defstate, fileloc loc)
 {
+  sRef_checkMutable (s);  
   sRef_setStateAux (s, defstate, loc);
 }
 
 static void sRef_clearAliasStateAux (sRef s, fileloc loc)
 {
+  sRef_checkMutable (s);  
   sRef_setAliasKind (s, AK_ERROR, loc);
 }
 
 void sRef_clearAliasState (sRef s, fileloc loc)
 {
+  sRef_checkMutable (s);  
   sRef_aliasSetComplete (sRef_clearAliasStateAux, s, loc);
 }
 
 void sRef_setAliasKindComplete (sRef s, alkind kind, fileloc loc)
 {
-  sRef_aliasSetCompleteParam (sRef_setAliasKind, s, kind, loc);
+  sRef_checkMutable (s);  
+  sRef_aliasSetCompleteAlkParam (sRef_setAliasKind, s, kind, loc); 
 }
 
 void sRef_setAliasKind (sRef s, alkind kind, fileloc loc)
 {
-  if (sRef_isValid (s))
+  sRef_checkMutable (s);  
+
+  if (sRef_isReasonable (s))
     {
       sRef_clearDerived (s);
 
       if ((kind != s->aliaskind && kind != s->oaliaskind)
 	  && fileloc_isDefined (loc))
 	{
-	  s->aliasinfo = alinfo_updateLoc (s->aliasinfo, loc);
+	  s->aliasinfo = stateInfo_updateLoc (s->aliasinfo, stateAction_fromAlkind (kind), loc);
 	}
       
       s->aliaskind = kind;
@@ -4556,7 +5016,9 @@ void sRef_setAliasKind (sRef s, alkind kind, fileloc loc)
 
 void sRef_setOrigAliasKind (sRef s, alkind kind)
 {
-  if (sRef_isValid (s))
+  sRef_checkMutable (s);  
+
+  if (sRef_isReasonable (s))
     {
       s->oaliaskind = kind;
     }
@@ -4564,7 +5026,7 @@ void sRef_setOrigAliasKind (sRef s, alkind kind)
 
 exkind sRef_getExKind (sRef s)
 {
-  if (sRef_isValid (s))
+  if (sRef_isReasonable (s))
     {
       return (s->expkind);
     }
@@ -4576,7 +5038,7 @@ exkind sRef_getExKind (sRef s)
 
 exkind sRef_getOrigExKind (sRef s)
 {
-  if (sRef_isValid (s))
+  if (sRef_isReasonable (s))
     {
       return (s->oexpkind);
     }
@@ -4588,16 +5050,19 @@ exkind sRef_getOrigExKind (sRef s)
 
 static void sRef_clearExKindAux (sRef s, fileloc loc)
 {
+  sRef_checkMutable (s);  
   sRef_setExKind (s, XO_UNKNOWN, loc);
 }
 
 void sRef_setObserver (sRef s, fileloc loc) 
 {
+  sRef_checkMutable (s);  
   sRef_setExKind (s, XO_OBSERVER, loc);
 }
 
 void sRef_setExposed (sRef s, fileloc loc) 
 {
+  sRef_checkMutable (s);  
   sRef_setExKind (s, XO_EXPOSED, loc);
 }
 
@@ -4608,11 +5073,13 @@ void sRef_clearExKindComplete (sRef s, fileloc loc)
 
 void sRef_setExKind (sRef s, exkind exp, fileloc loc)
 {
-  if (sRef_isValid (s))
+  sRef_checkMutable (s);
+
+  if (sRef_isReasonable (s))
     {
       if (s->expkind != exp)
 	{
-	  s->expinfo = alinfo_updateLoc (s->expinfo, loc);
+	  s->expinfo = stateInfo_updateLoc (s->expinfo, stateAction_fromExkind (exp), loc);
 	}
       
       s->expkind = exp;
@@ -4625,7 +5092,10 @@ void sRef_setExKind (sRef s, exkind exp, fileloc loc)
 
 static void sRef_copyRealDerived (sRef s1, sRef s2)
 {
-  if (sRef_isValid (s1) && sRef_isValid (s2))
+  DPRINTF (("Copy real: %s / %s", sRef_unparse (s1), sRef_unparse (s2)));
+  sRef_checkMutable (s1);
+
+  if (sRef_isReasonable (s1) && sRef_isReasonable (s2))
     {
       sRef sb = sRef_getRootBase (s1);
 
@@ -4633,7 +5103,7 @@ static void sRef_copyRealDerived (sRef s1, sRef s2)
 
       sRefSet_allElements (s2->deriv, el)
 	{
-	  if (sRef_isValid (el))
+	  if (sRef_isReasonable (el))
 	    {
 	      sRef rb = sRef_getRootBase (el);
 	      
@@ -4641,7 +5111,7 @@ static void sRef_copyRealDerived (sRef s1, sRef s2)
 		{
 		  sRef fb = sRef_fixDirectBase (el, s1);
 		  
-		  if (sRef_isValid (fb))
+		  if (sRef_isReasonable (fb))
 		    {
 		      sRef_copyRealDerived (fb, el);
 		      sRef_addDeriv (s1, fb);
@@ -4664,14 +5134,12 @@ void sRef_copyRealDerivedComplete (sRef s1, sRef s2)
 
 void sRef_setUndefined (sRef s, fileloc loc)
 {
-  if (sRef_isValid (s))
+  sRef_checkMutable (s);
+
+  if (sRef_isReasonable (s))
     {
       s->defstate = SS_UNDEFINED;
-
-      if (fileloc_isDefined (loc))
-	{
-	  s->definfo = alinfo_updateLoc (s->definfo, loc);
-	}
+      s->definfo = stateInfo_updateLoc (s->definfo, SA_UNDEFINED, loc);
 
       sRef_clearDerived (s);
     }
@@ -4679,25 +5147,39 @@ void sRef_setUndefined (sRef s, fileloc loc)
 
 static void sRef_setDefinedAux (sRef s, fileloc loc, bool clear)
 {
+  sRef_checkMutable (s);
   if (sRef_isInvalid (s)) return;
 
-  if (s->defstate != SS_DEFINED && fileloc_isDefined (loc))
-    {
-      s->definfo = alinfo_updateLoc (s->definfo, loc);
-    }
-  
+  DPRINTF (("Set defined: %s", sRef_unparseFull (s)));
+
+  s->definfo = stateInfo_updateLoc (s->definfo, SA_DEFINED, loc);  
   s->defstate = SS_DEFINED;
   
+  DPRINTF (("Set defined: %s", sRef_unparseFull (s)));
+
   /* e.g., if x is allocated, *x = 3 defines x */
   
   if (s->kind == SK_PTR)
     {
       sRef p = s->info->ref;
-      
-      if (p->defstate == SS_ALLOCATED)
+      sRef arr;
+
+      if (p->defstate == SS_ALLOCATED
+	  || p->defstate == SS_SPECIAL) /* evans 2001-07-12: shouldn't need this */
 	{
 	  sRef_setDefinedAux (p, loc, clear);
 	}
+
+      /* 
+      ** Defines a[0] also:
+      */
+
+      arr = sRef_findDerivedArrayFetch (p, FALSE, 0, FALSE);
+
+      if (sRef_isReasonable (arr))
+	{
+	  sRef_setDefinedAux (arr, loc, clear);
+	}
     }
   else if (s->kind == SK_ARRAYFETCH) 
     {
@@ -4706,11 +5188,12 @@ static void sRef_setDefinedAux (sRef s, fileloc loc, bool clear)
 	{
 	  sRef p = s->info->arrayfetch->arr;
 	  sRef ptr = sRef_constructPointer (p);
-	  
-	  if (sRef_isValid (ptr))
+
+	  if (sRef_isReasonable (ptr))
 	    {
 	      if (ptr->defstate == SS_ALLOCATED 
-		  || ptr->defstate == SS_UNDEFINED)
+		  || ptr->defstate == SS_UNDEFINED
+		  || ptr->defstate == SS_SPECIAL) /* evans 2001-07-12: shouldn't need this */
 		{
 		  sRef_setDefinedAux (ptr, loc, clear);
 		}
@@ -4720,7 +5203,8 @@ static void sRef_setDefinedAux (sRef s, fileloc loc, bool clear)
 	    {
 	      ;
 	    }
-	  else if (p->defstate == SS_ALLOCATED || p->defstate == SS_PDEFINED)
+	  else if (p->defstate == SS_ALLOCATED || p->defstate == SS_PDEFINED
+		   || p->defstate == SS_SPECIAL) /* evans 2001-07-12: shouldn't need this */
 	    {
 	      p->defstate = SS_DEFINED;
 	    }
@@ -4733,7 +5217,7 @@ static void sRef_setDefinedAux (sRef s, fileloc loc, bool clear)
     {
       sRef parent = s->info->field->rec;
       
-      if (sRef_isValid (parent))
+      if (sRef_isReasonable (parent))
 	{
 	  if (ctype_isUnion (ctype_realType (parent->type)))
 	    {
@@ -4758,11 +5242,24 @@ static void sRef_setDefinedAux (sRef s, fileloc loc, bool clear)
   if (clear)
     {
       sRef_clearDerived (s);
-    }  
+    } 
+  else
+    {
+      /* evans 2001-07-12: need to define the derived references */
+      sRefSet_elements (s->deriv, el)
+	{
+	  llassert (sRef_isReasonable (el));
+	  el->defstate = SS_DEFINED;
+	} end_sRefSet_elements ;
+    }
+  
+  DPRINTF (("Set defined: %s", sRef_unparseFull (s)));
 }
 
 static void sRef_setPartialDefined (sRef s, fileloc loc)
 {
+  sRef_checkMutable (s);
+
   if (!sRef_isPartial (s))
     {
       sRef_setDefined (s, loc);
@@ -4779,13 +5276,38 @@ void sRef_setDefinedComplete (sRef s, fileloc loc)
   sRef_innerAliasSetComplete (sRef_setDefined, s, loc);
 }
 
+void sRef_setDefinedCompleteDirect (sRef s, fileloc loc)
+{
+  sRefSet aliases;
+  
+  aliases = usymtab_allAliases (s);
+  DPRINTF (("Set defined complete: %s", sRef_unparseFull (s)));
+  DPRINTF (("All aliases: %s", sRefSet_unparseFull (aliases)));
+  
+  sRef_setDefined (s, loc);
+
+  sRefSet_realElements (aliases, current)
+    {
+      if (sRef_isReasonable (current))
+	{
+	  current = sRef_updateSref (current);
+	  sRef_setDefined (current, loc);
+	}
+    } end_sRefSet_realElements;
+  
+  sRefSet_free (aliases);
+  sRef_innerAliasSetComplete (sRef_setDefined, s, loc);
+}
+
 void sRef_setDefined (sRef s, fileloc loc)
 {
+  sRef_checkMutable (s);
   sRef_setDefinedAux (s, loc, TRUE);
 }
 
 static void sRef_setDefinedNoClear (sRef s, fileloc loc)
 {
+  sRef_checkMutable (s);
   DPRINTF (("Defining: %s", sRef_unparseFull (s)));
   sRef_setDefinedAux (s, loc, FALSE);
   DPRINTF (("==> %s", sRef_unparseFull (s)));
@@ -4793,6 +5315,7 @@ static void sRef_setDefinedNoClear (sRef s, fileloc loc)
 
 void sRef_setDefinedNCComplete (sRef s, fileloc loc)
 {
+  sRef_checkMutable (s);
   DPRINTF (("Set Defined Complete: %s", sRef_unparseFull (s)));
   sRef_innerAliasSetComplete (sRef_setDefinedNoClear, s, loc);
   DPRINTF (("==> %s", sRef_unparseFull (s)));
@@ -4805,7 +5328,7 @@ static bool sRef_isDeepUnionField (sRef s)
 
 bool sRef_isUnionField (sRef s)
 {
-  if (sRef_isValid (s) && s->kind == SK_FIELD)
+  if (sRef_isReasonable (s) && s->kind == SK_FIELD)
     {
       /*
        ** defining one field of a union defines the union
@@ -4813,7 +5336,7 @@ bool sRef_isUnionField (sRef s)
       
       sRef base = s->info->field->rec;
 
-      if (sRef_isValid (base))
+      if (sRef_isReasonable (base))
 	{
 	  return (ctype_isUnion (ctype_realType (base->type)));
 	}
@@ -4824,7 +5347,8 @@ bool sRef_isUnionField (sRef s)
 
 void sRef_setPdefined (sRef s, fileloc loc)
 {
-  if (sRef_isValid (s) && !sRef_isPartial (s))
+  sRef_checkMutable (s);
+  if (sRef_isReasonable (s) && !sRef_isPartial (s))
     {
       sRef base = sRef_getBaseSafe (s);
 
@@ -4833,22 +5357,19 @@ void sRef_setPdefined (sRef s, fileloc loc)
 	  return;
 	}
       
-      if (s->defstate != SS_PDEFINED && fileloc_isDefined (loc))
-	{
-	  s->definfo = alinfo_updateLoc (s->definfo, loc);
-	}
-
+      s->definfo = stateInfo_updateLoc (s->definfo, SA_PDEFINED, loc);
       s->defstate = SS_PDEFINED;
       
       /* e.g., if x is allocated, *x = 3 defines x */
       
-      while (sRef_isValid (base) && sRef_isKnown (base))
+      while (sRef_isReasonable (base) && sRef_isKnown (base))
 	{
 	  if (base->defstate == SS_DEFINED)
 	    { 
 	      sRef nb;
-
-	      	      base->defstate = SS_PDEFINED; 
+	      
+	      DPRINTF (("set pdefined: %s", sRef_unparseFull (base)));
+	      base->defstate = SS_PDEFINED; 
 	      nb = sRef_getBaseSafe (base); 
 	      base = nb;
 	    }
@@ -4862,13 +5383,18 @@ void sRef_setPdefined (sRef s, fileloc loc)
 
 static void sRef_setStateAux (sRef s, sstate ss, fileloc loc)
 {
-  if (sRef_isValid (s))
+  sRef_checkMutable (s);
+
+  DPRINTF (("Set state: %s => %s", sRef_unparseFull (s), sstate_unparse (ss)));
+
+  if (sRef_isReasonable (s))
     {
       /* if (s->defstate == SS_RELDEF) return; */
 
       if (s->defstate != ss && fileloc_isDefined (loc))
 	{
-	  s->definfo = alinfo_updateLoc (s->definfo, loc);
+	  s->definfo = stateInfo_updateLoc (s->definfo, 
+					    stateAction_fromSState (ss), loc);
 	}
 
       s->defstate = ss;
@@ -4878,14 +5404,14 @@ static void sRef_setStateAux (sRef s, sstate ss, fileloc loc)
 	{
 	  sRef base = sRef_getBaseSafe (s);
 	  
-	  while (sRef_isValid (base) && sRef_isKnown (base))
+	  while (sRef_isReasonable (base) && sRef_isKnown (base))
 	    {
 	      if (base->defstate == SS_DEFINED) 
 		{ 
 		  sRef nb;
-		  
+
+		  DPRINTF (("set pdefined: %s", sRef_unparseFull (s)));		  
 		  base->defstate = SS_PDEFINED; 
-		  
 		  nb = sRef_getBaseSafe (base); 
 		  base = nb;
 		}
@@ -4895,8 +5421,7 @@ static void sRef_setStateAux (sRef s, sstate ss, fileloc loc)
 		}
 	    }
 	}
-
-          }
+    }
 }
 
 void sRef_setAllocatedComplete (sRef s, fileloc loc)
@@ -4906,16 +5431,14 @@ void sRef_setAllocatedComplete (sRef s, fileloc loc)
 
 static void sRef_setAllocatedShallow (sRef s, fileloc loc)
 {
-  if (sRef_isValid (s))
+  sRef_checkMutable (s);
+
+  if (sRef_isReasonable (s))
     {
       if (s->defstate == SS_DEAD || s->defstate == SS_UNDEFINED)
 	{
 	  s->defstate = SS_ALLOCATED;
-	  
-	  if (fileloc_isDefined (loc))
-	    {
-	      s->definfo = alinfo_updateLoc (s->definfo, loc);
-	    }
+	  s->definfo = stateInfo_updateLoc (s->definfo, SA_ALLOCATED, loc);
 	}
     }
 }
@@ -4927,21 +5450,25 @@ void sRef_setAllocatedShallowComplete (sRef s, fileloc loc)
 
 void sRef_setAllocated (sRef s, fileloc loc)
 {
+  sRef_checkMutable (s);
   sRef_setStateAux (s, SS_ALLOCATED, loc);
-  }
+}
 
 void sRef_setPartial (sRef s, fileloc loc)
 {
+  sRef_checkMutable (s);
   sRef_setStateAux (s, SS_PARTIAL, loc);
-  }
+}
 
 void sRef_setShared (sRef s, fileloc loc)
 {
-  if (sRef_isValid (s))
+  sRef_checkMutable (s);
+
+  if (sRef_isReasonable (s))
     {
       if (s->aliaskind != AK_SHARED && fileloc_isDefined (loc))
 	{
-	  s->aliasinfo = alinfo_updateLoc (s->aliasinfo, loc);
+	  s->aliasinfo = stateInfo_updateLoc (s->aliasinfo, SA_SHARED, loc);
 	}
 
       s->aliaskind = AK_SHARED;
@@ -4949,58 +5476,73 @@ void sRef_setShared (sRef s, fileloc loc)
     }
 }
 
-void sRef_setLastReference (sRef s, sRef ref, fileloc loc)
+void sRef_setLastReference (sRef s, /*@exposed@*/ sRef ref, fileloc loc)
 {
-  if (sRef_isValid (s))
+  sRef_checkMutable (s);
+
+  if (sRef_isReasonable (s))
     {
       s->aliaskind = sRef_getAliasKind (ref);
-      s->aliasinfo = alinfo_updateRefLoc (s->aliasinfo, ref, loc);
+      s->aliasinfo = stateInfo_updateRefLoc (s->aliasinfo, ref, stateAction_fromAlkind (s->aliaskind), loc);
     }
 }
 
 static
 void sRef_setNullStateAux (/*@notnull@*/ sRef s, nstate ns, fileloc loc)
 {
- s->nullstate = ns;
+  sRef_checkMutable (s);
+  s->nullstate = ns;
+  sRef_resetAliasKind (s);
 
- if (fileloc_isDefined (loc))
-   {
-     s->nullinfo = alinfo_updateLoc (s->nullinfo, loc);
-   }
+  if (fileloc_isDefined (loc))
+    {
+      s->nullinfo = stateInfo_updateLoc (s->nullinfo, stateAction_fromNState (ns), loc);
+    }
+}
+
+void sRef_setNotNull (sRef s, fileloc loc)
+{
+  if (sRef_isReasonable (s))
+    {
+      sRef_setNullStateAux (s, NS_NOTNULL, loc);
+    }
 }
 
-void sRef_setNotNull (sRef s, fileloc loc)
+void sRef_setNullStateN (sRef s, nstate n)
 {
-  if (sRef_isValid (s))
+  if (sRef_isReasonable (s))
     {
-      sRef_setNullStateAux (s, NS_NOTNULL, loc);
+      sRef_checkMutable (s);
+      s->nullstate = n;
+      sRef_resetAliasKind (s);
     }
 }
 
 void sRef_setNullState (sRef s, nstate n, fileloc loc)
 {
-  if (sRef_isValid (s))
+  if (sRef_isReasonable (s))
     {
       sRef_setNullStateAux (s, n, loc);
     }
 }
 
-void sRef_setNullTerminatedStateInnerComplete (sRef s, struct _bbufinfo b, /*@unused@*/ fileloc loc) {
-   
+void sRef_setNullTerminatedStateInnerComplete (sRef s, struct s_bbufinfo b, /*@unused@*/ fileloc loc) 
+{
   switch (b.bufstate) {
-     case BB_NULLTERMINATED:
-	  sRef_setNullTerminatedState (s);
-          sRef_setLen (s, b.len);
-          break;
-     case BB_POSSIBLYNULLTERMINATED:
-          sRef_setPossiblyNullTerminatedState(s);
-          break;
-     case BB_NOTNULLTERMINATED:
-          sRef_setNotNullTerminatedState (s);
-          break;
+  case BB_NULLTERMINATED:
+    sRef_setNullTerminatedState (s);
+    sRef_setLen (s, b.len);
+    break;
+  case BB_POSSIBLYNULLTERMINATED:
+    sRef_setPossiblyNullTerminatedState(s);
+    break;
+  case BB_NOTNULLTERMINATED:
+    sRef_setNotNullTerminatedState (s);
+    break;
   }
-  sRef_setSize (s, b.size);
 
+  sRef_setSize (s, b.size);
+  
   /* PL: TO BE DONE : Aliases are not modified right now, have to be similar to
    * setNullStateInnerComplete.
    */
@@ -5008,8 +5550,10 @@ void sRef_setNullTerminatedStateInnerComplete (sRef s, struct _bbufinfo b, /*@un
 
 void sRef_setNullStateInnerComplete (sRef s, nstate n, fileloc loc)
 {
+  DPRINTF (("Set null state: %s", nstate_unparse (n)));
+  
   sRef_setNullState (s, n, loc);
-
+  
   switch (n)
     {
     case NS_POSNULL:
@@ -5044,7 +5588,7 @@ void sRef_setNullStateInnerComplete (sRef s, nstate n, fileloc loc)
 
 void sRef_setPosNull (sRef s, fileloc loc)
 {
-  if (sRef_isValid (s))
+  if (sRef_isReasonable (s))
     {
       sRef_setNullStateAux (s, NS_POSNULL, loc);
     }
@@ -5052,7 +5596,7 @@ void sRef_setPosNull (sRef s, fileloc loc)
   
 void sRef_setDefNull (sRef s, fileloc loc)
 {
-  if (sRef_isValid (s))
+  if (sRef_isReasonable (s))
     {
       sRef_setNullStateAux (s, NS_DEFNULL, loc);
     }
@@ -5060,7 +5604,7 @@ void sRef_setDefNull (sRef s, fileloc loc)
 
 void sRef_setNullUnknown (sRef s, fileloc loc)
 {
-  if (sRef_isValid (s))
+  if (sRef_isReasonable (s))
     {
       sRef_setNullStateAux (s, NS_UNKNOWN, loc);
     }
@@ -5068,67 +5612,75 @@ void sRef_setNullUnknown (sRef s, fileloc loc)
 
 void sRef_setNullError (sRef s)
 {
-  if (sRef_isValid (s))
+  if (sRef_isReasonable (s) && !sRef_isConst (s))
     {
       sRef_setNullStateAux (s, NS_UNKNOWN, fileloc_undefined);
     }
 }
 
-void sRef_setNullErrorLoc (sRef s, /*@unused@*/ fileloc loc)
+void sRef_setNullErrorLoc (sRef s, fileloc loc)
 {
-  sRef_setNullError (s);
+  if (sRef_isReasonable (s) && !sRef_isConst (s))
+    {
+      sRef_setNullStateAux (s, NS_UNKNOWN, loc);
+    }
 }
 
 void sRef_setOnly (sRef s, fileloc loc)
 {
-  if (sRef_isValid (s) && s->aliaskind != AK_ONLY)
+  if (sRef_isReasonable (s) && s->aliaskind != AK_ONLY)
     {
+      sRef_checkMutable (s);
       s->aliaskind = AK_ONLY;
-      s->aliasinfo = alinfo_updateLoc (s->aliasinfo, loc);
-          }
+      s->aliasinfo = stateInfo_updateLoc (s->aliasinfo, SA_ONLY, loc);
+    }
 }
 
 void sRef_setDependent (sRef s, fileloc loc)
 {
-  if (sRef_isValid (s) && !sRef_isConst (s) && (s->aliaskind != AK_DEPENDENT))
+  if (sRef_isReasonable (s) && !sRef_isConst (s) && (s->aliaskind != AK_DEPENDENT))
     {
+      sRef_checkMutable (s);
+      DPRINTF (("Setting dependent: %s", sRef_unparseFull (s)));
       s->aliaskind = AK_DEPENDENT;
-      s->aliasinfo = alinfo_updateLoc (s->aliasinfo, loc);
-          }
+      s->aliasinfo = stateInfo_updateLoc (s->aliasinfo, SA_DEPENDENT, loc);
+    }
 }
 
 void sRef_setOwned (sRef s, fileloc loc)
 {
-  if (sRef_isValid (s) && !sRef_isConst (s) && (s->aliaskind != AK_OWNED))
+  if (sRef_isReasonable (s) && !sRef_isConst (s) && (s->aliaskind != AK_OWNED))
     {
+      sRef_checkMutable (s);
       s->aliaskind = AK_OWNED;
-      s->aliasinfo = alinfo_updateLoc (s->aliasinfo, loc);
-          }
+      s->aliasinfo = stateInfo_updateLoc (s->aliasinfo, SA_OWNED, loc);
+    }
 }
 
 void sRef_setKept (sRef s, fileloc loc)
 {
-  if (sRef_isValid (s) && !sRef_isConst (s) && (s->aliaskind != AK_KEPT))
+  if (sRef_isReasonable (s) && !sRef_isConst (s) && (s->aliaskind != AK_KEPT))
     {
       sRef base = sRef_getBaseSafe (s);  
-      
-      while (sRef_isValid (base) && sRef_isKnown (base))
+ 
+      while (sRef_isReasonable (base) && sRef_isKnown (base))
 	{
 	  if (base->defstate == SS_DEFINED) 
 	    {
+	      sRef_checkMutable (base);
 	      base->defstate = SS_PDEFINED; 
-	      	      base = sRef_getBaseSafe (base); 
+	      base = sRef_getBaseSafe (base); 
 	    }
 	  else 
 	    {
 	      break; 
 	    }
-
 	}
 
+      sRef_checkMutable (s);
       s->aliaskind = AK_KEPT;
-      s->aliasinfo = alinfo_updateLoc (s->aliasinfo, loc);
-          }
+      s->aliasinfo = stateInfo_updateLoc (s->aliasinfo, SA_KEPT, loc);
+    }
 }
 
 static void sRef_setKeptAux (sRef s, fileloc loc)
@@ -5159,10 +5711,12 @@ void sRef_setDependentComplete (sRef s, fileloc loc)
 
 void sRef_setFresh (sRef s, fileloc loc)
 {
-  if (sRef_isValid (s))
+  if (sRef_isReasonable (s) && !sRef_isConst (s))
     {
+      sRef_checkMutable (s);
       s->aliaskind = AK_FRESH;
-      s->aliasinfo = alinfo_updateLoc (s->aliasinfo, loc);
+      s->aliasinfo = stateInfo_updateLoc (s->aliasinfo, SA_CREATED, loc);
+      DPRINTF (("SetFresh: %s", sRef_unparseFull (s)));
     }
 }
 
@@ -5170,14 +5724,16 @@ void sRef_kill (sRef s, fileloc loc)
 {
   DPRINTF (("Kill: %s", sRef_unparseFull (s)));
 
-  if (sRef_isValid (s) && !sRef_isShared (s) && !sRef_isConst (s))
+  if (sRef_isReasonable (s) && !sRef_isShared (s) && !sRef_isConst (s))
     {
       sRef base = sRef_getBaseSafe (s);  
-      
-      while (sRef_isValid (base) && sRef_isKnown (base))
+      sRef_checkMutable (s);
+	
+      while (sRef_isReasonable (base) && sRef_isKnown (base))
 	{
 	  if (base->defstate == SS_DEFINED) 
 	    {
+	      sRef_checkMutable (base);
 	      base->defstate = SS_PDEFINED; 
 	      base = sRef_getBaseSafe (base); 
 	    }
@@ -5185,42 +5741,43 @@ void sRef_kill (sRef s, fileloc loc)
 	    {
 	      break; 
 	    }
-
 	}
       
       s->aliaskind = s->oaliaskind;
       s->defstate = SS_DEAD;
-      s->definfo = alinfo_updateLoc (s->definfo, loc);
-
+      s->definfo = stateInfo_updateLoc (s->definfo, SA_KILLED, loc);
+      DPRINTF (("State info: %s", stateInfo_unparse (s->definfo)));
       sRef_clearDerived (s);
     }
 }
 
 void sRef_maybeKill (sRef s, fileloc loc)
 {
-        
-  if (sRef_isValid (s))
+  if (sRef_isReasonable (s))
     {
       sRef base = sRef_getBaseSafe (s);  
-
+      sRef_checkMutable (s);
             
-      while (sRef_isValid (base) && sRef_isKnown (base))
+      while (sRef_isReasonable (base) && sRef_isKnown (base))
 	{
 	  if (base->defstate == SS_DEFINED || base->defstate == SS_RELDEF)
 	    {
+	      sRef_checkMutable (base);
 	      base->defstate = SS_PDEFINED; 
-	      	      base = sRef_getBaseSafe (base); 
+	      base = sRef_getBaseSafe (base); 
 	    }
 	  else 
 	    {
-	      	      break; 
+	      break; 
 	    }
 	  
 	}
       
       s->aliaskind = s->oaliaskind;
       s->defstate = SS_HOFFA; 
-      s->definfo = alinfo_updateLoc (s->definfo, loc);
+      s->definfo = stateInfo_updateLoc (s->definfo, SA_PKILLED, loc);
+      DPRINTF (("State info: %s / %s", sRef_unparse (s), 
+		stateInfo_unparse (s->definfo)));
       sRef_clearDerived (s); 
     }
 
@@ -5232,7 +5789,7 @@ void sRef_maybeKill (sRef s, fileloc loc)
 
 static void sRef_killAux (sRef s, fileloc loc)
 {
-  if (sRef_isValid (s) && !sRef_isShared (s))
+  if (sRef_isReasonable (s) && !sRef_isShared (s))
     {
       if (sRef_isUnknownArrayFetch (s))
 	{
@@ -5240,8 +5797,8 @@ static void sRef_killAux (sRef s, fileloc loc)
 	}
       else
 	{
-	  	  sRef_kill (s, loc);
-	  	}
+	  sRef_kill (s, loc);
+	}
     }
 }
 
@@ -5268,7 +5825,7 @@ static bool sRef_equivalent (sRef s1, sRef s2)
 {
   sRef ret;
 
-  if (sRef_isValid (s))
+  if (sRef_isReasonable (s))
     {
       bool old = inFunction;
 
@@ -5295,26 +5852,29 @@ static bool sRef_equivalent (sRef s1, sRef s2)
 
 sRef sRef_copy (sRef s)
 {
-  if (sRef_isKindSpecial (s))
+  if (sRef_isKindSpecial (s) && !sRef_isGlobalMarker (s))
     {
       /*@-retalias@*/
-      return s; /* don't copy specials */
+      return s; /* don't copy specials (except for global markers) */
       /*@=retalias@*/
     }
-  
-  if (sRef_isValid (s))
+
+  if (sRef_isReasonable (s))
     {
       sRef t = sRef_alloc ();
 
+      DPRINTF (("Copying: [%p] %s", s, sRef_unparse (s)));
+      DPRINTF (("Full: %s", sRef_unparseFull (s)));
+
       t->kind = s->kind;
       t->safe = s->safe;
       t->modified = s->modified;
+      t->immut = FALSE; /* Note mutability is not copied. */
       t->type = s->type;
+      t->val = multiVal_copy (s->val);
 
-            t->info = sinfo_copy (s);
-      
+      t->info = sinfo_copy (s);
       t->defstate = s->defstate;
-
       t->nullstate = s->nullstate;
  
       /* start modifications */
@@ -5329,13 +5889,15 @@ sRef sRef_copy (sRef s)
       t->expkind = s->expkind;
       t->oexpkind = s->oexpkind;
 
-      t->aliasinfo = alinfo_copy (s->aliasinfo);
-      t->definfo = alinfo_copy (s->definfo);
-      t->nullinfo = alinfo_copy (s->nullinfo);
-      t->expinfo = alinfo_copy (s->expinfo);
+      t->nullinfo = stateInfo_copy (s->nullinfo);
+      t->aliasinfo = stateInfo_copy (s->aliasinfo);
+      t->definfo = stateInfo_copy (s->definfo);
+      t->expinfo = stateInfo_copy (s->expinfo);
 
       t->deriv = sRefSet_newDeepCopy (s->deriv);
+      t->state = valueTable_copy (s->state);
       
+      DPRINTF (("Made copy: %s => %s", sRef_unparseFull (s), sRef_unparseFull (t)));
       return t;
     }
   else
@@ -5363,7 +5925,7 @@ bool sRef_isAddress (sRef s)
 
 bool sRef_isThroughArrayFetch (sRef s)
 {
-  if (sRef_isValid (s))
+  if (sRef_isReasonable (s))
     {
       sRef tref = s;
 
@@ -5373,12 +5935,12 @@ bool sRef_isThroughArrayFetch (sRef s)
 
 	  if (sRef_isArrayFetch (tref)) 
 	    {
-	      	      return TRUE;
+	      return TRUE;
 	    }
 	  
 	  lt = sRef_getBase (tref);
 	  tref = lt;
-	} while (sRef_isValid (tref));
+	} while (sRef_isReasonable (tref));
     } 
 
   return FALSE;
@@ -5466,7 +6028,7 @@ bool sRef_isDirectParam (sRef s)
   return ((s->kind == SK_CVAR) &&
 	  (s->info->cvar->lexlevel == functionScope) &&
 	  (context_inFunction () && 
-	   (s->info->cvar->index <= uentryList_size (context_getParams ()))));
+	   (s->info->cvar->index <= usymId_fromInt (uentryList_size (context_getParams ())))));
 }
 
 bool sRef_isPointer (sRef s)
@@ -5483,7 +6045,7 @@ bool sRef_isReference (sRef s)
 {
   PREDTEST (sRef_isReference, s);
 
-  return (sRef_isPointer (s) || sRef_isIndex (s) || sRef_isGlobal (s)
+  return (sRef_isPointer (s) || sRef_isIndex (s) || sRef_isFileOrGlobalScope (s)
 	  || (sRef_isField (s) && (sRef_isReference (s->info->field->rec))));
 }
 
@@ -5493,7 +6055,7 @@ bool sRef_isIReference (sRef s)
 	  || sRef_isField (s) || sRef_isArrayFetch (s));
 }
 
-bool sRef_isGlobal (sRef s)
+bool sRef_isFileOrGlobalScope (sRef s)
 {
   return (sRef_isCvar (s) && (s->info->cvar->lexlevel <= fileScope));
 }
@@ -5510,7 +6072,7 @@ bool sRef_isFileStatic (sRef s)
 
 bool sRef_isAliasCheckedGlobal (sRef s)
 {
-  if (sRef_isGlobal (s))
+  if (sRef_isFileOrGlobalScope (s))
     {
       uentry ue = sRef_getUentry (s);
 
@@ -5526,31 +6088,48 @@ void sRef_free (/*@only@*/ sRef s)
 {
   if (s != sRef_undefined && s->kind != SK_SPECIAL)
     {
-      alinfo_free (s->expinfo);
-      alinfo_free (s->aliasinfo);
-      alinfo_free (s->definfo);
-      alinfo_free (s->nullinfo);
+      DPRINTF (("Free sref: [%p]", s));
+
+      sRef_checkValid (s);
       
+      multiVal_free (s->val); /* evans 2002-07-12 */
+
+      stateInfo_free (s->expinfo);
+      stateInfo_free (s->aliasinfo);
+      stateInfo_free (s->definfo);
+      stateInfo_free (s->nullinfo);
+
       sRefSet_free (s->deriv);
       s->deriv = sRefSet_undefined;
+
+      valueTable_free (s->state); 
       sinfo_free (s);
       
-      sfree (s); 
+      
+      /* drl added to help locate use after release*/
+      s->expinfo = stateInfo_undefined;
+      s->aliasinfo = stateInfo_undefined;
+      s->definfo = stateInfo_undefined;
+      s->nullinfo = stateInfo_undefined;
+
+      sfree (s);
     }
 }
 
 void sRef_setType (sRef s, ctype t)
 {
-  if (sRef_isValid (s))
+  if (sRef_isReasonable (s))
     {
+      sRef_checkMutable (s); 
       s->type = t;
     }
 }
 
 void sRef_setTypeFull (sRef s, ctype t)
 {
-  if (sRef_isValid (s))
+  if (sRef_isReasonable (s))
     {
+      sRef_checkMutable (s);
       s->type = t;
 
       sRefSet_allElements (s->deriv, current)
@@ -5561,7 +6140,7 @@ void sRef_setTypeFull (sRef s, ctype t)
 }
 
 /*@exposed@*/ sRef
-  sRef_buildField (sRef rec, /*@dependent@*/ cstring f)
+  sRef_buildField (/*@exposed@*/ sRef rec, /*@dependent@*/ cstring f)
 {
   return (sRef_buildNCField (rec, f)); 
 }
@@ -5569,13 +6148,23 @@ void sRef_setTypeFull (sRef s, ctype t)
 static /*@exposed@*/ sRef
 sRef_findDerivedField (/*@notnull@*/ sRef rec, cstring f)
 {
-  sRefSet_allElements (rec->deriv, sr)
+  sRefSet_allElements (sRef_derivedFields (rec), sr)
     {
-      if (sRef_isValid (sr))
+      if (sRef_isReasonable (sr))
 	{
-	  if (sr->kind == SK_FIELD && cstring_equal (sr->info->field->field, f))
+	  if (sRef_isReasonable (sr))
 	    {
-	      return sr;
+	      if (sr->info != NULL) 
+		{
+		  if (sr->kind == SK_FIELD && cstring_equal (sr->info->field->field, f))
+		    {
+		      return sr;
+		    }
+		}
+	    }
+	  else
+	    {
+	      llcontbug (message ("Invalid sRef as derived field of %s", sRef_unparse (rec)));
 	    }
 	}
     } end_sRefSet_allElements;
@@ -5583,10 +6172,9 @@ sRef_findDerivedField (/*@notnull@*/ sRef rec, cstring f)
   return sRef_undefined;
 }
 
-/*@dependent@*/ /*@observer@*/ sRefSet
-  sRef_derivedFields (sRef rec)
+/*@dependent@*/ /*@observer@*/ sRefSet sRef_derivedFields (/*@temp@*/ sRef rec)
 {
-  if (sRef_isValid (rec))
+  if (sRef_isReasonable (rec))
     {
       sRefSet ret;
       ret = rec->deriv;
@@ -5601,11 +6189,11 @@ sRef_findDerivedField (/*@notnull@*/ sRef rec, cstring f)
 static /*@exposed@*/ sRef
   sRef_findDerivedPointer (sRef s)
 {
-  if (sRef_isValid (s))
+  if (sRef_isReasonable (s))
     {
       sRefSet_realElements (s->deriv, sr)
 	{
-	  if (sRef_isValid (sr) && sr->kind == SK_PTR)
+	  if (sRef_isReasonable (sr) && sr->kind == SK_PTR)
 	    {
 	      return sr;
 	    }
@@ -5618,7 +6206,7 @@ static /*@exposed@*/ sRef
 bool
 sRef_isUnknownArrayFetch (sRef s)
 {
-  return (sRef_isValid (s) 
+  return (sRef_isReasonable (s) 
 	  && s->kind == SK_ARRAYFETCH
 	  && !s->info->arrayfetch->indknown);
 }
@@ -5631,7 +6219,7 @@ sRef_findDerivedArrayFetch (/*@notnull@*/ sRef s, bool isknown, int idx, bool de
     {
       sRefSet_realElements (s->deriv, sr)
 	{
-	  if (sRef_isValid (sr)
+	  if (sRef_isReasonable (sr)
 	      && sr->kind == SK_ARRAYFETCH
 	      && sr->info->arrayfetch->indknown
 	      && (sr->info->arrayfetch->ind == idx))
@@ -5644,7 +6232,7 @@ sRef_findDerivedArrayFetch (/*@notnull@*/ sRef s, bool isknown, int idx, bool de
     {
       sRefSet_realElements (s->deriv, sr)
 	{
-	  if (sRef_isValid (sr)
+	  if (sRef_isReasonable (sr)
 	      && sr->kind == SK_ARRAYFETCH
 	      && (!sr->info->arrayfetch->indknown
 		  || (sr->info->arrayfetch->indknown && 
@@ -5673,6 +6261,9 @@ sRef_buildNCField (/*@exposed@*/ sRef rec, /*@exposed@*/ cstring f)
 {
   sRef s;
 
+  DPRINTF (("Build nc field: %s / %s",
+	    sRef_unparseFull (rec), f));
+
   if (sRef_isInvalid (rec))
     {
       return sRef_undefined;
@@ -5684,28 +6275,32 @@ sRef_buildNCField (/*@exposed@*/ sRef rec, /*@exposed@*/ cstring f)
 
   s = sRef_findDerivedField (rec, f);
   
-  if (sRef_isValid (s))
+  if (sRef_isReasonable (s))
     {
-            return s;
+      return s;
     }
   else
     {
       ctype ct = ctype_realType (rec->type);
-
-      s = sRef_new ();      
+      
+      DPRINTF (("Field of: %s", sRef_unparse (rec)));
+      
+      s = sRef_newRef ();      
       s->kind = SK_FIELD;
       s->info = (sinfo) dmalloc (sizeof (*s->info));
       s->info->field = (fldinfo) dmalloc (sizeof (*s->info->field));
       s->info->field->rec = rec;
       s->info->field->field = f; /* doesn't copy f */
       
-      
       if (ctype_isKnown (ct) && ctype_isSU (ct))
 	{
 	  uentry ue = uentryList_lookupField (ctype_getFields (ct), f);
 	
 	  if (!uentry_isUndefined (ue))
 	    {
+	      DPRINTF (("lookup: %s for %s", uentry_unparseFull (ue),
+			ctype_unparse (ct)));
+	      
 	      s->type = uentry_getType (ue);
 
 	      if (ctype_isMutable (s->type)
@@ -5722,15 +6317,17 @@ sRef_buildNCField (/*@exposed@*/ sRef rec, /*@exposed@*/ cstring f)
 	      if (sRef_isStateDefined (rec) || sRef_isStateUnknown (rec) 
 		  || sRef_isPdefined (rec))
 		{
-		  		  sRef_setStateFromUentry (s, ue);
-		  		}
+		  sRef_setStateFromUentry (s, ue);
+		}
 	      else
 		{
 		  sRef_setPartsFromUentry (s, ue);
-		  		}
-
+		}
+	      
 	      s->oaliaskind = s->aliaskind;
 	      s->oexpkind = s->expkind;
+
+	      DPRINTF (("sref: %s", sRef_unparseFull (s)));
 	    }
 	  else
 	    {
@@ -5784,11 +6381,12 @@ sRef_buildNCField (/*@exposed@*/ sRef rec, /*@exposed@*/ cstring f)
 	  
 	  if (ctype_isArray (rt) || ctype_isSU (rt))
 	    {
-	      	      s->defstate = SS_ALLOCATED;
+	      s->defstate = SS_ALLOCATED;
 	    }
 	}
 
       sRef_addDeriv (rec, s);
+      DPRINTF (("Add deriv: %s", sRef_unparseFull (rec)));
 
       if (ctype_isInt (s->type) && cstring_equal (f, REFSNAME))
 	{
@@ -5796,14 +6394,15 @@ sRef_buildNCField (/*@exposed@*/ sRef rec, /*@exposed@*/ cstring f)
 	  s->oaliaskind = AK_REFS;
 	}
 
-            return s;
+      DPRINTF (("Build field ==> %s", sRef_unparseFull (s)));
+      return s;
     }
 }
 
 bool
 sRef_isStackAllocated (sRef s)
 {
-  return (sRef_isValid(s) 
+  return (sRef_isReasonable(s) 
 	  && s->defstate == SS_ALLOCATED && ctype_isStackAllocated (s->type));
 }
 	  
@@ -5811,12 +6410,18 @@ static
 void sRef_setArrayFetchState (/*@notnull@*/ /*@exposed@*/ sRef s, 
 			      /*@notnull@*/ /*@exposed@*/ sRef arr)
 {
+  sRef_checkMutable (s);
+
   if (ctype_isRealAP (arr->type))
     {
       s->type = ctype_baseArrayPtr (arr->type);
     }
 
   /* a hack, methinks... makeArrayFetch (&a[0]) ==> a[] */
+  /* evans - 2001-08-27: not sure where this was necessary - it
+  ** causes an assertion in in aliasCheckPred to fail.
+  */
+
   if (sRef_isAddress (arr)) 
     {
       sRef t = arr->info->ref;
@@ -5829,17 +6434,17 @@ void sRef_setArrayFetchState (/*@notnull@*/ /*@exposed@*/ sRef s,
   else if (ctype_isRealPointer (arr->type))
     {
       sRef sp = sRef_findDerivedPointer (arr);
-
       
-      if (sRef_isValid (sp))
+      if (sRef_isReasonable (sp))
 	{
 	  
 	  if (ctype_isMutable (s->type))
 	    {
-	      sRef_setExKind (s, sRef_getExKind (sp), fileloc_undefined);
-
-	      	      
+	      s->expkind = sRef_getExKind (sp);
+	      s->expinfo = stateInfo_copy (sp->expinfo);
+	      
 	      s->aliaskind = sp->aliaskind;
+	      s->aliasinfo = stateInfo_copy (sp->aliasinfo);
 	    }
 
 	  s->defstate = sp->defstate;
@@ -5852,7 +6457,8 @@ void sRef_setArrayFetchState (/*@notnull@*/ /*@exposed@*/ sRef s,
 		}
 	    }
 
-	  s->nullstate = sp->nullstate;
+	  DPRINTF (("Set null state: %s / %s", sRef_unparseFull (s), sRef_unparseFull (sp)));
+	  sRef_setNullStateN (s, sRef_getNullState (sp));
 	}
       else
 	{
@@ -5882,8 +6488,9 @@ void sRef_setArrayFetchState (/*@notnull@*/ /*@exposed@*/ sRef s,
 	      */
 	    }
 
-	  sRef_setExKind (s, sRef_getExKind (arr), g_currentloc);
-
+	  s->expkind = sRef_getExKind (arr);
+	  s->expinfo = stateInfo_copy (arr->expinfo);
+	  
 	  if (arr->aliaskind == AK_LOCAL || arr->aliaskind == AK_FRESH)
 	    {
 	      s->aliaskind = AK_LOCAL;
@@ -5934,32 +6541,38 @@ void sRef_setArrayFetchState (/*@notnull@*/ /*@exposed@*/ sRef s,
 		  
 		  sRefSet_allElements (arr->deriv, sr)
 		    {
-		      if (sRef_isValid (sr))
+		      if (sRef_isReasonable (sr))
 			{
-			  if (sr->defstate == SS_ALLOCATED)
-			    {
-			      s->defstate = SS_ALLOCATED;
-			    }
-			  else 
+			  if (sRef_isReasonable (sr))
 			    {
-			      if (sr->defstate == SS_DEFINED)
+			      if (sr->defstate == SS_ALLOCATED)
 				{
-				  if (context_getFlag (FLG_STRICTDESTROY))
-				    {
-				      s->defstate = SS_DEFINED;
-				    }
-				  else
+				  s->defstate = SS_ALLOCATED;
+				}
+			      else 
+				{
+				  if (sr->defstate == SS_DEFINED)
 				    {
-				      s->defstate = SS_PARTIAL;
+				      if (context_getFlag (FLG_STRICTDESTROY))
+					{
+					  s->defstate = SS_DEFINED;
+					}
+				      else
+					{
+					  s->defstate = SS_PARTIAL;
+					}
+				      
+				      break;
 				    }
-
-				  break;
 				}
 			    }
+			  else
+			    {
+			      llcontbug (message ("Invalid sRef as derived element of %s", sRef_unparse (arr)));
+			    }
 			}
 		    } end_sRefSet_allElements;
-		  
-		  		}
+		}
 	      else
 		{
 		  s->defstate = SS_UNDEFINED;
@@ -5994,6 +6607,7 @@ void sRef_setArrayFetchState (/*@notnull@*/ /*@exposed@*/ sRef s,
   if (sRef_isObserver (arr)) 
     {
       s->expkind = XO_OBSERVER;
+      s->expinfo = stateInfo_copy (arr->expinfo);
     }
 }  
 
@@ -6001,7 +6615,7 @@ void sRef_setArrayFetchState (/*@notnull@*/ /*@exposed@*/ sRef s,
 {
   sRef s;
 
-  if (!sRef_isValid (arr)) {
+  if (!sRef_isReasonable (arr)) {
     /*@-nullret@*/ return arr /*@=nullret@*/;
   }
 
@@ -6012,14 +6626,27 @@ void sRef_setArrayFetchState (/*@notnull@*/ /*@exposed@*/ sRef s,
   
   s = sRef_findDerivedArrayFetch (arr, FALSE, 0, FALSE);
   
-  if (sRef_isValid (s))
+  if (sRef_isReasonable (s))
     {
-      sRef_setExKind (s, sRef_getExKind (arr), g_currentloc);
+      /* evans 2001-07-12: this is bogus, clean-up hack */
+      if (s->info->arrayfetch->arr != arr)
+	{
+	  sRef res;
+	  check (sRefSet_delete (arr->deriv, s));
+	  res = sRef_buildArrayFetch (arr);
+	  sRef_copyState (res, s);
+	  llassert (res->info->arrayfetch->arr == arr); 
+	  return res;
+	}
+
+      s->expkind = sRef_getExKind (arr);
+      s->expinfo = stateInfo_copy (arr->expinfo);
+
       return s;
     }
   else
     {
-      s = sRef_new ();
+      s = sRef_newRef ();
 
       s->kind = SK_ARRAYFETCH;
       s->info = (sinfo) dmalloc (sizeof (*s->info));
@@ -6027,7 +6654,9 @@ void sRef_setArrayFetchState (/*@notnull@*/ /*@exposed@*/ sRef s,
       s->info->arrayfetch->indknown = FALSE;
       s->info->arrayfetch->ind = 0;
       s->info->arrayfetch->arr = arr;
+
       sRef_setArrayFetchState (s, arr);
+
       s->oaliaskind = s->aliaskind;
       s->oexpkind = s->expkind;
 
@@ -6036,6 +6665,12 @@ void sRef_setArrayFetchState (/*@notnull@*/ /*@exposed@*/ sRef s,
 	  sRef_addDeriv (arr, s);
 	}
       
+      if (valueTable_isUndefined (s->state))
+	{
+	  s->state = context_createValueTable 
+	    (s, stateInfo_makeLoc (g_currentloc, SA_CREATED));
+	}
+      
       return (s);
     }
 }
@@ -6045,25 +6680,42 @@ void sRef_setArrayFetchState (/*@notnull@*/ /*@exposed@*/ sRef s,
 {
   sRef s;
 
-  if (!sRef_isValid (arr)) {
+  if (!sRef_isReasonable (arr)) {
     /*@-nullret@*/ return arr /*@=nullret@*/;
   }
 
   if (ctype_isRealPointer (arr->type))
     {
-       (void) sRef_buildPointer (arr); /* do this to define arr! */
+      (void) sRef_buildPointer (arr); /* do this to define arr! */
     }
 
   s = sRef_findDerivedArrayFetch (arr, TRUE, i, FALSE);
-      
-  if (sRef_isValid (s))
+
+  if (sRef_isReasonable (s))
     {
-      sRef_setExKind (s, sRef_getExKind (arr), g_currentloc);      
+      /* evans 2001-07-12: this is bogus, clean-up hack */
+      if (s->info->arrayfetch->arr != arr)
+	{
+	  sRef res;
+
+	  check (sRefSet_delete (arr->deriv, s));
+	  res = sRef_buildArrayFetchKnown (arr, i);
+
+	  llassert (res->info->arrayfetch->arr == arr);
+	  sRef_copyState (res, s);
+	  llassert (res->info->arrayfetch->arr == arr);
+	  return res;
+	}
+
+      s->expkind = sRef_getExKind (arr);
+      s->expinfo = stateInfo_copy (arr->expinfo);
+
+      llassert (s->info->arrayfetch->arr == arr);
       return s;
     }
   else
     {
-      s = sRef_new ();
+      s = sRef_newRef ();
       
       s->kind = SK_ARRAYFETCH;
       s->info = (sinfo) dmalloc (sizeof (*s->info));
@@ -6071,13 +6723,16 @@ void sRef_setArrayFetchState (/*@notnull@*/ /*@exposed@*/ sRef s,
       s->info->arrayfetch->arr = arr;
       s->info->arrayfetch->indknown = TRUE;
       s->info->arrayfetch->ind = i;
-      
+
       sRef_setArrayFetchState (s, arr);
-      
+      /* evans 2001-08-27 no: can change this - llassert (s->info->arrayfetch->arr == arr); */
+
       s->oaliaskind = s->aliaskind;
       s->oexpkind = s->expkind;
       sRef_addDeriv (arr, s);
 
+      llassert (valueTable_isUndefined (s->state));
+      s->state = context_createValueTable (s, stateInfo_makeLoc (g_currentloc, SA_CREATED));
       return (s);
     }
 }
@@ -6088,9 +6743,10 @@ void sRef_setArrayFetchState (/*@notnull@*/ /*@exposed@*/ sRef s,
 
 static void
 sRef_setPartsFromUentry (sRef s, uentry ue)
-{
-    
-  llassert (sRef_isValid (s));
+{    
+  sRef uref = uentry_getSref (ue);
+
+  llassert (sRef_isReasonable (s));
 
   s->aliaskind = alkind_derive (s->aliaskind, uentry_getAliasKind (ue));
   s->oaliaskind = s->aliaskind;
@@ -6099,27 +6755,38 @@ sRef_setPartsFromUentry (sRef s, uentry ue)
     {
       s->expkind = uentry_getExpKind (ue);
     }
-
+  
   s->oexpkind = s->expkind;
-
-  if (s->nullstate == NS_UNKNOWN)
+  
+  if (sRef_getNullState (s) == NS_UNKNOWN)
+    {
+      DPRINTF (("Set null state: %s / %s", sRef_unparseFull (s), uentry_unparseFull (ue)));
+      sRef_setNullStateN (s, sRef_getNullState (uentry_getSref (ue)));
+    }
+  else
     {
-      s->nullstate = sRef_getNullState (uentry_getSref (ue));
+      DPRINTF (("Skipping null null state!"));
     }
 
-  if (s->aliaskind == AK_IMPONLY 
-      && (sRef_isExposed (s) || sRef_isObserver (s)))
+  if (s->aliaskind == AK_IMPONLY && (sRef_isExposed (s) || sRef_isObserver (s)))
     {
       s->oaliaskind = s->aliaskind = AK_IMPDEPENDENT;
-    }
+    } 
 
+  if (sRef_isReasonable (uref))
+    {
+      valueTable utable = uref->state;
+      valueTable_free (s->state);
+      s->state = valueTable_copy (utable);
+    }
 }
 
 static void
 sRef_setStateFromAbstractUentry (sRef s, uentry ue)
 {
-  llassert (sRef_isValid (s));
-  
+  llassert (sRef_isReasonable (s));
+  sRef_checkMutable (s);
+
   sRef_setPartsFromUentry (s, ue);
 
   s->aliaskind = alkind_derive (s->aliaskind, uentry_getAliasKind (ue));
@@ -6138,7 +6805,8 @@ sRef_setStateFromUentry (sRef s, uentry ue)
 {
   sstate defstate;
 
-  llassert (sRef_isValid (s));
+  sRef_checkMutable (s);
+  llassert (sRef_isReasonable (s));
   
   sRef_setPartsFromUentry (s, ue);
 
@@ -6172,10 +6840,11 @@ sRef_setStateFromUentry (sRef s, uentry ue)
 
       DPRINTF (("find derived: %s", sRef_unparse (s)));
 
-      if (sRef_isValid (s))
+      if (sRef_isReasonable (s))
 	{
-	  
-	  sRef_setExKind (s, sRef_getExKind (t), g_currentloc);
+	  s->expkind = sRef_getExKind (t);
+	  s->expinfo = stateInfo_copy (t->expinfo);	  
+
 	  s->oaliaskind = s->aliaskind;
 	  s->oexpkind = s->expkind;
 
@@ -6187,7 +6856,7 @@ sRef_setStateFromUentry (sRef s, uentry ue)
 	  
 	  DPRINTF (("construct: %s", sRef_unparse (s)));
 
-	  if (sRef_isValid (s))
+	  if (sRef_isReasonable (s))
 	    {
 	      sRef_addDeriv (t, s);
 
@@ -6201,7 +6870,7 @@ sRef_setStateFromUentry (sRef s, uentry ue)
 }
 
 /*@exposed@*/ sRef
-sRef_constructPointer (sRef t)
+sRef_constructPointer (/*@exposed@*/ sRef t)
    /*@modifies t@*/
 {
   return sRef_buildPointer (t);
@@ -6209,7 +6878,7 @@ sRef_constructPointer (sRef t)
 
 static /*@exposed@*/ sRef sRef_constructDerefAux (sRef t, bool isdead)
 {
-  if (sRef_isValid (t))
+  if (sRef_isReasonable (t))
     {
       sRef s;
       
@@ -6217,32 +6886,20 @@ static /*@exposed@*/ sRef sRef_constructDerefAux (sRef t, bool isdead)
       ** if there is a derived t[?], return that.  Otherwise, *t.
       */
       
-            
       s = sRef_findDerivedArrayFetch (t, FALSE, 0, isdead);
       
-      if (sRef_isValid (s))
+      if (sRef_isReasonable (s))
 	{
-	  	  return s;
+	  DPRINTF (("Found array fetch: %s", sRef_unparseFull (s)));
+	  return s;
 	}
       else
 	{
 	  sRef ret = sRef_constructPointer (t);
 
-	  /*
-	  ** This is necessary to prevent infinite depth
-	  ** in checking complete destruction.  
-	  */
+	  DPRINTF (("Constructed pointer: %s", sRef_unparseFull (ret)));
 
-	  
-	  if (isdead)
-	    {
-	      /* ret->defstate = SS_UNKNOWN;  */
-	      return ret; 
-	    }
-	  else
-	    {
-	      return ret;
-	    }
+	  return ret;
 	}
     }
   else
@@ -6264,33 +6921,37 @@ sRef sRef_constructDeadDeref (sRef t)
 static sRef
 sRef_constructPointerAux (/*@notnull@*/ /*@exposed@*/ sRef t)
 {
-  sRef s = sRef_new ();
+  sRef s = sRef_newRef ();
   ctype rt = t->type;
   ctype st;
   
+  llassert (valueTable_isUndefined (s->state));
+
   s->kind = SK_PTR;
   s->info = (sinfo) dmalloc (sizeof (*s->info));
-  s->info->ref = t;
+  s->info->ref = t; 
   
   if (ctype_isRealAP (rt))
     {
       s->type = ctype_baseArrayPtr (rt);
     }
   
-  st = ctype_realType (s->type);
-  
-    
+  st = ctype_realType (s->type);  
+
   if (t->defstate == SS_UNDEFINED)
     {
       s->defstate = SS_UNUSEABLE;
+      s->definfo = stateInfo_copy (t->definfo);
     }
   else if ((t->defstate == SS_ALLOCATED) && !ctype_isSU (st))
     {
       s->defstate = SS_UNDEFINED;
+      s->definfo = stateInfo_copy (t->definfo);
     }
   else
     {
       s->defstate = t->defstate;
+      s->definfo = stateInfo_copy (t->definfo);
     }
   
   if (t->aliaskind == AK_LOCAL || t->aliaskind == AK_FRESH)
@@ -6301,55 +6962,64 @@ sRef_constructPointerAux (/*@notnull@*/ /*@exposed@*/ sRef t)
     {
       s->aliaskind = AK_UNKNOWN;
     }
-  
-  sRef_setExKind (s, sRef_getExKind (t), fileloc_undefined);
+
+  s->expkind = sRef_getExKind (t);
+  s->expinfo = stateInfo_copy (t->expinfo);
+
   sRef_setTypeState (s);
-  
+
   s->oaliaskind = s->aliaskind;
   s->oexpkind = s->expkind;
 
+  if (valueTable_isUndefined (s->state))
+    {
+      s->state = context_createValueTable (s, stateInfo_makeLoc (g_currentloc, SA_CREATED));
+    }
+
+  DPRINTF (("pointer: %s", sRef_unparseFull (s)));
   return s;
 }
 
 bool sRef_hasDerived (sRef s)
 {
-  return (sRef_isValid (s) && !sRefSet_isEmpty (s->deriv));
+  return (sRef_isReasonable (s) && !sRefSet_isEmpty (s->deriv));
 }
 
 void
 sRef_clearDerived (sRef s)
 {
-  if (sRef_isValid (s))
+  if (sRef_isReasonable (s))
     {
-            sRefSet_clear (s->deriv); 
+      DPRINTF (("Clear derived: [%p] %s", s, sRef_unparseDebug (s)));
+      sRefSet_clear (s->deriv); 
     }
 }
 
 void
 sRef_clearDerivedComplete (sRef s)
 {
-  
-  if (sRef_isValid (s))
+  if (sRef_isReasonable (s))
     {
       sRef base = sRef_getBaseSafe (s);
-
-      while (sRef_isValid (base))
+      
+      while (sRef_isReasonable (base))
 	{
+	  DPRINTF (("Clear derived: [%p] %s", base, sRef_unparse (base)));
 	  sRefSet_clear (base->deriv); 
 	  base = sRef_getBaseSafe (base);
 	}
 
+      DPRINTF (("Clear derived: [%p] %s", s, sRef_unparse (s)));
       sRefSet_clear (s->deriv); 
     }
 }
 
-/*@exposed@*/ sRef
-sRef_makePointer (sRef s)
-   /*@modifies s@*/
+/*@exposed@*/ sRef sRef_makePointer (/*@exposed@*/ sRef s)
+     /*@modifies s@*/
 {
   sRef res = sRef_buildPointer (s); 
 
-  DPRINTF (("Res: %s", sRef_unparse (res)));
+  DPRINTF (("Res: %s", sRef_unparseFull (res)));
   return res;
 }
 
@@ -6359,11 +7029,10 @@ sRef_makePointer (sRef s)
 
 /*@exposed@*/ sRef
 sRef_makeAnyArrayFetch (/*@exposed@*/ sRef arr)
-{
-  
+{  
   if (sRef_isAddress (arr))
     {
-            return (arr->info->ref);
+      return (arr->info->ref);
     }
   else
     {
@@ -6372,13 +7041,13 @@ sRef_makeAnyArrayFetch (/*@exposed@*/ sRef arr)
 }
 
 /*@exposed@*/ sRef
-sRef_makeArrayFetch (sRef arr)
+sRef_makeArrayFetch (/*@exposed@*/ sRef arr)
 {
   return (sRef_buildArrayFetch (arr));
 }
 
 /*@exposed@*/ sRef
-sRef_makeArrayFetchKnown (sRef arr, int i)
+sRef_makeArrayFetchKnown (/*@exposed@*/ sRef arr, int i)
 {
   return (sRef_buildArrayFetchKnown (arr, i));
 }
@@ -6392,9 +7061,9 @@ sRef_makeField (sRef rec, /*@dependent@*/ cstring f)
 }
 
 /*@exposed@*/ sRef
-sRef_makeNCField (sRef rec, /*@dependent@*/ cstring f)
+sRef_makeNCField (/*@exposed@*/ sRef rec, /*@dependent@*/ cstring f)
 {
-    return (sRef_buildNCField (rec, f));
+  return (sRef_buildNCField (rec, f));
 }
 
 /*@only@*/ cstring
@@ -6564,13 +7233,10 @@ sRef_unparseKindNamePlain (sRef s)
 void
 sRef_copyState (sRef s1, sRef s2)
 {
-  if (sRef_isValid (s1) && sRef_isValid (s2))
+  if (sRef_isReasonable (s1) && sRef_isReasonable (s2))
     {
       s1->defstate = s2->defstate;
       
-      s1->nullstate = s2->nullstate;
-      s1->nullinfo = alinfo_update (s1->nullinfo, s2->nullinfo);
-      
       /* start modifications */
       s1->bufinfo.bufstate = s2->bufinfo.bufstate;
       s1->bufinfo.len = s2->bufinfo.len;
@@ -6578,55 +7244,67 @@ sRef_copyState (sRef s1, sRef s2)
       /* end modifications */
 
       s1->aliaskind = s2->aliaskind;
-      s1->aliasinfo = alinfo_update (s1->aliasinfo, s2->aliasinfo);
+      s1->aliasinfo = stateInfo_update (s1->aliasinfo, s2->aliasinfo);
 
       s1->expkind = s2->expkind;
-      s1->expinfo = alinfo_update (s1->expinfo, s2->expinfo);
+      s1->expinfo = stateInfo_update (s1->expinfo, s2->expinfo);
+
+      s1->nullstate = s2->nullstate;
+      s1->nullinfo = stateInfo_update (s1->nullinfo, s2->nullinfo);
 
+      valueTable_free (s1->state);  
+      s1->state = valueTable_copy (s2->state);
       s1->safe = s2->safe;
-          }
+    }
 }
 
 sRef
 sRef_makeNew (ctype ct, sRef t, cstring name)
 {
-  sRef s = sRef_new ();
+  sRef s = sRef_newRef ();
 
   s->kind = SK_NEW;
   s->type = ct;
 
-  llassert (sRef_isValid (t));
+  llassert (sRef_isReasonable (t));
   s->defstate = t->defstate;
 
   s->aliaskind = t->aliaskind;
   s->oaliaskind = s->aliaskind;
-
   s->nullstate = t->nullstate;
-
+  
   s->expkind = t->expkind;
   s->oexpkind = s->expkind;
-
+  
   s->info = (sinfo) dmalloc (sizeof (*s->info));
   s->info->fname = name;
 
   /* start modifications */
   s->bufinfo.bufstate = t->bufinfo.bufstate;
   /* end modifications */
+  
+  llassert (valueTable_isUndefined (s->state));
+  s->state = valueTable_copy (t->state);
 
-    return s;
+  DPRINTF (("==> Copying state: %s", valueTable_unparse (s->state)));
+  DPRINTF (("==> new: %s", sRef_unparseFull (s)));
+  return s;
 }
 
 sRef
 sRef_makeType (ctype ct)
 {
-  sRef s = sRef_new ();
-  
+  sRef s = sRef_newRef ();
+
+  sRef_checkMutable (s);
+
   s->kind = SK_TYPE;
   s->type = ct;
 
   s->defstate = SS_UNKNOWN; 
   s->aliaskind = AK_UNKNOWN;
-  s->nullstate = NS_UNKNOWN;
+  sRef_setNullStateN (s, NS_UNKNOWN);
+
   /* start modification */
   s->bufinfo.bufstate = BB_NOTNULLTERMINATED;
   /* end modification */
@@ -6642,30 +7320,34 @@ sRef_makeType (ctype ct)
 	  sRef_mergeStateQuiet (s, uentry_getSref (ue));
 	}
     }
-
-    s->oaliaskind = s->aliaskind;
+  
+  s->oaliaskind = s->aliaskind;
   s->oexpkind = s->expkind;
+  llassert (valueTable_isUndefined (s->state));
+  s->state = context_createValueTable (s, stateInfo_makeLoc (g_currentloc, SA_CREATED));
 
+  DPRINTF (("Create: %s", sRef_unparseFull (s)));
   return s;
 }
 
 sRef
 sRef_makeConst (ctype ct)
 {
-  sRef s = sRef_new ();
+  sRef s = sRef_newRef ();
   
   s->kind = SK_CONST;
   s->type = ct;
 
   s->defstate = SS_UNKNOWN;
   s->aliaskind = AK_UNKNOWN;
-  s->nullstate = NS_UNKNOWN;
+  sRef_setNullStateN (s, NS_UNKNOWN);
+
   /* start modification */
   s->bufinfo.bufstate = BB_NULLTERMINATED;
   /* end modification */
 
-  
-  if (ctype_isUA (ct))
+  /* evans 2002-04-22: added isManifestBool to avoid errors for -boolfalse initializations */
+  if (!ctype_isManifestBool (ct) && ctype_isUA (ct)) 
     {
       typeId uid = ctype_typeId (ct);
       uentry te = usymtab_getTypeEntrySafe (uid);
@@ -6675,11 +7357,13 @@ sRef_makeConst (ctype ct)
 	  sRef_mergeStateQuiet (s, uentry_getSref (te));
 	}
     }
-
   
   s->oaliaskind = s->aliaskind;
   s->oexpkind = s->expkind;
 
+  llassert (valueTable_isUndefined (s->state));
+  s->state = context_createValueTable (s, stateInfo_makeLoc (g_currentloc, SA_CREATED));
+
   return s;
 }
 
@@ -6700,10 +7384,18 @@ bool sRef_hasName (sRef s)
       }
     case SK_PARAM:
       {
-	uentry u = uentryList_getN (context_getParams (), 
-				    s->info->paramno);
-
-	return (uentry_hasName (u));
+	if (s->info->paramno >= 0)
+	  {
+	    uentry u = uentryList_getN (context_getParams (), 
+					s->info->paramno);
+	    
+	    return (uentry_hasName (u));
+	  }
+	else
+	  {
+	    llassert (s->info->paramno == PARAMUNKNOWN);
+	    return FALSE;
+	  }
       }
     default:
       return TRUE;
@@ -6735,13 +7427,20 @@ sRef_sameName (sRef s1, sRef s2)
 	{
 	  if (context_inFunctionLike ())
 	    {
-	      uentry u1 = usymtab_getRefQuiet (s1->info->cvar->lexlevel,
-					       s1->info->cvar->index);
-	      uentry u2 = uentryList_getN (context_getParams (), 
-					   s2->info->paramno);
-	  
-	      return (cstring_equalFree (uentry_getName (u1),
-					 uentry_getName (u2)));
+	      if (s2->info->paramno != PARAMUNKNOWN)
+		{
+		  uentry u1 = usymtab_getRefQuiet (s1->info->cvar->lexlevel,
+						   s1->info->cvar->index);
+		  uentry u2 = uentryList_getN (context_getParams (), 
+					       s2->info->paramno);
+		  
+		  return (cstring_equalFree (uentry_getName (u1),
+					     uentry_getName (u2)));
+		}
+	      else
+		{
+		  return s1->info->paramno == PARAMUNKNOWN;
+		}
 	    }
 	  else 
 	    {
@@ -6762,14 +7461,21 @@ sRef_sameName (sRef s1, sRef s2)
 	  {
 	    if (context_inFunctionLike ())
 	      {
-		uentry u1 = uentryList_getN (context_getParams (), 
-					     s1->info->paramno);
-		uentry u2 = usymtab_getRefQuiet (s2->info->cvar->lexlevel,
-						 s2->info->cvar->index);
-
-		
-		return (cstring_equalFree (uentry_getName (u1),
-					   uentry_getName (u2)));
+		if (s1->info->paramno == PARAMUNKNOWN)
+		  {
+		    return FALSE;
+		  }
+		else
+		  {
+		    uentry u1 = uentryList_getN (context_getParams (), 
+						 s1->info->paramno);
+		    uentry u2 = usymtab_getRefQuiet (s2->info->cvar->lexlevel,
+						     s2->info->cvar->index);
+		    
+		    
+		    return (cstring_equalFree (uentry_getName (u1),
+					       uentry_getName (u2)));
+		  }
 	      }
 	    else 
 	      {
@@ -6886,6 +7592,7 @@ sRef_storeState (sRef s)
 {
   if (sRef_isInvalid (s)) return;
 
+  sRef_checkMutable (s);
   s->oaliaskind = s->aliaskind;
   s->oexpkind = s->expkind;
 }
@@ -6929,7 +7636,7 @@ sRef_resetState (sRef s)
 	{
 	  changed = TRUE;
 	  s->aliaskind = s->oaliaskind;
-	  	}
+	}
     }
 
   if (changed)
@@ -7009,9 +7716,9 @@ sRef_fixDirectBase (sRef s, sRef base)
   
   if (sRef_isInvalid (s))
     {
-            return sRef_undefined;
+      return sRef_undefined;
     }
-
+  
   switch (s->kind)
     {
     case SK_ARRAYFETCH:
@@ -7063,17 +7770,21 @@ sRef_showRefLost (sRef s)
   if (sRef_hasAliasInfoLoc (s))
     {
       llgenindentmsg (cstring_makeLiteral ("Original reference lost"),
-		sRef_getAliasInfoLoc (s));
+		      sRef_getAliasInfoLoc (s));
     }
 }
 
 void
 sRef_showRefKilled (sRef s)
 {
-  if (sRef_hasStateInfoLoc (s))
+  if (sRef_isValid (s)) 
     {
-      llgenindentmsg (message ("Storage %q released", 
-			       sRef_unparse (s)), sRef_getStateInfoLoc (s));
+      DPRINTF (("Killed: %s", sRef_unparseFull (s)));
+      if (context_getLocIndentSpaces () == 0) {
+	stateInfo_display (s->definfo, message ("  Storage %q", sRef_unparseOpt (s)));
+      } else {
+	stateInfo_display (s->definfo, message ("Storage %q", sRef_unparseOpt (s)));
+      }
     }
 }
 
@@ -7089,60 +7800,62 @@ sRef_showStateInconsistent (sRef s)
     }
 }
 
-void
-sRef_showStateInfo (sRef s)
-{
-  if (sRef_hasStateInfoLoc (s))
-    {
-      if (s->defstate == SS_DEAD)
-	{
-	  llgenindentmsg 
-	    (message ("Storage %qis released", sRef_unparseOpt (s)),
-	     sRef_getStateInfoLoc (s));
-	}
-      else if (s->defstate == SS_ALLOCATED || s->defstate == SS_DEFINED)
-	{
-	  llgenindentmsg 
-	    (message ("Storage %qis %s", sRef_unparseOpt (s), 
-		      sstate_unparse (s->defstate)),
-	     sRef_getStateInfoLoc (s));
-	}
-      else if (s->defstate == SS_UNUSEABLE)
-	{
-	  llgenindentmsg 
-	    (message ("Storage %qbecomes inconsistent (clauses merge with"
-		      "%qreleased on one branch)",
-		      sRef_unparseOpt (s), 
-		      sRef_unparseOpt (s)),
-	     sRef_getStateInfoLoc (s));
-	}
-      else 
-	{
-	  llgenindentmsg (message ("Storage %qbecomes %s", 
-				   sRef_unparseOpt (s), 
-				   sstate_unparse (s->defstate)),
-			  sRef_getStateInfoLoc (s));
-	}
+void
+sRef_showStateInfo (sRef s)
+{
+  if (sRef_isValid (s)) {
+    if (context_getLocIndentSpaces () == 0) {
+      stateInfo_display (s->definfo, message ("   Storage %q", sRef_unparseOpt (s)));
+    } else {
+      stateInfo_display (s->definfo, message ("Storage %q", sRef_unparseOpt (s)));
     }
+  }
 }
 
 void
 sRef_showExpInfo (sRef s)
 {
-  if (sRef_hasExpInfoLoc (s))
+  if (sRef_isValid (s)) {
+    if (context_getLocIndentSpaces () == 0) {
+      stateInfo_display (s->expinfo, message ("   Storage %q", sRef_unparseOpt (s)));
+    } else {
+      stateInfo_display (s->expinfo, message ("Storage %q", sRef_unparseOpt (s)));
+    }
+  }
+}
+
+void
+sRef_showMetaStateInfo (sRef s, cstring key)
+{
+  stateValue val;
+  metaStateInfo minfo = context_lookupMetaStateInfo (key);
+
+  llassert (sRef_isReasonable (s));
+  llassert (valueTable_isDefined (s->state));
+  llassert (metaStateInfo_isDefined (minfo));
+
+  val = valueTable_lookup (s->state, key);
+  
+  if (stateValue_hasLoc (val))
     {
-      llgenindentmsg (message ("Storage %qbecomes %s", sRef_unparseOpt (s), 
-			       exkind_unparse (s->expkind)),
-		      sRef_getExpInfoLoc (s));
+      llgenindentmsg 
+	(message ("%qbecomes %q", sRef_unparseOpt (s), 
+		  stateValue_unparseValue (val, minfo)),
+	 stateValue_getLoc (val));
     }
 }
 
 void
 sRef_showNullInfo (sRef s)
 {
+  DPRINTF (("Show null info: %s", sRef_unparseFull (s)));
+
   if (sRef_hasNullInfoLoc (s) && sRef_isKnown (s))
     {
-      switch (s->nullstate)
+      DPRINTF (("has null info: %s",
+		fileloc_unparse (sRef_getNullInfoLoc (s))));
+
+      switch (sRef_getNullState (s))
 	{
 	case NS_CONSTNULL:
 	  {
@@ -7194,7 +7907,7 @@ sRef_showNullInfo (sRef s)
 	  llgenindentmsg
 	    (message ("<error case> Storage %q becomes %s",
 		      sRef_unparse (s), 
-		      nstate_unparse (s->nullstate)),
+		      nstate_unparse (sRef_getNullState (s))),
 	     sRef_getNullInfoLoc (s));
 	  
 	  break;
@@ -7205,24 +7918,23 @@ sRef_showNullInfo (sRef s)
 void
 sRef_showAliasInfo (sRef s)
 {
-  if (sRef_hasAliasInfoLoc (s))
+  if (sRef_isValid (s)) 
     {
       if (sRef_isFresh (s))
 	{
-	  llgenindentmsg 
-	    (message ("Fresh storage %qallocated", sRef_unparseOpt (s)),
-	     sRef_getAliasInfoLoc (s));
+	  if (context_getLocIndentSpaces () == 0) {
+	    stateInfo_display (s->aliasinfo, message ("   Fresh storage %q", sRef_unparseOpt (s)));
+	  } else {
+	    stateInfo_display (s->aliasinfo, message ("Fresh storage %q", sRef_unparseOpt (s)));
+	  }
 	}
-      else 
+      else
 	{
-	  if (!sRef_isRefCounted (s))
-	    {
-	      llgenindentmsg 
-		(message ("Storage %qbecomes %s", 
-			  sRef_unparseOpt (s),
-			  alkind_unparse (sRef_getAliasKind (s))),
-		 sRef_getAliasInfoLoc (s));
-	    }
+	  if (context_getLocIndentSpaces () == 0) {
+	    stateInfo_display (s->aliasinfo, message ("   Storage %q", sRef_unparseOpt (s))); 
+	  } else {
+	    stateInfo_display (s->aliasinfo, message ("Storage %q", sRef_unparseOpt (s)));
+	  }
 	}
     }
 }
@@ -7230,17 +7942,15 @@ sRef_showAliasInfo (sRef s)
 void
 sRef_mergeNullState (sRef s, nstate n)
 {
-  if (sRef_isValid (s))
+  if (sRef_isReasonable (s))
     {
       nstate old;
       
-      old = s->nullstate;
+      old = sRef_getNullState (s);
       
       if (n != old && n != NS_UNKNOWN)
-	{
-	  	  
-	  s->nullstate = n;
-	  s->nullinfo = alinfo_updateLoc (s->nullinfo, g_currentloc);
+	{	  	  
+	  sRef_setNullState (s, n, g_currentloc);
 	}
     }
   else
@@ -7252,12 +7962,12 @@ sRef_mergeNullState (sRef s, nstate n)
 bool
 sRef_possiblyNull (sRef s)
 {
-  if (sRef_isValid (s))
+  if (sRef_isReasonable (s))
     {
-      if (s->nullstate == NS_ABSNULL)
+      if (sRef_getNullState (s) == NS_ABSNULL)
 	{
 	  ctype rct = ctype_realType (s->type);
-
+	  
 	  if (ctype_isAbstract (rct))
 	    {
 	      return FALSE;
@@ -7279,10 +7989,10 @@ sRef_possiblyNull (sRef s)
 	}
       else
 	{
-	  return nstate_possiblyNull (s->nullstate);
+	  return nstate_possiblyNull (sRef_getNullState (s));
 	}
     }
-
+  
   return FALSE;
 }
 
@@ -7327,7 +8037,7 @@ sRef_unparseScope (sRef s)
 int
 sRef_getScope (sRef s)
 {
-  llassert (sRef_isValid (s));
+  llassert (sRef_isReasonable (s));
 
   if (sRef_isCvar (s))
     {
@@ -7346,13 +8056,13 @@ sRef_getScope (sRef s)
 bool
 sRef_isDead (sRef s)
 {
-  return (sRef_isValid (s) && (s)->defstate == SS_DEAD);
+  return (sRef_isReasonable (s) && (s)->defstate == SS_DEAD);
 }
 
 bool
 sRef_isDeadStorage (sRef s)
 {
-  if (sRef_isValid (s))
+  if (sRef_isReasonable (s))
     {
       if (s->defstate == SS_DEAD
 	  || s->defstate == SS_UNUSEABLE
@@ -7375,12 +8085,12 @@ sRef_isDeadStorage (sRef s)
 bool
 sRef_isPossiblyDead (sRef s)
 {
-  return (sRef_isValid (s) && s->defstate == SS_HOFFA);
+  return (sRef_isReasonable (s) && s->defstate == SS_HOFFA);
 }
 
 bool sRef_isStateLive (sRef s)
 {
-  if (sRef_isValid (s))
+  if (sRef_isReasonable (s))
     {
       sstate ds = s->defstate;
 
@@ -7398,7 +8108,7 @@ bool sRef_isStateLive (sRef s)
 
 bool sRef_isStateUndefined (sRef s)
 {
-  return ((sRef_isValid(s)) && ((s)->defstate == SS_UNDEFINED));
+  return ((sRef_isReasonable(s)) && ((s)->defstate == SS_UNDEFINED));
 }
 
 bool sRef_isJustAllocated (sRef s)
@@ -7422,7 +8132,7 @@ bool sRef_isJustAllocated (sRef s)
 static bool
 sRef_isAllocatedStorage (sRef s)
 {
-  if (sRef_isValid (s) && ynm_toBoolStrict (sRef_isReadable (s)))
+  if (sRef_isReasonable (s) && ynm_toBoolStrict (sRef_isValidLvalue (s)))
     {
       return (ctype_isVisiblySharable (sRef_getType (s)));
     }
@@ -7441,9 +8151,9 @@ sRef_isUnuseable (sRef s)
 bool
 sRef_perhapsNull (sRef s)
 {
-  if (sRef_isValid (s))
+  if (sRef_isReasonable (s))
     {
-      if (s->nullstate == NS_ABSNULL)
+      if (sRef_getNullState (s) == NS_ABSNULL)
 	{
 	  ctype rct = ctype_realType (s->type);
 
@@ -7468,7 +8178,7 @@ sRef_perhapsNull (sRef s)
 	}
       else
 	{
-	  return nstate_perhapsNull (s->nullstate);
+	  return nstate_perhapsNull (sRef_getNullState (s));
 	}
     }
 
@@ -7482,8 +8192,8 @@ sRef_perhapsNull (sRef s)
 bool 
 sRef_definitelyNull (sRef s)
 {
-  return (sRef_isValid (s)
-	  && (s->nullstate == NS_DEFNULL || s->nullstate == NS_CONSTNULL));
+  return (sRef_isReasonable (s)
+	  && (sRef_getNullState (s) == NS_DEFNULL || sRef_getNullState (s) == NS_CONSTNULL));
 }
 
 /*
@@ -7493,13 +8203,13 @@ sRef_definitelyNull (sRef s)
 void
 sRef_setDerivNullState (sRef set, sRef guide, nstate ns)
 {
-  if (sRef_isValid (set))
+  if (sRef_isReasonable (set))
     {
       sRef deriv = sRef_getDeriv (set, guide);
       
-      if (sRef_isValid (deriv))
+      if (sRef_isReasonable (deriv))
 	{
-	  deriv->nullstate = ns;
+	  sRef_setNullStateN (deriv, ns);
 	}
     }
 }
@@ -7507,20 +8217,18 @@ sRef_setDerivNullState (sRef set, sRef guide, nstate ns)
 static /*@exposed@*/ sRef
 sRef_getDeriv (/*@returned@*/ /*@notnull@*/ sRef set, sRef guide)
 {
-  llassert (sRef_isValid (set));
-  llassert (sRef_isValid (guide));
+  llassert (sRef_isReasonable (set));
+  llassert (sRef_isReasonable (guide));
 
   switch (guide->kind)
     {
     case SK_CVAR:
-      llassert (set->kind == SK_CVAR);
-      
+      llassert (set->kind == SK_CVAR);      
       return set;
 
     case SK_PARAM:
       llassert (set->kind == guide->kind);
       llassert (set->info->paramno == guide->info->paramno);
-
       return set;
 
     case SK_ARRAYFETCH:
@@ -7619,18 +8327,24 @@ sRef_aliasCheckPred (bool (predf) (sRef, exprNode, sRef, exprNode),
   else
     {
       sRefSet aliases = usymtab_allAliases (s);
-
       
       sRefSet_realElements (aliases, current)
 	{
-	  if (sRef_isValid (current))
+	  if (sRef_isReasonable (current))
 	    {
-	      if (!sRef_similar (current, s)
-		  || (error && sRef_sameName (current, s)))
+	      if (sRef_isReasonable (current))
 		{
-		  (void) (*predf)(current, e, s, err);
+		  if (!sRef_similar (current, s)
+		      || (error && sRef_sameName (current, s)))
+		    {
+		      (void) (*predf)(current, e, s, err);
+		    }
 		}
-	      }
+	      else
+		{
+		  llcontbug (message ("Invalid sRef as alias field of %s", sRef_unparse (s)));
+		}
+	    }
 	} end_sRefSet_realElements;
 
       sRefSet_free (aliases);
@@ -7657,7 +8371,7 @@ sRef_aliasCheckSimplePred (sRefTest predf, sRef s)
       
       sRefSet_realElements (aliases, current)
 	{
-	  if (sRef_isValid (current))
+	  if (sRef_isReasonable (current))
 	    {
 	      sRef cref = sRef_updateSref (current);
 	      
@@ -7667,9 +8381,9 @@ sRef_aliasCheckSimplePred (sRefTest predf, sRef s)
 	      ** a great idea.  ;(
 	      */
 	      
-	      	      
 	      if ((*predf)(cref))
 		{
+		  DPRINTF (("Checking alias: %s", sRef_unparseFull (cref)));
 		  sRefSet_free (aliases);
 		  return TRUE;
 		}
@@ -7695,10 +8409,10 @@ sRef_aliasCompleteSimplePred (bool (predf) (sRef), sRef s)
   
   sRefSet_realElements (aliases, current)
     {
-      if (sRef_isValid (current))
+      if (sRef_isReasonable (current))
 	{
-	  	  current = sRef_updateSref (current);
-	  	  if ((*predf)(current)) result = TRUE;
+	  current = sRef_updateSref (current);
+	  if ((*predf)(current)) result = TRUE;
 	}
     } end_sRefSet_realElements;
   
@@ -7706,33 +8420,68 @@ sRef_aliasCompleteSimplePred (bool (predf) (sRef), sRef s)
   return result;
 }
 
-static void
+void
 sRef_aliasSetComplete (void (predf) (sRef, fileloc), sRef s, fileloc loc)
 {
   sRefSet aliases;
   
   aliases = usymtab_allAliases (s);
 
+  DPRINTF (("All aliases: %s", sRefSet_unparseFull (aliases)));
+
   (*predf)(s, loc);
 
   sRefSet_realElements (aliases, current)
     {
-      if (sRef_isValid (current))
+      if (sRef_isReasonable (current))
 	{
 	  current = sRef_updateSref (current);
-	  	  ((*predf)(current, loc));
+	  ((*predf)(current, loc));
+	  DPRINTF (("Killed: %s", sRef_unparseFull (current)));
 	}
     } end_sRefSet_realElements;
 
   sRefSet_free (aliases);
 }
 
-static void
-sRef_aliasSetCompleteParam (void (predf) (sRef, alkind, fileloc), sRef s, 
-			    alkind kind, fileloc loc)
+void
+sRef_aliasSetCompleteParam (void (predf) (sRef, int, fileloc), sRef s, 
+			    int kind, fileloc loc)
 {
   sRefSet aliases;
+  
+  if (sRef_isDeep (s))
+    {
+      aliases = usymtab_allAliases (s);
+    }
+  else
+    {
+      aliases = usymtab_aliasedBy (s);
+    }
+
+  (*predf)(s, kind, loc);
+
+  sRefSet_realElements (aliases, current)
+    {
+      if (sRef_isReasonable (current))
+	{
+	  current = sRef_updateSref (current);
+	  ((*predf)(current, kind, loc));
+	}
+    } end_sRefSet_realElements;
+
+  sRefSet_free (aliases);
+}
+
+/*
+** Version of aliasSetCompleteParam for alkind parameters
+*/
 
+void
+sRef_aliasSetCompleteAlkParam (void (predf) (sRef, alkind, fileloc), sRef s, 
+			       alkind kind, fileloc loc)
+{
+  sRefSet aliases;
   
   if (sRef_isDeep (s))
     {
@@ -7747,10 +8496,10 @@ sRef_aliasSetCompleteParam (void (predf) (sRef, alkind, fileloc), sRef s,
 
   sRefSet_realElements (aliases, current)
     {
-      if (sRef_isValid (current))
+      if (sRef_isReasonable (current))
 	{
 	  current = sRef_updateSref (current);
-	  	  ((*predf)(current, kind, loc));
+	  ((*predf)(current, kind, loc));
 	}
     } end_sRefSet_realElements;
 
@@ -7764,9 +8513,8 @@ sRef_innerAliasSetComplete (void (predf) (sRef, fileloc), sRef s, fileloc loc)
   sRefSet aliases;
   ctype ct;
 
-  if (!sRef_isValid (s)) return;
+  if (!sRef_isReasonable (s)) return;
 
-  
   /*
   ** Type equivalence checking is necessary --- there might be casting.
   */
@@ -7783,18 +8531,16 @@ sRef_innerAliasSetComplete (void (predf) (sRef, fileloc), sRef s, fileloc loc)
       inner = s->info->ref;
       aliases = usymtab_allAliases (inner);
       ct = sRef_getType (inner);
-
       
       sRefSet_realElements (aliases, current)
 	{
-	  if (sRef_isValid (current))
+	  if (sRef_isReasonable (current))
 	    {
 	      current = sRef_updateSref (current);
 	      
 	      if (ctype_equal (ct, sRef_getType (current)))
 		{
 		  sRef ptr = sRef_makePointer (current);
-		  
 		  ((*predf)(ptr, loc));
 		}
 	    }
@@ -7807,28 +8553,44 @@ sRef_innerAliasSetComplete (void (predf) (sRef, fileloc), sRef s, fileloc loc)
       aliases = usymtab_allAliases (inner);
       ct = sRef_getType (inner);
 
+      DPRINTF (("Array fetch: %s", sRefSet_unparse (aliases)));
+
       sRefSet_realElements (aliases, current)
 	{
-	  if (sRef_isValid (current))
+	  if (sRef_isReasonable (current))
 	    {
 	      current = sRef_updateSref (current);
-	      
+	      DPRINTF (("Current: %s", sRef_unparseFull (current)));
+
 	      if (ctype_equal (ct, sRef_getType (current)))
 		{
-		  		  
 		  if (s->info->arrayfetch->indknown)
 		    {
 		      sRef af = sRef_makeArrayFetchKnown (current, s->info->arrayfetch->ind);
-		      
+		      DPRINTF (("Defining: %s", sRef_unparseFull (af)));
+		      /* evans 2001-08-27 This isn't true:
+			   llassert (af->info->arrayfetch->arr == current);
+			 see comments in buildArrayFetchKnown
+		      */
 		      ((*predf)(af, loc));
 		    }
 		  else
 		    {
 		      sRef af = sRef_makeArrayFetch (current);
-		      
+		      /* evans 2001-08-27 This isn't true:
+			 llassert (af->info->arrayfetch->arr == current);
+			 see comments in buildArrayFetch
+		      */ 
+		      DPRINTF (("Defining: %s", sRef_unparseFull (af)));
 		      ((*predf)(af, loc));
 		    }
 		}
+	      else
+		{
+		  DPRINTF (("Type mismatch: %s / %s",
+			    ctype_unparse (ct),
+			    ctype_unparse (sRef_getType (current))));
+		}
 	    }
 	} end_sRefSet_realElements;
 
@@ -7838,11 +8600,10 @@ sRef_innerAliasSetComplete (void (predf) (sRef, fileloc), sRef s, fileloc loc)
       inner = s->info->field->rec;
       aliases = usymtab_allAliases (inner);
       ct = sRef_getType (inner);
-
       
       sRefSet_realElements (aliases, current)
 	{
-	  if (sRef_isValid (current))
+	  if (sRef_isReasonable (current))
 	    {
 	      current = sRef_updateSref (current);
 	      
@@ -7882,9 +8643,8 @@ sRef_innerAliasSetCompleteParam (void (predf) (sRef, sRef), sRef s, sRef t)
   sRefSet aliases;
   ctype ct;
 
-  if (!sRef_isValid (s)) return;
+  if (!sRef_isReasonable (s)) return;
 
-  
   /*
   ** Type equivalence checking is necessary --- there might be casting.
   */
@@ -7901,11 +8661,10 @@ sRef_innerAliasSetCompleteParam (void (predf) (sRef, sRef), sRef s, sRef t)
       inner = s->info->ref;
       aliases = usymtab_allAliases (inner);
       ct = sRef_getType (inner);
-      
-      
+            
       sRefSet_realElements (aliases, current)
 	{
-	  if (sRef_isValid (current))
+	  if (sRef_isReasonable (current))
 	    {
 	      current = sRef_updateSref (current);
 	      
@@ -7927,7 +8686,7 @@ sRef_innerAliasSetCompleteParam (void (predf) (sRef, sRef), sRef s, sRef t)
 
       sRefSet_realElements (aliases, current)
 	{
-	  if (sRef_isValid (current))
+	  if (sRef_isReasonable (current))
 	    {
 	      current = sRef_updateSref (current);
 	      
@@ -7960,7 +8719,7 @@ sRef_innerAliasSetCompleteParam (void (predf) (sRef, sRef), sRef s, sRef t)
       
       sRefSet_realElements (aliases, current)
 	{
-	  if (sRef_isValid (current))
+	  if (sRef_isReasonable (current))
 	    {
 	      current = sRef_updateSref (current);
 	      
@@ -8004,7 +8763,7 @@ static void sRef_combineExKinds (/*@notnull@*/ sRef res, /*@notnull@*/ sRef othe
     }
   else if (a1 == XO_UNKNOWN) 
     { 
-      res->expinfo = alinfo_update (res->expinfo, other->expinfo);
+      res->expinfo = stateInfo_update (res->expinfo, other->expinfo);
       res->expkind = a2;
     }
   else
@@ -8028,11 +8787,13 @@ static void
   alkind ares = sRef_getAliasKind (res);
   alkind aother = sRef_getAliasKind (other);
 
+  sRef_checkMutable (res);
+
   if (alkind_isDependent (ares))
     {
       if (aother == AK_KEPT)
 	{
-	  res->aliasinfo = alinfo_update (res->aliasinfo, other->aliasinfo);
+	  res->aliasinfo = stateInfo_update (res->aliasinfo, other->aliasinfo);
 	  res->aliaskind = AK_KEPT;      
 	}
       else 
@@ -8040,6 +8801,7 @@ static void
 	  if (aother == AK_LOCAL || aother == AK_STATIC 
 	      || alkind_isTemp (aother))
 	    {
+	      DPRINTF (("Setting dependent: %s", sRef_unparseFull (res)));
 	      res->aliaskind = AK_DEPENDENT;
 	    }
 	}
@@ -8054,7 +8816,8 @@ static void
 	{
 	  if (ares == AK_LOCAL || ares == AK_STATIC || alkind_isTemp (ares))
 	    {
-	      res->aliasinfo = alinfo_update (res->aliasinfo, other->aliasinfo);
+	      DPRINTF (("Setting dependent: %s", sRef_unparseFull (res)));
+	      res->aliasinfo = stateInfo_update (res->aliasinfo, other->aliasinfo);
 	      res->aliaskind = AK_DEPENDENT;
 	    }
 	}
@@ -8068,7 +8831,7 @@ static void
       **    don't generate errors
       */
       
-      if (usymtab_isAltProbablyDeepNull (res))
+      if (usymtab_isAltDefinitelyNullDeep (res))
 	{
 	  res->aliaskind = ares;
 	}
@@ -8086,9 +8849,9 @@ static void
       **    don't generate errors
       */
       
-      if (usymtab_isProbableDeepNull (other))
+      if (usymtab_isDefinitelyNullDeep (other))
 	{
-	  res->aliasinfo = alinfo_update (res->aliasinfo, other->aliasinfo);
+	  res->aliasinfo = stateInfo_update (res->aliasinfo, other->aliasinfo);
 	  res->aliaskind = aother;
 	}
       else
@@ -8104,7 +8867,7 @@ static void
   else if (aother == AK_NEWREF && ares == AK_REFCOUNTED
 	   && sRef_isConst (res))
     {
-      res->aliasinfo = alinfo_update (res->aliasinfo, other->aliasinfo);
+      res->aliasinfo = stateInfo_update (res->aliasinfo, other->aliasinfo);
       res->aliaskind = AK_NEWREF;
     }
   else if (sRef_isLocalVar (res)
@@ -8113,6 +8876,16 @@ static void
     {
       res->aliaskind = AK_KEPT;
     }
+  else if ((ares == AK_OWNED && aother == AK_ONLY)
+	   || (aother == AK_OWNED && ares == AK_ONLY))
+    {
+      res->aliaskind = AK_OWNED;
+
+      if (aother == AK_OWNED)
+	{
+	  res->aliasinfo = stateInfo_update (res->aliasinfo, other->aliasinfo);
+	}
+    }
   else
     {
       hasError = TRUE;
@@ -8143,7 +8916,7 @@ static void
 	      if (ares == AK_KEPT || aother == AK_KEPT)
 		{
 		  sRef_maybeKill (res, loc);
-		  		}
+		}
 	    }
 	}
       else 
@@ -8177,6 +8950,10 @@ static void
   alkind ares = sRef_getAliasKind (res);
   alkind aother = sRef_getAliasKind (other);
 
+  sRef_checkMutable (res);
+
+  DPRINTF (("Combine alias kinds: \n\t%s / \n\t%s",
+	    sRef_unparseFull (res), sRef_unparseFull (other)));
   if (alkind_equal (ares, aother)
       || aother == AK_UNKNOWN
       || aother == AK_ERROR)
@@ -8189,12 +8966,14 @@ static void
       res ->aliaskind = AK_ERROR; 
     }
   else if (ares == AK_UNKNOWN || ares == AK_ERROR
-	   || sRef_isStateUndefined (res))
+	   || sRef_isStateUndefined (res)
+	   || sRef_isDefinitelyNull (res))
     { 
-      res->aliasinfo = alinfo_update (res->aliasinfo, other->aliasinfo);
+      res->aliasinfo = stateInfo_update (res->aliasinfo, other->aliasinfo);
       res->aliaskind = aother;  
     }
-  else if (sRef_isStateUndefined (other))
+  else if (sRef_isStateUndefined (other)
+	   || sRef_isDefinitelyNull (other))
     {
       ;
     }
@@ -8205,7 +8984,7 @@ static void
     {
       if (ares != AK_LOCAL)
 	{
-	  res->aliasinfo = alinfo_update (res->aliasinfo, other->aliasinfo);
+	  res->aliasinfo = stateInfo_update (res->aliasinfo, other->aliasinfo);
 	}
 
       res->aliaskind = AK_LOCAL;
@@ -8215,7 +8994,7 @@ static void
     {
       if (ares != AK_FRESH)
 	{
-	  res->aliasinfo = alinfo_update (res->aliasinfo, other->aliasinfo);
+	  res->aliasinfo = stateInfo_update (res->aliasinfo, other->aliasinfo);
 	}
       
       res->aliaskind = AK_FRESH;
@@ -8225,7 +9004,7 @@ static void
     {
       if (ares != AK_KEEP)
 	{
-	  res->aliasinfo = alinfo_update (res->aliasinfo, other->aliasinfo);
+	  res->aliasinfo = stateInfo_update (res->aliasinfo, other->aliasinfo);
 	}
       
       res->aliaskind = AK_KEEP;
@@ -8235,7 +9014,7 @@ static void
     {
       if (ares != AK_STACK)
 	{
-	  res->aliasinfo = alinfo_update (res->aliasinfo, other->aliasinfo);
+	  res->aliasinfo = stateInfo_update (res->aliasinfo, other->aliasinfo);
 	}
 
       res->aliaskind = AK_STACK;
@@ -8247,7 +9026,7 @@ static void
     {
       if (ares != AK_LOCAL)
 	{
-	  res->aliasinfo = alinfo_update (res->aliasinfo, other->aliasinfo);
+	  res->aliasinfo = stateInfo_update (res->aliasinfo, other->aliasinfo);
 	}
 
       res->aliaskind = AK_LOCAL;
@@ -8262,7 +9041,7 @@ static void
     {
       if (ares != AK_FRESH)
 	{
-	  res->aliasinfo = alinfo_update (res->aliasinfo, other->aliasinfo);
+	  res->aliasinfo = stateInfo_update (res->aliasinfo, other->aliasinfo);
 	  res->aliaskind = AK_FRESH;
 	}
     }
@@ -8276,7 +9055,7 @@ static void
 
       if (!sRef_isFresh (res))
 	{
-	  res->aliasinfo = alinfo_update (res->aliasinfo, other->aliasinfo);
+	  res->aliasinfo = stateInfo_update (res->aliasinfo, other->aliasinfo);
 	}
 
       res->aliaskind = AK_FRESH;
@@ -8286,7 +9065,7 @@ static void
     {
       if (!alkind_isStatic (ares))
 	{
-	  res->aliasinfo = alinfo_update (res->aliasinfo, other->aliasinfo);
+	  res->aliasinfo = stateInfo_update (res->aliasinfo, other->aliasinfo);
 	  res->aliaskind = AK_STATIC;
 	}
     }
@@ -8303,6 +9082,8 @@ static void sRef_combineDefState (/*@notnull@*/ sRef res,
   sstate s2 = other->defstate;
   bool flip = FALSE;
 
+  sRef_checkMutable (res);
+
   if (s1 == s2 || s2 == SS_UNKNOWN)
     {
       ;
@@ -8349,7 +9130,7 @@ static void sRef_combineDefState (/*@notnull@*/ sRef res,
 
   if (flip)
     {
-      res->definfo = alinfo_update (res->definfo, other->definfo);
+      res->definfo = stateInfo_update (res->definfo, other->definfo);
       res->defstate = s2;
     }
 }
@@ -8378,10 +9159,12 @@ extern /*@exposed@*/ sRef sRef_makeArrow (sRef s, /*@dependent@*/ cstring f)
 {
   sRef p;
   sRef ret;
-
-    p = sRef_makePointer (s);
+  
+  p = sRef_makePointer (s);
   ret = sRef_makeField (p, f);
-    return ret;
+  DPRINTF (("Arrow: %s => %s",
+	    sRef_unparseFull (s), sRef_unparseFull (ret)));
+  return ret;
 }
 
 extern /*@exposed@*/ sRef sRef_buildArrow (sRef s, cstring f)
@@ -8411,6 +9194,7 @@ static /*@null@*/ sinfo sinfo_copy (/*@notnull@*/ sRef s)
     case SK_PARAM:
       ret = (sinfo) dmalloc (sizeof (*ret));
       ret->paramno = s->info->paramno; 
+      llassert (ret->paramno >= -1);
       break;
 
     case SK_ARRAYFETCH:
@@ -8418,13 +9202,13 @@ static /*@null@*/ sinfo sinfo_copy (/*@notnull@*/ sRef s)
       ret->arrayfetch = (ainfo) dmalloc (sizeof (*ret->arrayfetch));
       ret->arrayfetch->indknown = s->info->arrayfetch->indknown;
       ret->arrayfetch->ind = s->info->arrayfetch->ind;
-      ret->arrayfetch->arr = s->info->arrayfetch->arr;
+      ret->arrayfetch->arr = s->info->arrayfetch->arr; 
       break;
 
     case SK_FIELD:
       ret = (sinfo) dmalloc (sizeof (*ret));
       ret->field = (fldinfo) dmalloc (sizeof (*ret->field));
-      ret->field->rec = s->info->field->rec;
+      ret->field->rec = s->info->field->rec; 
       ret->field->field = s->info->field->field; 
       break;
 
@@ -8438,24 +9222,26 @@ static /*@null@*/ sinfo sinfo_copy (/*@notnull@*/ sRef s)
     case SK_DERIVED:
     case SK_EXTERNAL:
       ret = (sinfo) dmalloc (sizeof (*ret));
-      ret->ref = s->info->ref;	 
+      ret->ref = s->info->ref; /* Ref_copy (s->info->ref); */
       break;
 
     case SK_CONJ:
       ret = (sinfo) dmalloc (sizeof (*ret));
       ret->conj = (cjinfo) dmalloc (sizeof (*ret->conj));
-      ret->conj->a = s->info->conj->a;
-      ret->conj->b = s->info->conj->b;
+      ret->conj->a = s->info->conj->a; /* sRef_copy (s->info->conj->a); */
+      ret->conj->b = s->info->conj->b; /* sRef_copy (s->info->conj->b);*/
       break;
     case SK_SPECIAL:
       ret = (sinfo) dmalloc (sizeof (*ret));
       ret->spec = s->info->spec;
       break;
+
     case SK_UNCONSTRAINED:
     case SK_NEW:
       ret = (sinfo) dmalloc (sizeof (*ret));
       ret->fname = s->info->fname;
       break;
+
     case SK_RESULT:
     case SK_CONST:
     case SK_TYPE:
@@ -8490,6 +9276,7 @@ static /*@null@*/ sinfo sinfo_fullCopy (/*@notnull@*/ sRef s)
     case SK_PARAM:
       ret = (sinfo) dmalloc (sizeof (*ret));
       ret->paramno = s->info->paramno; 
+      llassert (ret->paramno >= -1);
       break;
 
     case SK_ARRAYFETCH:
@@ -8563,6 +9350,7 @@ static void
 
     case SK_PARAM:
       res->info->paramno = other->info->paramno; 
+      llassert (res->info->paramno >= -1);
       break;
 
     case SK_ARRAYFETCH:
@@ -8617,6 +9405,7 @@ static void sinfo_free (/*@special@*/ /*@temp@*/ /*@notnull@*/ sRef s)
   switch (s->kind)
     {
     case SK_CVAR:
+      DPRINTF (("Free sinfo: [%p]", s->info->cvar));
       sfree (s->info->cvar);
       break;
 
@@ -8624,10 +9413,12 @@ static void sinfo_free (/*@special@*/ /*@temp@*/ /*@notnull@*/ sRef s)
       break;
 
     case SK_ARRAYFETCH:
+      DPRINTF (("Free sinfo: [%p]", s->info->arrayfetch));
       sfree (s->info->arrayfetch);
       break;
 
     case SK_FIELD:
+      DPRINTF (("Free sinfo: [%p]", s->info->field));
       sfree (s->info->field); 
       break;
 
@@ -8637,10 +9428,11 @@ static void sinfo_free (/*@special@*/ /*@temp@*/ /*@notnull@*/ sRef s)
     case SK_PTR:
     case SK_ADR:
     case SK_DERIVED:
-    case SK_EXTERNAL:
+    case SK_EXTERNAL: /* is copy now! */
       break;
 
     case SK_CONJ:
+      DPRINTF (("Free sinfo: [%p]", s->info->conj));
       sfree (s->info->conj);
       break;
 
@@ -8654,6 +9446,10 @@ static void sinfo_free (/*@special@*/ /*@temp@*/ /*@notnull@*/ sRef s)
       break;
     }
 
+  if (s->info != NULL) {
+      DPRINTF (("Free sinfo: [%p]", s->info));
+  }
+
   sfree (s->info);
 }
 
@@ -8733,10 +9529,19 @@ static speckind speckind_fromInt (int i)
   return ((speckind) i);
 }
 
+
+static void sRef_updateNullState (/*@notnull@*/ sRef res, /*@notnull@*/ sRef other)
+     /*@modifies res@*/
+{
+  res->nullstate = other->nullstate;
+  res->nullinfo = stateInfo_update (res->nullinfo, other->nullinfo);
+  sRef_resetAliasKind (res);
+}
+
 void sRef_combineNullState (/*@notnull@*/ sRef res, /*@notnull@*/ sRef other)
 {
-  nstate n1 = res->nullstate;
-  nstate n2 = other->nullstate;
+  nstate n1 = sRef_getNullState (res);
+  nstate n2 = sRef_getNullState (other);
   bool flip = FALSE;
   nstate nn = n1;
 
@@ -8786,17 +9591,18 @@ void sRef_combineNullState (/*@notnull@*/ sRef res, /*@notnull@*/ sRef other)
   
   if (flip)
     {
-      res->nullinfo = alinfo_update (res->nullinfo, other->nullinfo);      
+      res->nullinfo = stateInfo_update (res->nullinfo, other->nullinfo);      
     }
 
   res->nullstate = nn;
+  sRef_resetAliasKind (res);
 }
 
 cstring sRef_nullMessage (sRef s)
 {
-  llassert (sRef_isValid (s));
+  llassert (sRef_isReasonable (s));
 
-  switch (s->nullstate)
+  switch (sRef_getNullState (s))
     {
     case NS_DEFNULL:
     case NS_CONSTNULL:
@@ -8809,7 +9615,7 @@ cstring sRef_nullMessage (sRef s)
 
 /*@observer@*/ cstring sRef_ntMessage (sRef s)
 {
-  llassert (sRef_isValid (s));
+  llassert (sRef_isReasonable (s));
 
   switch (s->nullstate)
     {
@@ -8829,7 +9635,7 @@ sRef sRef_fixResultType (/*@returned@*/ sRef s, ctype typ, uentry ue)
   sRef tmp = sRef_undefined;
   sRef ret;
 
-  llassert (sRef_isValid (s));
+  llassert (sRef_isReasonable (s));
 
   switch (s->kind)
     {
@@ -8965,74 +9771,287 @@ bool sRef_isDependent (sRef s)
 
 bool sRef_isOwned (sRef s)
 {
-  return (sRef_isValid (s) && (s->aliaskind == AK_OWNED));
+  return (sRef_isReasonable (s) && (s->aliaskind == AK_OWNED));
 }
 
 bool sRef_isKeep (sRef s) 
 {
-  return (sRef_isValid (s) && (s->aliaskind == AK_KEEP));
+  return (sRef_isReasonable (s) && (s->aliaskind == AK_KEEP));
 }
 
 bool sRef_isTemp (sRef s)
 {
-  return (sRef_isValid (s) && alkind_isTemp (s->aliaskind));
+  return (sRef_isReasonable (s) && alkind_isTemp (s->aliaskind));
 }
 
 bool sRef_isLocalState (sRef s) 
 {
-  return (sRef_isValid (s) && (s->aliaskind == AK_LOCAL));
+  return (sRef_isReasonable (s) && (s->aliaskind == AK_LOCAL));
 }
 
 bool sRef_isUnique (sRef s)
 {
-  return (sRef_isValid (s) && (s->aliaskind == AK_UNIQUE));
+  return (sRef_isReasonable (s) && (s->aliaskind == AK_UNIQUE));
 }
 
 bool sRef_isShared (sRef s) 
 {
-  return (sRef_isValid (s) && (s->aliaskind == AK_SHARED));
+  return (sRef_isReasonable (s) && (s->aliaskind == AK_SHARED));
 }
 
 bool sRef_isExposed (sRef s) 
 {
-  return (sRef_isValid (s) && (s->expkind == XO_EXPOSED));
+  return (sRef_isReasonable (s) && (s->expkind == XO_EXPOSED));
 }
 
 bool sRef_isObserver (sRef s) 
 {
-  return (sRef_isValid (s) && (s->expkind == XO_OBSERVER));
+  return (sRef_isReasonable (s) && (s->expkind == XO_OBSERVER));
 }
 
 bool sRef_isFresh (sRef s) 
 {
-  return (sRef_isValid (s) && (s->aliaskind == AK_FRESH));
+  return (sRef_isReasonable (s) && (s->aliaskind == AK_FRESH));
 }
 
 bool sRef_isDefinitelyNull (sRef s) 
 {
-  return (sRef_isValid (s) && (s->nullstate == NS_DEFNULL 
-			       || s->nullstate == NS_CONSTNULL));
+  return (sRef_isReasonable (s) && (sRef_getNullState (s) == NS_DEFNULL 
+			       || sRef_getNullState (s) == NS_CONSTNULL));
 }
 
 bool sRef_isAllocated (sRef s)
 {
-  return (sRef_isValid (s) && (s->defstate == SS_ALLOCATED));
+  return (sRef_isReasonable (s) && (s->defstate == SS_ALLOCATED));
 }
 
 bool sRef_isStack (sRef s)
 {
-  return (sRef_isValid (s) && (s->aliaskind == AK_STACK));
+  return (sRef_isReasonable (s) && (s->aliaskind == AK_STACK));
+}
+
+bool sRef_isNotNull (sRef s)
+{
+  return (sRef_isValid(s) && (sRef_getNullState (s) == NS_MNOTNULL 
+			      || sRef_getNullState (s) == NS_NOTNULL));
+}
+
+alkind sRef_getAliasKind (sRef s)
+{
+  if (sRef_isValid(s)) {
+    llassert (alkind_isValid (s->aliaskind));
+    return s->aliaskind;
+  }
+
+  return AK_ERROR;
+}
+
+nstate sRef_getNullState (sRef s)
+{
+  if (sRef_isReasonable (s)) {
+    llassert (nstate_isValid (s->nullstate));
+    return s->nullstate;
+  }
+  
+  return NS_UNKNOWN;
+}
+
+void sRef_reflectAnnotation (sRef s, annotationInfo a, fileloc loc)
+{
+  if (sRef_isReasonable (s))
+    {
+      if (!valueTable_isDefined (s->state))
+	{
+	  s->state = valueTable_create (1);
+	  valueTable_insert
+	    (s->state, 
+	     cstring_copy (metaStateInfo_getName (annotationInfo_getState (a))),
+	     stateValue_create (annotationInfo_getValue (a), 
+				stateInfo_makeLoc (loc, SA_DECLARED)));
+	}
+      else
+	{
+	  DPRINTF (("reflect loc: %s", fileloc_unparse (loc)));
+	  valueTable_update 
+	    (s->state,
+	     metaStateInfo_getName (annotationInfo_getState (a)),
+	     stateValue_create (annotationInfo_getValue (a),
+				stateInfo_makeLoc (loc, SA_DECLARED)));
+	  
+	  DPRINTF (("sref: %s", sRef_unparse (s)));
+	  DPRINTF (("sref: %s", sRef_unparseFull (s)));
+	}
+    }
+}
+
+void sRef_setMetaStateValueComplete (sRef s, cstring key, int value, fileloc loc)
+{
+  sRefSet aliases = usymtab_allAliases (s);
+
+  sRef_setMetaStateValue (s, key, value, loc);
+
+  sRefSet_realElements (aliases, current)
+    {
+      if (sRef_isReasonable (current))
+	{
+	  current = sRef_updateSref (current);
+	  sRef_setMetaStateValue (current, key, value, loc);
+	}
+    } end_sRefSet_realElements ;
+
+  sRefSet_free (aliases);
+}
+
+void sRef_setMetaStateValue (sRef s, cstring key, int value, fileloc loc)
+{
+  sRef_checkMutable (s);
+
+  if (sRef_isReasonable (s))
+    {
+      if (!valueTable_isDefined (s->state))
+	{
+	  DPRINTF (("inserting state: %s: %s %d", sRef_unparse (s), key, value));
+	  s->state = valueTable_create (1);
+	  valueTable_insert (s->state, cstring_copy (key),
+			     stateValue_create (value, 
+						stateInfo_makeLoc (loc, SA_CHANGED)));
+	}
+      else
+	{
+	  DPRINTF (("Updating state: %s: %s %d / %s", sRef_unparse (s), key, value,
+		    fileloc_unparse (loc)));
+	  if (valueTable_contains (s->state, key))
+	    {
+	      valueTable_update 
+		(s->state, key, stateValue_create (value,
+						   stateInfo_makeLoc (loc, SA_CHANGED)));
+	    }
+	  else
+	    {
+	      valueTable_insert 
+		(s->state, cstring_copy (key),
+		 stateValue_create (value, stateInfo_makeLoc (loc, SA_CHANGED)));
+	    }
+
+	  DPRINTF (("After: %s", sRef_unparseFull (s)));
+	}
+    }
+}
+
+bool sRef_checkMetaStateValue (sRef s, cstring key, int value)
+{
+  if (sRef_isReasonable (s))
+    {
+      if (valueTable_isDefined (s->state))
+	{
+	  stateValue val;
+	  
+	  DPRINTF (("check state: %s: %s %d", sRef_unparse (s), key, value));
+	  
+	  val = valueTable_lookup (s->state, key);
+	  llassert (stateValue_isDefined (val));
+	  return (stateValue_isError (val)
+		  || stateValue_getValue (val) == value);
+	}
+      else
+	{
+	  return TRUE;
+	}
+    }
+  else
+    {
+      return TRUE;
+    }
+}
+
+/*@observer@*/ stateValue sRef_getMetaStateValue (sRef s, cstring key)
+{
+  if (sRef_isReasonable (s))
+    {
+      if (valueTable_isDefined (s->state))
+	{
+	  stateValue val;
+	  
+	  val = valueTable_lookup (s->state, key);
+	  /* Okay if its not defined, just returns stateValue_undefined */
+	  return val;
+	}
+      else
+	{
+	  return stateValue_undefined;
+	}
+    }
+  else
+    {
+      return stateValue_undefined;
+    }
+}
+
+/*@observer@*/ valueTable sRef_getValueTable (sRef s) 
+{
+  DPRINTF (("Get value table: %s", sRef_unparse (s)));
+
+  if (sRef_isReasonable (s)) 
+    {
+      llassert (sRef_isReasonable (s));
+      DPRINTF (("Value table: %s", valueTable_unparse (s->state)));
+      return s->state;
+    }  
+  else 
+    {
+      DPRINTF (("No value table!"));
+      return valueTable_undefined;
+    }
+}
+
+bool sRef_makeStateSpecial (sRef s)
+{
+  /*
+  ** Default defined state can be made special.
+  */
+
+  llassert (sRef_isReasonable (s));
+
+  if (s->defstate == SS_UNKNOWN || s->defstate == SS_DEFINED || s->defstate == SS_SPECIAL)
+    {
+      /* s->aliaskind = AK_IMPTEMP; */ /* evans 2001-07-23 shouldn't effect alias state */
+      s->defstate = SS_SPECIAL;
+      DPRINTF (("Made special: %s", sRef_unparseFull (s)));
+      return TRUE;
+    }
+  else
+    {
+      /* s->aliaskind = AK_IMPTEMP; */
+      s->defstate = SS_SPECIAL;
+      return FALSE;
+    }
+}
+
+void sRef_markImmutable (sRef s)
+{
+  if (sRef_isReasonable (s))
+    {
+      DPRINTF (("Mark immutable: %s", sRef_unparseFull (s)));
+      s->immut = TRUE;
+    }
+}
+
+bool sRef_definitelyNullContext (sRef s)
+{
+  return (sRef_definitelyNull (s)
+	  || usymtab_isDefinitelyNullDeep (s));
 }
 
-extern bool sRef_isNotNull (sRef s)
+bool sRef_definitelyNullAltContext (sRef s)
 {
-  return (sRef_isValid(s) && (s->nullstate == NS_MNOTNULL 
-			      || s->nullstate == NS_NOTNULL));
+  return (sRef_definitelyNull (s)
+	  || usymtab_isAltDefinitelyNullDeep (s));
 }
 
+
 /* start modifications */
-struct _bbufinfo sRef_getNullTerminatedState (sRef p_s) {
-   struct _bbufinfo BUFSTATE_UNKNOWN;
+struct s_bbufinfo sRef_getNullTerminatedState (sRef p_s) {
+   struct s_bbufinfo BUFSTATE_UNKNOWN;
    BUFSTATE_UNKNOWN.bufstate = BB_NOTNULLTERMINATED;
    BUFSTATE_UNKNOWN.size = 0;
    BUFSTATE_UNKNOWN.len = 0;
@@ -9043,7 +10062,7 @@ struct _bbufinfo sRef_getNullTerminatedState (sRef p_s) {
 }
 
 void sRef_setNullTerminatedState(sRef p_s) {
-   if(sRef_isValid (p_s)) {
+   if(sRef_isReasonable (p_s)) {
       p_s->bufinfo.bufstate = BB_NULLTERMINATED;
    } else {
       llfatalbug( message("sRef_setNT passed a invalid sRef\n"));
@@ -9052,7 +10071,7 @@ void sRef_setNullTerminatedState(sRef p_s) {
 
 
 void sRef_setPossiblyNullTerminatedState(sRef p_s) {
-   if( sRef_isValid (p_s)) {
+   if( sRef_isReasonable (p_s)) {
       p_s->bufinfo.bufstate = BB_POSSIBLYNULLTERMINATED;
    } else {
       llfatalbug( message("sRef_setPossNT passed a invalid sRef\n"));
@@ -9060,7 +10079,7 @@ void sRef_setPossiblyNullTerminatedState(sRef p_s) {
 }
 
 void sRef_setNotNullTerminatedState(sRef p_s) {
-   if( sRef_isValid (p_s)) {
+   if( sRef_isReasonable (p_s)) {
       p_s->bufinfo.bufstate = BB_NOTNULLTERMINATED;
    } else {
       llfatalbug( message("sRef_unsetNT passed a invalid sRef\n"));
@@ -9068,46 +10087,82 @@ void sRef_setNotNullTerminatedState(sRef p_s) {
 }
 
 void sRef_setLen(sRef p_s, int len) {
-   if( sRef_isValid (p_s) && sRef_isNullTerminated(p_s)) {
-      p_s->bufinfo.len = len;
-   } else {
-      llfatalbug( message("sRef_setLen passed a invalid sRef\n"));
-   }
+   if (sRef_isReasonable (p_s) && sRef_isNullTerminated(p_s)) 
+     {
+       p_s->bufinfo.len = len;
+     } 
+   else 
+     {
+       llfatalbug( message("sRef_setLen passed an invalid sRef\n"));
+     }
 }
     
 
 void sRef_setSize(sRef p_s, int size) {
-   if( sRef_isValid(p_s)) {
+   if( sRef_isValid(p_s)) 
+     {
        p_s->bufinfo.size = size;
-   } else {
-      llfatalbug( message("sRef_setSize passed a invalid sRef\n"));
-   }
+     } 
+   else
+     {
+       llfatalbug( message("sRef_setSize passed a invalid sRef\n"));
+     }
 }
 
 void sRef_resetLen(sRef p_s) {
-	if (sRef_isValid (p_s)) {
-		p_s->bufinfo.len = 0;
-	} else {
-		llfatalbug (message ("sRef_setLen passed an invalid sRef\n"));
-	}
+  if (sRef_isReasonable (p_s)) 
+    {
+      p_s->bufinfo.len = 0;
+    }
+  else
+    {
+      llfatalbug (message ("sRef_setLen passed an invalid sRef\n"));
+    }
 }
 
 /*drl7x 11/28/2000 */
 
-bool sRef_isFixedArray (sRef p_s) {
+bool sRef_isFixedArray (sRef p_s) /*@*/ {
   ctype c;
   c = sRef_getType (p_s);
   return ( ctype_isFixedArray (c) );
 }
 
-int sRef_getArraySize (sRef p_s) {
+size_t sRef_getArraySize (sRef p_s) /*@*/ 
+{
   ctype c;
   llassert (sRef_isFixedArray(p_s) );
-
+  DPRINTF (( message ("sRef_getArraySize getting array size for %s", sRef_unparse(p_s) )  ));
+  
   c = sRef_getType (p_s);
+  return (ctype_getArraySize (c));
+}
+
+void sRef_setValue (sRef s, multiVal val)
+{
+  if (!sRef_isReasonable (s))
+    {
+      llcontbuglit ("Unreasonable sRef");
+      llcontbug (message ("sRef: %s", sRef_unparse (s)));
+      return;
+    }
 
-  return (ctype_getArraySize (c) );
+  multiVal_free (s->val);
+  s->val = val;
 }
 
+bool sRef_hasValue (sRef s)
+{
+  return (sRef_isReasonable (s)
+	  && multiVal_isDefined (s->val));
+}
 
+multiVal sRef_getValue (sRef s)
+{
+  if (sRef_isReasonable (s))
+    {
+      return s->val;
+    }
 
+  return multiVal_undefined;
+}