+/*
+** 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));
+}
+