From 9db418be50038672695e39efc7ce61271e64a7d3 Mon Sep 17 00:00:00 2001
From: David Malcolm <dmalcolm@redhat.com>
Date: Fri, 17 May 2019 05:43:31 -0400
Subject: [PATCH 54/54] FIXME: 2019-05-17 WIP on data model

---
 gcc/analyzer/impl-4.cc                             |   22 +-
 gcc/analyzer/region-model.cc                       | 1609 ++++++++++++++------
 gcc/analyzer/region-model.h                        |   65 +-
 gcc/analyzer/supergraph.cc                         |   20 +-
 gcc/analyzer/supergraph.h                          |    2 +
 .../NOT_FOR_UPSTREAM-clang-paper-example-2.c       |    5 +-
 .../NOT_FOR_UPSTREAM-clang-paper-example-3.c       |    4 +
 gcc/testsuite/gcc.dg/analyzer/data-model-1.c       |  486 +++++-
 8 files changed, 1715 insertions(+), 498 deletions(-)

diff --git a/gcc/analyzer/impl-4.cc b/gcc/analyzer/impl-4.cc
index d9f61d6..4e62d51 100644
--- a/gcc/analyzer/impl-4.cc
+++ b/gcc/analyzer/impl-4.cc
@@ -767,6 +767,10 @@ class exploded_node : public dnode
 				 const gcall *stmt,
 				 const program_state &old_state,
 				 program_state *new_state) const;
+  void on_return_for_region_model (const exploded_graph &eg,
+				   const greturn *return_,
+				   const program_state &old_state,
+				   program_state *new_state) const;
 
   void copy_sm_state (const exploded_graph &eg,
 		      path_var lhs,
@@ -2718,6 +2722,7 @@ exploded_node::on_stmt (exploded_graph &eg) const
 		       new_ps->make_path_var (rhs),
 		       old_state,
 		       &new_state);
+      on_return_for_region_model (eg, return_, old_state, &new_state);
     }
 
   if (const gcall *call = dyn_cast <const gcall *> (stmt))
@@ -2804,6 +2809,18 @@ exploded_node::on_call_for_region_model (const exploded_graph &eg,
     new_state->m_region_model->on_call (stmt);
 }
 
+/* FIXME.  */
+
+void
+exploded_node::on_return_for_region_model (const exploded_graph &eg,
+					   const greturn *stmt,
+					   const program_state &old_state,
+					   program_state *new_state) const
+{
+  if (new_state->m_region_model)
+    new_state->m_region_model->on_return (stmt);
+}
+
 /* Copy SM state (if any) from RHS to LHS.  */
 
 void
@@ -4156,7 +4173,7 @@ exploded_graph::add_function_entry (function *fun)
   program_point point = program_point::from_function_entry (m_sg, fun);
   program_state state (m_ext_state);
   if (state.m_region_model)
-    state.m_region_model->push_frame (fun);
+    state.m_region_model->push_frame (fun, NULL);
 
   add_edge (m_origin, get_or_create_node (point, state), NULL);
 }
@@ -4335,6 +4352,9 @@ exploded_graph::process_node (exploded_node *node)
 				 point.make_path_var (src),
 				 state,
 				 &next_state);
+
+	    if (next_state.m_region_model)
+	      next_state.m_region_model->handle_phi (lhs, src);
 	  }
 
 	if (point.m_supernode->m_stmts.length () > 0)
diff --git a/gcc/analyzer/region-model.cc b/gcc/analyzer/region-model.cc
index ad7866c..a7a81c5 100644
--- a/gcc/analyzer/region-model.cc
+++ b/gcc/analyzer/region-model.cc
@@ -91,6 +91,14 @@ region_id::dump_node_name_to_pp (pretty_printer *pp) const
 
 /* class svalue.  */
 
+/* FIXME.  */
+
+bool
+svalue::operator== (const svalue &other) const
+{
+  return false; // FIXME
+}
+
 void
 svalue::print (const region_model &model,
 	       svalue_id this_sid,
@@ -287,6 +295,14 @@ region_kind_to_str (enum region_kind kind)
     }
 }
 
+/* FIXME.  */
+
+bool
+region::operator== (const region &other) const
+{
+  return false; // FIXME
+}
+
 /* class region.  */
 
 void
@@ -743,6 +759,18 @@ stack_region::get_current_frame_id () const
 /* FIXME.  */
 
 void
+stack_region::pop_frame (region_model *model)
+{
+  gcc_assert (m_frame_rids.length () > 0);
+  region_id frame_id = m_frame_rids.pop ();
+
+  // TODO: poison all regions in the frame
+  //gcc_unreachable ();
+}
+
+/* FIXME.  */
+
+void
 stack_region::add_to_hash (inchash::hash &hstate) const
 {
   region::add_to_hash (hstate);
@@ -824,41 +852,71 @@ root_region::dump_child_label (const region_model &model ATTRIBUTE_UNUSED,
 /* FIXME.  */
 
 void
-root_region::push_frame (region_model *model, function *fun)
+root_region::push_frame (region_model *model, function *fun,
+			 vec<svalue_id> *arg_sids)
 {
-  if (m_stack_rid.null_p ())
-    {
-      svalue_id uninit_sid
-	= model->add_svalue (new poisoned_svalue (POISON_KIND_UNINIT));
-      m_stack_rid
-	= model->add_region (new stack_region (model->m_root_rid,
-					       uninit_sid));
-    }
+  gcc_assert (fun);
+  /* arg_sids can be NULL.  */
+
+  ensure_stack_region (model);
   frame_region *region = new frame_region (m_stack_rid, fun);
   region_id frame_rid = model->add_region (region);
 
-  /* FIXME: params have a defined, unknown value; they should not inherit
-     from the poisoned uninit value.  */
-  tree fndecl = fun->decl;
-  for (tree iter_parm = DECL_ARGUMENTS (fndecl); iter_parm;
-       iter_parm = DECL_CHAIN (iter_parm))
+  // TODO: unify these cases by building a vec of unknown?
+
+  if (arg_sids)
     {
-      svalue_id parm_sid
-	= model->add_svalue (new unknown_svalue (TREE_TYPE (iter_parm)));
+      /* Arguments supplied from a caller frame.  */
 
-      region_id parm_rid
-	= region->get_or_create (model, frame_rid, iter_parm,
-				 TREE_TYPE (iter_parm));
-      model->get_region (parm_rid)->set_value (*model, parm_sid);
+      tree fndecl = fun->decl;
+      int idx = 0;
+      for (tree iter_parm = DECL_ARGUMENTS (fndecl); iter_parm;
+	   iter_parm = DECL_CHAIN (iter_parm), ++idx)
+	{
+	  svalue_id arg_sid = (*arg_sids)[idx];
+	  region_id parm_rid
+	    = region->get_or_create (model, frame_rid, iter_parm,
+				     TREE_TYPE (iter_parm));
+	  model->set_value (parm_rid, arg_sid);
+
+	  /* Also do it for default SSA name (sharing the same unknown
+	     value).  */
+	  tree parm_default_ssa = ssa_default_def (fun, iter_parm);
+	  if (parm_default_ssa)
+	    {
+	      region_id defssa_rid
+		= region->get_or_create (model, frame_rid, parm_default_ssa,
+					 TREE_TYPE (iter_parm));
+	      model->set_value (defssa_rid, arg_sid);
+	    }
+	}
+    }
+  else
+    {
+      /* No known arguments (a top-level call within the analysis).  */
 
-      /* Also do it for default SSA name.  */
-      tree parm_default_ssa = ssa_default_def (fun, iter_parm);
-      if (parm_default_ssa)
+      /* Params have a defined, unknown value; they should not inherit
+	 from the poisoned uninit value.  */
+      tree fndecl = fun->decl;
+      for (tree iter_parm = DECL_ARGUMENTS (fndecl); iter_parm;
+	   iter_parm = DECL_CHAIN (iter_parm))
 	{
-	  region_id defssa_rid
-	    = region->get_or_create (model, frame_rid, parm_default_ssa,
+	  region_id parm_rid
+	    = region->get_or_create (model, frame_rid, iter_parm,
 				     TREE_TYPE (iter_parm));
-	  model->get_region (defssa_rid)->set_value (*model, parm_sid);
+	  svalue_id parm_sid
+	    = model->set_to_new_unknown_value (parm_rid, TREE_TYPE (iter_parm));
+
+	  /* Also do it for default SSA name (sharing the same unknown
+	     value).  */
+	  tree parm_default_ssa = ssa_default_def (fun, iter_parm);
+	  if (parm_default_ssa)
+	    {
+	      region_id defssa_rid
+		= region->get_or_create (model, frame_rid, parm_default_ssa,
+					 TREE_TYPE (iter_parm));
+	      model->get_region (defssa_rid)->set_value (*model, parm_sid);
+	    }
 	}
     }
 
@@ -880,6 +938,31 @@ root_region::get_current_frame_id (const region_model &model) const
 
 /* FIXME.  */
 
+void
+root_region::pop_frame (region_model *model)
+{
+  stack_region *stack = model->get_region <stack_region> (m_stack_rid);
+  stack->pop_frame (model);
+}
+
+/* FIXME.  */
+
+region_id
+root_region::ensure_stack_region (region_model *model)
+{
+  if (m_stack_rid.null_p ())
+    {
+      svalue_id uninit_sid
+	= model->add_svalue (new poisoned_svalue (POISON_KIND_UNINIT));
+      m_stack_rid
+	= model->add_region (new stack_region (model->m_root_rid,
+					       uninit_sid));
+    }
+  return m_stack_rid;
+}
+
+/* FIXME.  */
+
 region_id
 root_region::ensure_globals_region (region_model *model)
 {
@@ -918,11 +1001,15 @@ root_region::add_to_hash (inchash::hash &hstate) const
 
 /* class symbolic_region : public map_region.  */
 
+/* FIXME.  */
+
 symbolic_region::symbolic_region (const symbolic_region &other)
 : map_region (other)
 {
 }
 
+/* FIXME.  */
+
 region *
 symbolic_region::clone () const
 {
@@ -931,6 +1018,52 @@ symbolic_region::clone () const
 
 ////////////////////////////////////////////////////////////////////////////
 
+/* struct svalue_constraint.  */
+
+/* FIXME.  */
+
+void
+svalue_constraint::print (const region_model &model, pretty_printer *pp) const
+{
+  model.print_svalue (m_lhs, pp);
+  switch (m_op)
+    {
+    default:
+      gcc_unreachable ();
+    case EQ_EXPR:
+      pp_string (pp, " == ");
+      break;
+    case GE_EXPR:
+      pp_string (pp, " >= ");
+      break;
+    case LE_EXPR:
+      pp_string (pp, " <= ");
+      break;
+    case NE_EXPR:
+      pp_string (pp, " != ");
+      break;
+    case GT_EXPR:
+      pp_string (pp, " > ");
+      break;
+    case LT_EXPR:
+      pp_string (pp, " < ");
+      break;
+    }
+  model.print_svalue (m_rhs, pp);
+}
+
+/* FIXME.  */
+
+bool
+svalue_constraint::operator== (const svalue_constraint &other) const
+{
+  return (m_lhs == other.m_lhs
+	  && m_op == other.m_op
+	  && m_rhs == other.m_rhs);
+}
+
+////////////////////////////////////////////////////////////////////////////
+
 /* class region_model.  */
 
 /* FIXME.  */
@@ -956,6 +1089,10 @@ region_model::region_model (const region_model &other)
   region *region;
   FOR_EACH_VEC_ELT (other.m_regions, i, region)
     m_regions.safe_push (region->clone ());
+
+  svalue_constraint *c;
+  FOR_EACH_VEC_ELT (other.m_constraints, i, c)
+    m_constraints.safe_push (*c);
 }
 
 /* FIXME.  */
@@ -963,8 +1100,35 @@ region_model::region_model (const region_model &other)
 bool
 region_model::operator== (const region_model &other) const
 {
-  // TODO
-  return true; // FIXME
+  /* FIXME: for now, simple equality checking, rather than an attempt
+     to do it independent of ordering.  */
+
+  if (m_root_rid != other.m_root_rid)
+    return false;
+
+  if (m_svalues.length () != other.m_svalues.length ())
+    return false;
+
+  if (m_constraints.length () != other.m_constraints.length ())
+    return false;
+
+  unsigned i;
+  svalue *svalue;
+  FOR_EACH_VEC_ELT (other.m_svalues, i, svalue)
+    if (!(*m_svalues[i] == *other.m_svalues[i]))
+      return false;
+
+  region *region;
+  FOR_EACH_VEC_ELT (other.m_regions, i, region)
+    if (!(*m_regions[i] == *other.m_regions[i]))
+      return false;
+
+  svalue_constraint *c;
+  FOR_EACH_VEC_ELT (other.m_constraints, i, c)
+    if (!(m_constraints[i] == other.m_constraints[i]))
+      return false;
+
+  return true;
 }
 
 /* FIXME.  */
@@ -983,6 +1147,8 @@ region_model::hash () const
   FOR_EACH_VEC_ELT (m_regions, i, region)
     result ^= region->hash ();
 
+  // FIXME: constraints
+
   return result;
 }
 
@@ -1001,7 +1167,7 @@ region_model::print (pretty_printer *pp) const
     {
       if (i > 0)
 	pp_string (pp, ", ");
-      svalue->print (*this, svalue_id::from_int (i), pp);
+      print_svalue (svalue_id::from_int (i), pp);
     }
 
   pp_string (pp, "], regions: [");
@@ -1014,6 +1180,16 @@ region_model::print (pretty_printer *pp) const
       region->print (*this, region_id::from_int (i), pp);
     }
 
+  pp_string (pp, "], constraints: [");
+
+  svalue_constraint *c;
+  FOR_EACH_VEC_ELT (m_constraints, i, c)
+    {
+      if (i > 0)
+	pp_string (pp, ", ");
+      c->print (*this, pp);
+    }
+
   pp_string (pp, "]");
 }
 
@@ -1031,6 +1207,14 @@ region_model::to_str () const
 /* FIXME.  */
 
 void
+region_model::print_svalue (svalue_id sid, pretty_printer *pp) const
+{
+  get_svalue (sid)->print (*this, sid, pp);
+}
+
+/* FIXME.  */
+
+void
 region_model::dump_dot_to_pp (pretty_printer *pp) const
 {
   graphviz_out gv (pp);
@@ -1055,6 +1239,8 @@ region_model::dump_dot_to_pp (pretty_printer *pp) const
   FOR_EACH_VEC_ELT (m_regions, i, region)
     region->dump_dot_to_pp (*this, region_id::from_int (i), pp);
 
+  // FIXME: constraints
+
   /* Terminate "digraph" */
   gv.outdent ();
   pp_string (pp, "}");
@@ -1090,7 +1276,7 @@ region_model::dump_to_pp (pretty_printer *pp) const
 {
   get_region (m_root_rid)->dump_to_pp (*this, m_root_rid, pp, "", true);
 
-  pp_string (pp, "svalues: ");
+  pp_string (pp, "svalues:");
   pp_newline (pp);
   int i;
   svalue *svalue;
@@ -1098,7 +1284,17 @@ region_model::dump_to_pp (pretty_printer *pp) const
     {
       pp_string (pp, "  ");
       svalue_id sid = svalue_id::from_int (i);
-      svalue->print (*this, sid, pp);
+      print_svalue (sid, pp);
+      pp_newline (pp);
+    }
+
+  pp_string (pp, "constraints:");
+  pp_newline (pp);
+  svalue_constraint *c;
+  FOR_EACH_VEC_ELT (m_constraints, i, c)
+    {
+      pp_string (pp, "  ");
+      c->print (*this, pp);
       pp_newline (pp);
     }
 }
@@ -1189,8 +1385,7 @@ region_model::on_assignment (const gassign *assign)
     case ADDR_EXPR:
       {
 	/* LHS = &RHS;  */
-	region_id rhs_rid = get_lvalue (TREE_OPERAND (rhs1, 0));
-	svalue_id ptr_sid = get_svalue_for_region (rhs_rid);
+	svalue_id ptr_sid = get_rvalue (rhs1);
 	set_value (lhs_rid, ptr_sid);
       }
       break;
@@ -1250,6 +1445,53 @@ region_model::on_assignment (const gassign *assign)
       }
       break;
 
+    case NEGATE_EXPR:
+    case BIT_NOT_EXPR:
+      {
+	// TODO: unary ops
+
+	// TODO: constant?
+
+	set_to_new_unknown_value (lhs_rid, TREE_TYPE (lhs));
+      }
+      break;
+
+    case PLUS_EXPR:
+    case MINUS_EXPR:
+    case MULT_EXPR:
+    case TRUNC_DIV_EXPR:
+    case TRUNC_MOD_EXPR:
+    case LSHIFT_EXPR:
+    case RSHIFT_EXPR:
+    case BIT_IOR_EXPR:
+    case BIT_XOR_EXPR:
+    case BIT_AND_EXPR:
+    case MIN_EXPR:
+    case MAX_EXPR:
+      {
+	/* Binary ops.  */
+	tree rhs2 = gimple_assign_rhs2 (assign);
+
+	svalue_id rhs1_sid = get_rvalue (rhs1);
+	svalue_id rhs2_sid = get_rvalue (rhs2);
+
+	if (tree rhs1_cst = maybe_get_constant (rhs1_sid))
+	  if (tree rhs2_cst = maybe_get_constant (rhs2_sid))
+	    {
+	      tree result = fold_build2 (op, TREE_TYPE (lhs),
+					 rhs1_cst, rhs2_cst);
+	      if (CONSTANT_CLASS_P (result))
+		{
+		  svalue_id result_sid
+		    = get_svalue_for_constant (result);
+		  set_value (lhs_rid, result_sid);
+		  return;
+		}
+	    }
+	set_to_new_unknown_value (lhs_rid, TREE_TYPE (lhs));
+      }
+      break;
+
     case COMPONENT_REF:
       {
 	/* LHS = op0.op1;  */
@@ -1266,6 +1508,14 @@ region_model::on_assignment (const gassign *assign)
 void
 region_model::on_call (const gcall *call)
 {
+  region_id lhs_rid;
+  tree lhs_type = NULL_TREE;
+  if (tree lhs = gimple_call_lhs (call))
+    {
+      lhs_rid = get_lvalue (lhs);
+      lhs_type = TREE_TYPE (lhs);
+    }
+
   if (is_named_call_p (call, "malloc", 1))
     {
       // FIXME: we should split state into two outcomes: success and failure
@@ -1279,19 +1529,80 @@ region_model::on_call (const gcall *call)
 
       if (tree lhs = gimple_call_lhs (call))
 	{
-	  tree type = TREE_TYPE (lhs);
-	  svalue_id ptr_sid = add_svalue (new region_svalue (type, new_rid));
-	  region_id lhs_rid = get_lvalue (lhs);
+	  svalue_id ptr_sid
+	    = add_svalue (new region_svalue (lhs_type, new_rid));
 	  set_value (lhs_rid, ptr_sid);
 	}
+      return;
     }
   else if (is_named_call_p (call, "__builtin_alloca", 1))
     {
-      // TODO:
+      region_id frame_rid = get_current_frame_id ();
+      region_id new_rid = add_region (new symbolic_region (frame_rid));
+      if (tree lhs = gimple_call_lhs (call))
+	{
+	  svalue_id ptr_sid
+	    = add_svalue (new region_svalue (lhs_type, new_rid));
+	  set_value (lhs_rid, ptr_sid);
+	}
+      return;
+    }
+  else if (is_named_call_p (call, "strlen", 1))
+    {
+      region_id buf_rid = deref_rvalue (gimple_call_arg (call, 0));
+      svalue_id buf_sid = get_region (buf_rid)->get_value (*this, true);
+      if (tree cst_expr = maybe_get_constant (buf_sid))
+	{
+	  if (TREE_CODE (cst_expr) == STRING_CST
+	      && !lhs_rid.null_p ())
+	    {
+	      /* TREE_STRING_LENGTH is sizeof, not strlen.  */
+	      int sizeof_cst = TREE_STRING_LENGTH (cst_expr);
+	      int strlen_cst = sizeof_cst - 1;
+	      tree t_cst = build_int_cst (lhs_type, strlen_cst);
+	      svalue_id result_sid
+		= get_svalue_for_constant (t_cst);
+	      set_value (lhs_rid, result_sid);
+	      return;
+	    }
+	}
+
+      // FIXME: otherwise an unknown value
 #if 0
       gcc_unreachable ();
 #endif
     }
+
+  /* Unrecognized call.  */
+
+  /* Unknown return value.  */
+  if (!lhs_rid.null_p ())
+    set_to_new_unknown_value (lhs_rid, lhs_type);
+
+  /* TODO: also, any pointer arguments might have been written through,
+     or the things they point to (implying a graph traversal, which
+     presumably we need to do before overwriting the old value).  */
+}
+
+/* FIXME.  */
+
+void
+region_model::on_return (const greturn *return_stmt)
+{
+  tree callee = get_current_function ()->decl;
+  tree lhs = DECL_RESULT (callee);
+  tree rhs = gimple_return_retval (return_stmt);
+
+  if (lhs && rhs)
+    set_value (get_lvalue (lhs), get_rvalue (rhs));
+}
+
+/* FIXME.  */
+
+void
+region_model::handle_phi (tree lhs, tree rhs)
+{
+  set_value (get_lvalue (lhs), get_rvalue (rhs));
 }
 
 /* FIXME.  */
@@ -1349,14 +1660,17 @@ region_model::get_lvalue (tree expr)
 
     case SSA_NAME:
     case PARM_DECL:
+    case RESULT_DECL:
       {
 	// FIXME:
 	gcc_assert (TREE_CODE (expr) == SSA_NAME
 		    || TREE_CODE (expr) == PARM_DECL
-		    || TREE_CODE (expr) == VAR_DECL);
+		    || TREE_CODE (expr) == VAR_DECL
+		    || TREE_CODE (expr) == RESULT_DECL);
 
 	region_id frame_rid = get_current_frame_id ();
 	frame_region *frame = get_region <frame_region> (frame_rid);
+	gcc_assert (frame);
 	region_id child_rid = frame->get_or_create (this, frame_rid, expr,
 						    TREE_TYPE (expr));
 	return child_rid;
@@ -1380,7 +1694,7 @@ region_model::get_lvalue (tree expr)
 	// FIXME: should map to a unique, custom region, containing the constant
 	tree cst_type = TREE_TYPE (expr);
 	map_region *cst_region = new map_region (m_root_rid, cst_type);
-	svalue_id cst_sid = add_svalue (new constant_svalue (expr));
+	svalue_id cst_sid = get_svalue_for_constant (expr);
 	cst_region->set_value (*this, cst_sid);
 	region_id cst_rid = add_region (cst_region);
 	return cst_rid;
@@ -1399,6 +1713,14 @@ region_model::get_rvalue (tree expr)
     default:
       gcc_unreachable ();
 
+    case ADDR_EXPR:
+      {
+	/* "&EXPR".  */
+	region_id expr_rid = get_lvalue (TREE_OPERAND (expr, 0));
+	return get_svalue_for_region (expr_rid);
+      }
+      break;
+
     case ARRAY_REF:
       {
 	region_id element_rid = get_lvalue (expr);
@@ -1412,6 +1734,8 @@ region_model::get_rvalue (tree expr)
 
     case SSA_NAME:
     case VAR_DECL:
+    case PARM_DECL:
+    case RESULT_DECL:
       {
 	region_id var_rid = get_lvalue (expr);
 	return get_region (var_rid)->get_value (*this, true);
@@ -1435,7 +1759,17 @@ region_model::get_svalue_for_region (region_id rid)
 svalue_id
 region_model::get_svalue_for_constant (tree cst_expr)
 {
-  return add_svalue (new constant_svalue (cst_expr));
+  /* Reuse one if it already exists.  */
+  // FIXME: maybe store a map, rather than do linear search?
+  int i;
+  svalue *svalue;
+  FOR_EACH_VEC_ELT (m_svalues, i, svalue)
+    if (constant_svalue *cst_svalue = svalue->dyn_cast_constant_svalue ())
+      if (cst_svalue->get_constant () == cst_expr)
+	return svalue_id::from_int (i);
+
+  svalue_id cst_sid = add_svalue (new constant_svalue (cst_expr));
+  return cst_sid;
 }
 
 /* FIXME.  */
@@ -1452,6 +1786,12 @@ region_model::deref_rvalue (tree ptr)
 	  = ptr_svalue->dyn_cast_region_svalue ())
 	return region_sval->get_pointee ();
 
+      if (constant_svalue *constant_sval
+	  = ptr_svalue->dyn_cast_constant_svalue ())
+	{
+	  gcc_unreachable (); // TODO
+	}
+
       if (unknown_svalue *unknown_sval
 	  = ptr_svalue->dyn_cast_unknown_svalue ())
 	{
@@ -1472,6 +1812,12 @@ region_model::deref_rvalue (tree ptr)
 
 	  return new_rid;
 	}
+
+      if (poisoned_svalue *poisoned_sval
+	  = ptr_svalue->dyn_cast_poisoned_svalue ())
+	{
+	  gcc_unreachable (); // TODO
+	}
     }
 
   gcc_unreachable ();
@@ -1582,9 +1928,87 @@ region_model::eval_condition (svalue_id lhs_sid,
 
   // TODO: try constraints
 
+  /* FIXME: this is a very simplistic implementation.  */
+
+#if 0
+  unsigned i;
+  svalue_constraint *c;
+  FOR_EACH_VEC_ELT (m_constraints, i, c)
+    {
+      if (lhs_sid == c->m_lhs
+	  && rhs_sid == c->m_rhs)
+	{
+	  if (op == c->m_op)
+	    return tristate::TS_TRUE;
+
+	  if (op == EQ_EXPR && c->m_op == NE_EXPR)
+	    return tristate::TS_FALSE;
+	  if (op == NE_EXPR && c->m_op == EQ_EXPR)
+	    return tristate::TS_FALSE;
+	}
+    }
+#endif
+
+  // FIXME: constraints
+
   return tristate::TS_UNKNOWN;
 }
 
+/* FIXME.  */
+
+bool
+region_model::add_constraint (tree lhs, enum tree_code op, tree rhs)
+{
+  svalue_id lhs_sid = get_rvalue (lhs);
+  svalue_id rhs_sid = get_rvalue (rhs);
+
+  tristate t_cond = eval_condition (lhs_sid, op, rhs_sid);
+
+  /* If we already have the condition, do nothing.  */
+  if (t_cond.is_true ())
+    return true;
+
+  /* Reject constraint that contradicts existing knowledge as unsatisfiable.  */
+  if (t_cond.is_false ())
+    return false;
+
+  /* Store the constraint.  */
+
+#if 1
+  /* For now, a trivial implementation.  */
+  m_constraints.safe_push (svalue_constraint (lhs_sid, op, rhs_sid));
+#else
+  svalue *lhs_sval = get_svalue (lhs_sid);
+  svalue *rhs_sval = get_svalue (rhs_sid);
+
+  enum svalue_kind lhs_kind = lhs_sval->get_kind ();
+  enum svalue_kind rhs_kind = rhs_sval->get_kind ();
+
+  if (op == EQ_EXPR
+      && TREE_TYPE (lhs) == TREE_TYPE (rhs))
+    {
+      /* We have lhs_sid == rhs_sid.
+	 Can we merge them?  */
+
+      /* If we have a pair of unknown, then merge them
+	 into one unknown.  */
+#if 0
+      if (lhs_kind == SK_UNKNOWN
+	  && rhs_kind == SK_UNKNOWN)
+#endif
+
+#if 0
+	  replace_svalue (ptr_sid, ptr_val);
+#endif
+      //gcc_unreachable ();
+    }
+#endif
+
+  return true;
+}
+
+/* FIXME.  */
+
 tristate
 region_model::eval_condition (tree lhs,
 			      enum tree_code op,
@@ -1593,17 +2017,202 @@ region_model::eval_condition (tree lhs,
   return eval_condition (get_rvalue (lhs), op, get_rvalue (rhs));
 }
 
+/* If SID is a constant, return the underlying tree value.
+   Otherwise, return NULL_TREE.  */
+
+tree
+region_model::maybe_get_constant (svalue_id sid)
+{
+  gcc_assert (!sid.null_p ());
+  svalue *sval = get_svalue (sid);
+  if (constant_svalue *cst_sval = sval->dyn_cast_constant_svalue ())
+    return cst_sval->get_constant ();
+  return NULL_TREE;
+}
+
+/* FIXME.  */
+
+svalue_id
+region_model::set_to_new_unknown_value (region_id dst_rid, tree type)
+{
+  gcc_assert (!dst_rid.null_p ());
+  svalue_id new_sid = add_svalue (new unknown_svalue (type));
+  set_value (dst_rid, new_sid);
+
+  // TODO: presumably purge all child regions too (but do this in set_value?)
+
+  return new_sid;
+}
+
 /* FIXME.  */
+// FIXME: this also updates frame information
 
 bool
 region_model::apply_constraints_for_edge (const superedge &edge,
 					  const gimple *last_stmt)
 {
+  /* Handle frame updates for interprocedural edges.  */
+  switch (edge.m_kind)
+    {
+    default:
+      break;
+
+    case SUPEREDGE_CALL:
+      {
+	const call_superedge *call_edge
+	  = edge.dyn_cast_call_superedge ();
+	// FIXME: should be an as_a
+	update_for_call_superedge (*call_edge);
+      }
+      break;
+
+    case SUPEREDGE_RETURN:
+      {
+	const return_superedge *return_edge
+	  = edge.dyn_cast_return_superedge ();
+	// FIXME: should be an as_a
+	update_for_return_superedge (*return_edge);
+      }
+      break;
+    }
+
+  // TODO: update constraints
+
+  if (last_stmt == NULL)
+    return true;
+
+  if (const gcond *cond_stmt = dyn_cast <const gcond *> (last_stmt))
+    return apply_constraints_for_gcond (edge, cond_stmt);
+
+  // FIXME: some linker issues with is_a_helper const
+  if (const gswitch *switch_stmt = dyn_cast <gswitch *> (const_cast <gimple *> (last_stmt)))
+    return apply_constraints_for_gswitch (edge, switch_stmt);
+
   return true;
 }
 
 /* FIXME.  */
 
+void
+region_model::update_for_call_superedge (const call_superedge &call_edge)
+{
+  /* Build a vec of argument svalue_id, using the current top
+     frame for resolving tree expressions.  */
+  auto_vec<svalue_id> arg_sids;
+
+  tree callee = call_edge.get_callee_decl ();
+  gcall *call_stmt = call_edge.get_call_stmt ();
+
+  int i = 0;
+  for (tree parm = DECL_ARGUMENTS (callee); parm;
+       parm = DECL_CHAIN (parm), ++i)
+    {
+      tree arg = gimple_call_arg (call_stmt, i);
+      arg_sids.safe_push (get_rvalue (arg));
+    }
+
+  push_frame (call_edge.get_callee_function (), &arg_sids);
+}
+
+/* FIXME.  */
+
+void
+region_model::update_for_return_superedge (const return_superedge &return_edge)
+{
+  tree callee = return_edge.get_callee_decl ();
+  tree result = DECL_RESULT (callee);
+  gcall *call_stmt = return_edge.get_call_stmt ();
+  tree lhs = gimple_call_lhs (call_stmt);
+
+  /* Evaluate the result, within the callee frame.  */
+  svalue_id result_sid;
+  if (lhs)
+    result_sid = get_rvalue (result);
+  pop_frame ();
+
+  /* Set the result of the call, within the caller frame.  */
+  if (lhs)
+    set_value (get_lvalue (lhs), result_sid);
+}
+
+/* FIXME.  */
+
+bool
+region_model::apply_constraints_for_gcond (const superedge &edge,
+					   const gcond *cond_stmt)
+{
+  ::edge cfg_edge = edge.get_any_cfg_edge ();
+  gcc_assert (cfg_edge != NULL);
+  gcc_assert (cfg_edge->flags & (EDGE_TRUE_VALUE | EDGE_FALSE_VALUE));
+
+  enum tree_code op = gimple_cond_code (cond_stmt);
+  tree lhs = gimple_cond_lhs (cond_stmt);
+  tree rhs = gimple_cond_rhs (cond_stmt);
+  if (cfg_edge->flags & EDGE_FALSE_VALUE)
+    op = invert_tree_comparison (op, false /* honor_nans */);
+  return add_constraint (lhs, op, rhs);
+}
+
+/* FIXME.  */
+
+bool
+region_model::apply_constraints_for_gswitch (const superedge &edge,
+					     const gswitch *switch_stmt)
+{
+  // FIXME: use an as_a for this cast:
+  const switch_cfg_superedge &switch_edge = (const switch_cfg_superedge &)edge;
+  tree index  = gimple_switch_index (switch_stmt);
+  tree case_label = switch_edge.get_case_label ();
+  gcc_assert (TREE_CODE (case_label) == CASE_LABEL_EXPR);
+  tree lower_bound = CASE_LOW (case_label);
+  tree upper_bound = CASE_HIGH (case_label);
+  if (lower_bound)
+    {
+      if (upper_bound)
+	{
+	  /* Range.  */
+	  if (!add_constraint (index, GE_EXPR, lower_bound))
+	    return false;
+	  return add_constraint (index, LE_EXPR, upper_bound);
+	}
+      else
+	/* Single-value.  */
+	return add_constraint (index, EQ_EXPR, lower_bound);
+    }
+  else
+    {
+      /* The default case.
+	 Add exclusions based on the other cases.  */
+      for (unsigned other_idx = 1;
+	   other_idx < gimple_switch_num_labels (switch_stmt);
+	   other_idx++)
+	{
+	  tree other_label = gimple_switch_label (switch_stmt,
+						  other_idx);
+	  tree other_lower_bound = CASE_LOW (other_label);
+	  tree other_upper_bound = CASE_HIGH (other_label);
+	  gcc_assert (other_lower_bound);
+	  if (other_upper_bound)
+	    {
+	      /* Exclude this range-valued case.
+		 For now, we just exclude the boundary values.
+		 TODO: exclude the values within the region.  */
+	      if (!add_constraint (index, NE_EXPR, other_lower_bound))
+		return false;
+	      if (!add_constraint (index, NE_EXPR, other_upper_bound))
+		return false;
+	    }
+	  else
+	    /* Exclude this single-valued case.  */
+	    if (!add_constraint (index, NE_EXPR, other_lower_bound))
+	      return false;
+	}
+      return true;
+    }
+}
+
+/* FIXME.  */
+
 root_region *
 region_model::get_root_region () const
 {
@@ -1613,9 +2222,9 @@ region_model::get_root_region () const
 /* FIXME.  */
 
 void
-region_model::push_frame (function *fun)
+region_model::push_frame (function *fun, vec<svalue_id> *arg_sids)
 {
-  get_root_region ()->push_frame (this, fun);
+  get_root_region ()->push_frame (this, fun, arg_sids);
 }
 
 /* FIXME.  */
@@ -1628,6 +2237,24 @@ region_model::get_current_frame_id () const
 
 /* FIXME.  */
 
+function *
+region_model::get_current_function () const
+{
+  region_id frame_id = get_current_frame_id ();
+  frame_region *frame = get_region<frame_region> (frame_id);
+  return frame->get_function ();
+}
+
+/* FIXME.  */
+
+void
+region_model::pop_frame ()
+{
+  get_root_region ()->pop_frame (this);
+}
+
+/* FIXME.  */
+
 svalue_id
 region_model::add_svalue (svalue *sval)
 {
@@ -1714,45 +2341,64 @@ namespace selftest {
 static void
 test_dump ()
 {
-  auto_fix_quotes sentinel;
   region_model model;
+  model.get_root_region ()->ensure_stack_region (&model);
+  model.get_root_region ()->ensure_globals_region (&model);
+  model.get_root_region ()->ensure_heap_region (&model);
+
+  auto_fix_quotes sentinel;
   pretty_printer pp;
   pp_format_decoder (&pp) = default_tree_printer;
   model.dump_to_pp (&pp);
   ASSERT_STREQ (pp_formatted_text (&pp),
 		"r0: {kind: `root', parent: null, sval: null}\n"
-		"svalues: \n");
+		"|-stack: r1: {kind: `stack', parent: r0, sval: sv0}\n"
+		"|  |: sval: sv0: {poisoned: uninit}\n"
+		"|-globals: r2: {kind: `map', parent: r0, sval: null, map: {}}\n"
+		"`-heap: r3: {kind: `heap', parent: r0, sval: sv1}\n"
+		"  |: sval: sv1: {poisoned: uninit}\n"
+		"svalues:\n"
+		"  sv0: {poisoned: uninit}\n"
+		"  sv1: {poisoned: uninit}\n"
+		"constraints:\n");
 }
 
-#if 0
+static void
+test_unique_constants ()
+{
+  tree int_0 = build_int_cst (integer_type_node, 0);
+  tree int_42 = build_int_cst (integer_type_node, 42);
 
-/* Attempt to add the constraint (LHS OP RHS) to PS.
-   Verify that PS remains satisfiable.  */
+  region_model model;
+  ASSERT_EQ (model.get_rvalue (int_0), model.get_rvalue (int_0));
+  ASSERT_NE (model.get_rvalue (int_0), model.get_rvalue (int_42));
+}
 
-#define ADD_SAT_CONSTRAINT(PS, LHS, OP, RHS)				\
-  SELFTEST_BEGIN_STMT							\
-    bool sat = (PS).add_constraint (LHS, OP, RHS);			\
-    ASSERT_TRUE (sat);							\
+/* Attempt to add the constraint (LHS OP RHS) to MODEL.
+   Verify that MODEL remains satisfiable.  */
+
+#define ADD_SAT_CONSTRAINT(MODEL, LHS, OP, RHS)	\
+  SELFTEST_BEGIN_STMT					\
+    bool sat = (MODEL).add_constraint (LHS, OP, RHS);	\
+    ASSERT_TRUE (sat);					\
   SELFTEST_END_STMT
 
-/* Attempt to add the constraint (LHS OP RHS) to PS.
+/* Attempt to add the constraint (LHS OP RHS) to MODEL.
    Verify that the result is not satisfiable.  */
 
-#define ADD_UNSAT_CONSTRAINT(PS, LHS, OP, RHS)				\
-  SELFTEST_BEGIN_STMT							\
-    bool sat = (PS).add_constraint (LHS, OP, RHS);			\
-    ASSERT_FALSE (sat);							\
+#define ADD_UNSAT_CONSTRAINT(MODEL, LHS, OP, RHS)	\
+  SELFTEST_BEGIN_STMT					\
+    bool sat = (MODEL).add_constraint (LHS, OP, RHS);	\
+    ASSERT_FALSE (sat);				\
   SELFTEST_END_STMT
 
 static void
 assert_condition (const location &loc,
-		  path_state &ps,
-		  path_var lhs, tree_code op, path_var rhs,
+		  region_model &model,
+		  tree lhs, tree_code op, tree rhs,
 		  tristate expected)
 {
-  equiv_class_id lhs_ec = ps.get_or_add_equiv_class (lhs);
-  equiv_class_id rhs_ec = ps.get_or_add_equiv_class (rhs);
-  tristate actual = ps.eval_condition (lhs_ec, op, rhs_ec);
+  tristate actual = model.eval_condition (lhs, op, rhs);
   ASSERT_EQ_AT (loc, actual, expected);
 }
 
@@ -1779,368 +2425,376 @@ assert_condition (const location &loc,
 static void
 test_constraint_conditions ()
 {
-  path_var int_42 (build_int_cst (integer_type_node, 42), 0);
-  path_var int_0 (build_int_cst (integer_type_node, 0), 0);
+  tree int_42 = build_int_cst (integer_type_node, 42);
+  tree int_0 = build_int_cst (integer_type_node, 0);
 
-  path_var x (build_decl (UNKNOWN_LOCATION, PARM_DECL,
-			  get_identifier ("x"),
-			  integer_type_node), 0);
-  path_var y (build_decl (UNKNOWN_LOCATION, PARM_DECL,
-			  get_identifier ("y"),
-			  integer_type_node), 0);
-  path_var z (build_decl (UNKNOWN_LOCATION, PARM_DECL,
-			  get_identifier ("z"),
-			  integer_type_node), 0);
+  tree x = build_decl (UNKNOWN_LOCATION, VAR_DECL,
+		      get_identifier ("x"),
+		      integer_type_node);
+  tree y = build_decl (UNKNOWN_LOCATION, VAR_DECL,
+		       get_identifier ("y"),
+		       integer_type_node);
+  tree z = build_decl (UNKNOWN_LOCATION, VAR_DECL,
+		       get_identifier ("z"),
+		       integer_type_node);
 
   /* Self-comparisons.  */
   {
-    path_state ps;
-    ASSERT_CONDITION_TRUE (ps, x, EQ_EXPR, x);
-    ASSERT_CONDITION_TRUE (ps, x, LE_EXPR, x);
-    ASSERT_CONDITION_TRUE (ps, x, GE_EXPR, x);
-    ASSERT_CONDITION_FALSE (ps, x, NE_EXPR, x);
-    ASSERT_CONDITION_FALSE (ps, x, LT_EXPR, x);
-    ASSERT_CONDITION_FALSE (ps, x, GT_EXPR, x);
+    region_model model;
+    ASSERT_CONDITION_TRUE (model, x, EQ_EXPR, x);
+    ASSERT_CONDITION_TRUE (model, x, LE_EXPR, x);
+    ASSERT_CONDITION_TRUE (model, x, GE_EXPR, x);
+    ASSERT_CONDITION_FALSE (model, x, NE_EXPR, x);
+    ASSERT_CONDITION_FALSE (model, x, LT_EXPR, x);
+    ASSERT_CONDITION_FALSE (model, x, GT_EXPR, x);
   }
 
   /* x == y.  */
   {
-    path_state ps;
-    ASSERT_CONDITION_UNKNOWN (ps, x, EQ_EXPR, y);
+    region_model model;
+    ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, y);
 
-    ADD_SAT_CONSTRAINT (ps, x, EQ_EXPR, y);
+    ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, y);
 
-    ASSERT_CONDITION_TRUE (ps, x, EQ_EXPR, y);
-    ASSERT_CONDITION_TRUE (ps, x, LE_EXPR, y);
-    ASSERT_CONDITION_TRUE (ps, x, GE_EXPR, y);
-    ASSERT_CONDITION_FALSE (ps, x, NE_EXPR, y);
-    ASSERT_CONDITION_FALSE (ps, x, LT_EXPR, y);
-    ASSERT_CONDITION_FALSE (ps, x, GT_EXPR, y);
+#if 0
+    ASSERT_CONDITION_TRUE (model, x, EQ_EXPR, y);
+    ASSERT_CONDITION_TRUE (model, x, LE_EXPR, y);
+    ASSERT_CONDITION_TRUE (model, x, GE_EXPR, y);
+    ASSERT_CONDITION_FALSE (model, x, NE_EXPR, y);
+    ASSERT_CONDITION_FALSE (model, x, LT_EXPR, y);
+    ASSERT_CONDITION_FALSE (model, x, GT_EXPR, y);
 
     /* Swapped operands.  */
-    ASSERT_CONDITION_TRUE (ps, y, EQ_EXPR, x);
-    ASSERT_CONDITION_TRUE (ps, y, LE_EXPR, x);
-    ASSERT_CONDITION_TRUE (ps, y, GE_EXPR, x);
-    ASSERT_CONDITION_FALSE (ps, y, NE_EXPR, x);
-    ASSERT_CONDITION_FALSE (ps, y, LT_EXPR, x);
-    ASSERT_CONDITION_FALSE (ps, y, GT_EXPR, x);
+    ASSERT_CONDITION_TRUE (model, y, EQ_EXPR, x);
+    ASSERT_CONDITION_TRUE (model, y, LE_EXPR, x);
+    ASSERT_CONDITION_TRUE (model, y, GE_EXPR, x);
+    ASSERT_CONDITION_FALSE (model, y, NE_EXPR, x);
+    ASSERT_CONDITION_FALSE (model, y, LT_EXPR, x);
+    ASSERT_CONDITION_FALSE (model, y, GT_EXPR, x);
 
     /* Comparison with other var.  */
-    ASSERT_CONDITION_UNKNOWN (ps, x, EQ_EXPR, z);
-    ASSERT_CONDITION_UNKNOWN (ps, x, LE_EXPR, z);
-    ASSERT_CONDITION_UNKNOWN (ps, x, GE_EXPR, z);
-    ASSERT_CONDITION_UNKNOWN (ps, x, NE_EXPR, z);
-    ASSERT_CONDITION_UNKNOWN (ps, x, LT_EXPR, z);
-    ASSERT_CONDITION_UNKNOWN (ps, x, GT_EXPR, z);
+    ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, z);
+    ASSERT_CONDITION_UNKNOWN (model, x, LE_EXPR, z);
+    ASSERT_CONDITION_UNKNOWN (model, x, GE_EXPR, z);
+    ASSERT_CONDITION_UNKNOWN (model, x, NE_EXPR, z);
+    ASSERT_CONDITION_UNKNOWN (model, x, LT_EXPR, z);
+    ASSERT_CONDITION_UNKNOWN (model, x, GT_EXPR, z);
+#endif
   }
 
+#if 0
+
   /* x == y, then y == z  */
   {
-    path_state ps;
-    ASSERT_CONDITION_UNKNOWN (ps, x, EQ_EXPR, y);
-
-    ADD_SAT_CONSTRAINT (ps, x, EQ_EXPR, y);
-    ADD_SAT_CONSTRAINT (ps, y, EQ_EXPR, z);
-
-    ASSERT_CONDITION_TRUE (ps, x, EQ_EXPR, z);
-    ASSERT_CONDITION_TRUE (ps, x, LE_EXPR, z);
-    ASSERT_CONDITION_TRUE (ps, x, GE_EXPR, z);
-    ASSERT_CONDITION_FALSE (ps, x, NE_EXPR, z);
-    ASSERT_CONDITION_FALSE (ps, x, LT_EXPR, z);
-    ASSERT_CONDITION_FALSE (ps, x, GT_EXPR, z);
+    region_model model;
+    ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, y);
+
+    ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, y);
+    ADD_SAT_CONSTRAINT (model, y, EQ_EXPR, z);
+
+    ASSERT_CONDITION_TRUE (model, x, EQ_EXPR, z);
+    ASSERT_CONDITION_TRUE (model, x, LE_EXPR, z);
+    ASSERT_CONDITION_TRUE (model, x, GE_EXPR, z);
+    ASSERT_CONDITION_FALSE (model, x, NE_EXPR, z);
+    ASSERT_CONDITION_FALSE (model, x, LT_EXPR, z);
+    ASSERT_CONDITION_FALSE (model, x, GT_EXPR, z);
   }
 
   /* x != y.  */
   {
-    path_state ps;
+    region_model model;
 
-    ADD_SAT_CONSTRAINT (ps, x, NE_EXPR, y);
+    ADD_SAT_CONSTRAINT (model, x, NE_EXPR, y);
 
-    ASSERT_CONDITION_TRUE (ps, x, NE_EXPR, y);
-    ASSERT_CONDITION_FALSE (ps, x, EQ_EXPR, y);
-    ASSERT_CONDITION_UNKNOWN (ps, x, LE_EXPR, y);
-    ASSERT_CONDITION_UNKNOWN (ps, x, GE_EXPR, y);
-    ASSERT_CONDITION_UNKNOWN (ps, x, LT_EXPR, y);
-    ASSERT_CONDITION_UNKNOWN (ps, x, GT_EXPR, y);
+    ASSERT_CONDITION_TRUE (model, x, NE_EXPR, y);
+    ASSERT_CONDITION_FALSE (model, x, EQ_EXPR, y);
+    ASSERT_CONDITION_UNKNOWN (model, x, LE_EXPR, y);
+    ASSERT_CONDITION_UNKNOWN (model, x, GE_EXPR, y);
+    ASSERT_CONDITION_UNKNOWN (model, x, LT_EXPR, y);
+    ASSERT_CONDITION_UNKNOWN (model, x, GT_EXPR, y);
 
     /* Swapped operands.  */
-    ASSERT_CONDITION_TRUE (ps, y, NE_EXPR, x);
-    ASSERT_CONDITION_FALSE (ps, y, EQ_EXPR, x);
-    ASSERT_CONDITION_UNKNOWN (ps, y, LE_EXPR, x);
-    ASSERT_CONDITION_UNKNOWN (ps, y, GE_EXPR, x);
-    ASSERT_CONDITION_UNKNOWN (ps, y, LT_EXPR, x);
-    ASSERT_CONDITION_UNKNOWN (ps, y, GT_EXPR, x);
+    ASSERT_CONDITION_TRUE (model, y, NE_EXPR, x);
+    ASSERT_CONDITION_FALSE (model, y, EQ_EXPR, x);
+    ASSERT_CONDITION_UNKNOWN (model, y, LE_EXPR, x);
+    ASSERT_CONDITION_UNKNOWN (model, y, GE_EXPR, x);
+    ASSERT_CONDITION_UNKNOWN (model, y, LT_EXPR, x);
+    ASSERT_CONDITION_UNKNOWN (model, y, GT_EXPR, x);
 
     /* Comparison with other var.  */
-    ASSERT_CONDITION_UNKNOWN (ps, x, EQ_EXPR, z);
-    ASSERT_CONDITION_UNKNOWN (ps, x, LE_EXPR, z);
-    ASSERT_CONDITION_UNKNOWN (ps, x, GE_EXPR, z);
-    ASSERT_CONDITION_UNKNOWN (ps, x, NE_EXPR, z);
-    ASSERT_CONDITION_UNKNOWN (ps, x, LT_EXPR, z);
-    ASSERT_CONDITION_UNKNOWN (ps, x, GT_EXPR, z);
+    ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, z);
+    ASSERT_CONDITION_UNKNOWN (model, x, LE_EXPR, z);
+    ASSERT_CONDITION_UNKNOWN (model, x, GE_EXPR, z);
+    ASSERT_CONDITION_UNKNOWN (model, x, NE_EXPR, z);
+    ASSERT_CONDITION_UNKNOWN (model, x, LT_EXPR, z);
+    ASSERT_CONDITION_UNKNOWN (model, x, GT_EXPR, z);
   }
 
   /* x < y.  */
   {
-    path_state ps;
+    region_model model;
 
-    ADD_SAT_CONSTRAINT (ps, x, LT_EXPR, y);
+    ADD_SAT_CONSTRAINT (model, x, LT_EXPR, y);
 
-    ASSERT_CONDITION_TRUE (ps, x, LT_EXPR, y);
-    ASSERT_CONDITION_TRUE (ps, x, LE_EXPR, y);
-    ASSERT_CONDITION_TRUE (ps, x, NE_EXPR, y);
-    ASSERT_CONDITION_FALSE (ps, x, EQ_EXPR, y);
-    ASSERT_CONDITION_FALSE (ps, x, GT_EXPR, y);
-    ASSERT_CONDITION_FALSE (ps, x, GE_EXPR, y);
+    ASSERT_CONDITION_TRUE (model, x, LT_EXPR, y);
+    ASSERT_CONDITION_TRUE (model, x, LE_EXPR, y);
+    ASSERT_CONDITION_TRUE (model, x, NE_EXPR, y);
+    ASSERT_CONDITION_FALSE (model, x, EQ_EXPR, y);
+    ASSERT_CONDITION_FALSE (model, x, GT_EXPR, y);
+    ASSERT_CONDITION_FALSE (model, x, GE_EXPR, y);
 
     /* Swapped operands.  */
-    ASSERT_CONDITION_FALSE (ps, y, LT_EXPR, x);
-    ASSERT_CONDITION_FALSE (ps, y, LE_EXPR, x);
-    ASSERT_CONDITION_TRUE (ps, y, NE_EXPR, x);
-    ASSERT_CONDITION_FALSE (ps, y, EQ_EXPR, x);
-    ASSERT_CONDITION_TRUE (ps, y, GT_EXPR, x);
-    ASSERT_CONDITION_TRUE (ps, y, GE_EXPR, x);
+    ASSERT_CONDITION_FALSE (model, y, LT_EXPR, x);
+    ASSERT_CONDITION_FALSE (model, y, LE_EXPR, x);
+    ASSERT_CONDITION_TRUE (model, y, NE_EXPR, x);
+    ASSERT_CONDITION_FALSE (model, y, EQ_EXPR, x);
+    ASSERT_CONDITION_TRUE (model, y, GT_EXPR, x);
+    ASSERT_CONDITION_TRUE (model, y, GE_EXPR, x);
   }
 
   /* x <= y.  */
   {
-    path_state ps;
+    region_model model;
 
-    ADD_SAT_CONSTRAINT (ps, x, LE_EXPR, y);
+    ADD_SAT_CONSTRAINT (model, x, LE_EXPR, y);
 
-    ASSERT_CONDITION_UNKNOWN (ps, x, LT_EXPR, y);
-    ASSERT_CONDITION_TRUE (ps, x, LE_EXPR, y);
-    ASSERT_CONDITION_UNKNOWN (ps, x, NE_EXPR, y);
-    ASSERT_CONDITION_UNKNOWN (ps, x, EQ_EXPR, y);
-    ASSERT_CONDITION_FALSE (ps, x, GT_EXPR, y);
-    ASSERT_CONDITION_UNKNOWN (ps, x, GE_EXPR, y);
+    ASSERT_CONDITION_UNKNOWN (model, x, LT_EXPR, y);
+    ASSERT_CONDITION_TRUE (model, x, LE_EXPR, y);
+    ASSERT_CONDITION_UNKNOWN (model, x, NE_EXPR, y);
+    ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, y);
+    ASSERT_CONDITION_FALSE (model, x, GT_EXPR, y);
+    ASSERT_CONDITION_UNKNOWN (model, x, GE_EXPR, y);
 
     /* Swapped operands.  */
-    ASSERT_CONDITION_FALSE (ps, y, LT_EXPR, x);
-    ASSERT_CONDITION_UNKNOWN (ps, y, LE_EXPR, x);
-    ASSERT_CONDITION_UNKNOWN (ps, y, NE_EXPR, x);
-    ASSERT_CONDITION_UNKNOWN (ps, y, EQ_EXPR, x);
-    ASSERT_CONDITION_UNKNOWN (ps, y, GT_EXPR, x);
-    ASSERT_CONDITION_TRUE (ps, y, GE_EXPR, x);
+    ASSERT_CONDITION_FALSE (model, y, LT_EXPR, x);
+    ASSERT_CONDITION_UNKNOWN (model, y, LE_EXPR, x);
+    ASSERT_CONDITION_UNKNOWN (model, y, NE_EXPR, x);
+    ASSERT_CONDITION_UNKNOWN (model, y, EQ_EXPR, x);
+    ASSERT_CONDITION_UNKNOWN (model, y, GT_EXPR, x);
+    ASSERT_CONDITION_TRUE (model, y, GE_EXPR, x);
   }
 
   /* x > y.  */
   {
-    path_state ps;
+    region_model model;
 
-    ADD_SAT_CONSTRAINT (ps, x, GT_EXPR, y);
+    ADD_SAT_CONSTRAINT (model, x, GT_EXPR, y);
 
-    ASSERT_CONDITION_TRUE (ps, x, GT_EXPR, y);
-    ASSERT_CONDITION_TRUE (ps, x, GE_EXPR, y);
-    ASSERT_CONDITION_TRUE (ps, x, NE_EXPR, y);
-    ASSERT_CONDITION_FALSE (ps, x, EQ_EXPR, y);
-    ASSERT_CONDITION_FALSE (ps, x, LT_EXPR, y);
-    ASSERT_CONDITION_FALSE (ps, x, LE_EXPR, y);
+    ASSERT_CONDITION_TRUE (model, x, GT_EXPR, y);
+    ASSERT_CONDITION_TRUE (model, x, GE_EXPR, y);
+    ASSERT_CONDITION_TRUE (model, x, NE_EXPR, y);
+    ASSERT_CONDITION_FALSE (model, x, EQ_EXPR, y);
+    ASSERT_CONDITION_FALSE (model, x, LT_EXPR, y);
+    ASSERT_CONDITION_FALSE (model, x, LE_EXPR, y);
 
     /* Swapped operands.  */
-    ASSERT_CONDITION_FALSE (ps, y, GT_EXPR, x);
-    ASSERT_CONDITION_FALSE (ps, y, GE_EXPR, x);
-    ASSERT_CONDITION_TRUE (ps, y, NE_EXPR, x);
-    ASSERT_CONDITION_FALSE (ps, y, EQ_EXPR, x);
-    ASSERT_CONDITION_TRUE (ps, y, LT_EXPR, x);
-    ASSERT_CONDITION_TRUE (ps, y, LE_EXPR, x);
+    ASSERT_CONDITION_FALSE (model, y, GT_EXPR, x);
+    ASSERT_CONDITION_FALSE (model, y, GE_EXPR, x);
+    ASSERT_CONDITION_TRUE (model, y, NE_EXPR, x);
+    ASSERT_CONDITION_FALSE (model, y, EQ_EXPR, x);
+    ASSERT_CONDITION_TRUE (model, y, LT_EXPR, x);
+    ASSERT_CONDITION_TRUE (model, y, LE_EXPR, x);
   }
 
   /* x >= y.  */
   {
-    path_state ps;
+    region_model model;
 
-    ADD_SAT_CONSTRAINT (ps, x, GE_EXPR, y);
+    ADD_SAT_CONSTRAINT (model, x, GE_EXPR, y);
 
-    ASSERT_CONDITION_UNKNOWN (ps, x, GT_EXPR, y);
-    ASSERT_CONDITION_TRUE (ps, x, GE_EXPR, y);
-    ASSERT_CONDITION_UNKNOWN (ps, x, NE_EXPR, y);
-    ASSERT_CONDITION_UNKNOWN (ps, x, EQ_EXPR, y);
-    ASSERT_CONDITION_FALSE (ps, x, LT_EXPR, y);
-    ASSERT_CONDITION_UNKNOWN (ps, x, LE_EXPR, y);
+    ASSERT_CONDITION_UNKNOWN (model, x, GT_EXPR, y);
+    ASSERT_CONDITION_TRUE (model, x, GE_EXPR, y);
+    ASSERT_CONDITION_UNKNOWN (model, x, NE_EXPR, y);
+    ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, y);
+    ASSERT_CONDITION_FALSE (model, x, LT_EXPR, y);
+    ASSERT_CONDITION_UNKNOWN (model, x, LE_EXPR, y);
 
     /* Swapped operands.  */
-    ASSERT_CONDITION_FALSE (ps, y, GT_EXPR, x);
-    ASSERT_CONDITION_UNKNOWN (ps, y, GE_EXPR, x);
-    ASSERT_CONDITION_UNKNOWN (ps, y, NE_EXPR, x);
-    ASSERT_CONDITION_UNKNOWN (ps, y, EQ_EXPR, x);
-    ASSERT_CONDITION_UNKNOWN (ps, y, LT_EXPR, x);
-    ASSERT_CONDITION_TRUE (ps, y, LE_EXPR, x);
+    ASSERT_CONDITION_FALSE (model, y, GT_EXPR, x);
+    ASSERT_CONDITION_UNKNOWN (model, y, GE_EXPR, x);
+    ASSERT_CONDITION_UNKNOWN (model, y, NE_EXPR, x);
+    ASSERT_CONDITION_UNKNOWN (model, y, EQ_EXPR, x);
+    ASSERT_CONDITION_UNKNOWN (model, y, LT_EXPR, x);
+    ASSERT_CONDITION_TRUE (model, y, LE_EXPR, x);
   }
 
   // TODO: implied orderings
 
   /* Constants.  */
   {
-    path_state ps;
-    ASSERT_CONDITION_FALSE (ps, int_0, EQ_EXPR, int_42);
-    ASSERT_CONDITION_TRUE (ps, int_0, NE_EXPR, int_42);
-    ASSERT_CONDITION_TRUE (ps, int_0, LT_EXPR, int_42);
-    ASSERT_CONDITION_TRUE (ps, int_0, LE_EXPR, int_42);
-    ASSERT_CONDITION_FALSE (ps, int_0, GT_EXPR, int_42);
-    ASSERT_CONDITION_FALSE (ps, int_0, GE_EXPR, int_42);
+    region_model model;
+    ASSERT_CONDITION_FALSE (model, int_0, EQ_EXPR, int_42);
+    ASSERT_CONDITION_TRUE (model, int_0, NE_EXPR, int_42);
+    ASSERT_CONDITION_TRUE (model, int_0, LT_EXPR, int_42);
+    ASSERT_CONDITION_TRUE (model, int_0, LE_EXPR, int_42);
+    ASSERT_CONDITION_FALSE (model, int_0, GT_EXPR, int_42);
+    ASSERT_CONDITION_FALSE (model, int_0, GE_EXPR, int_42);
   }
 
   /* x == 0, y == 42.  */
   {
-    path_state ps;
-    ADD_SAT_CONSTRAINT (ps, x, EQ_EXPR, int_0);
-    ADD_SAT_CONSTRAINT (ps, y, EQ_EXPR, int_42);
-
-    ASSERT_CONDITION_TRUE (ps, x, NE_EXPR, y);
-    ASSERT_CONDITION_FALSE (ps, x, EQ_EXPR, y);
-    ASSERT_CONDITION_TRUE (ps, x, LE_EXPR, y);
-    ASSERT_CONDITION_FALSE (ps, x, GE_EXPR, y);
-    ASSERT_CONDITION_TRUE (ps, x, LT_EXPR, y);
-    ASSERT_CONDITION_FALSE (ps, x, GT_EXPR, y);
+    region_model model;
+    ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, int_0);
+    ADD_SAT_CONSTRAINT (model, y, EQ_EXPR, int_42);
+
+    ASSERT_CONDITION_TRUE (model, x, NE_EXPR, y);
+    ASSERT_CONDITION_FALSE (model, x, EQ_EXPR, y);
+    ASSERT_CONDITION_TRUE (model, x, LE_EXPR, y);
+    ASSERT_CONDITION_FALSE (model, x, GE_EXPR, y);
+    ASSERT_CONDITION_TRUE (model, x, LT_EXPR, y);
+    ASSERT_CONDITION_FALSE (model, x, GT_EXPR, y);
   }
 
   /* Unsatisfiable combinations.  */
 
   /* x == y && x != y.  */
   {
-    path_state ps;
-    ADD_SAT_CONSTRAINT (ps, x, EQ_EXPR, y);
-    ADD_UNSAT_CONSTRAINT (ps, x, NE_EXPR, y);
+    region_model model;
+    ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, y);
+    ADD_UNSAT_CONSTRAINT (model, x, NE_EXPR, y);
   }
 
   /* x == 0 then x == 42.  */
   {
-    path_state ps;
-    ADD_SAT_CONSTRAINT (ps, x, EQ_EXPR, int_0);
-    ADD_UNSAT_CONSTRAINT (ps, x, EQ_EXPR, int_42);
+    region_model model;
+    ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, int_0);
+    ADD_UNSAT_CONSTRAINT (model, x, EQ_EXPR, int_42);
   }
 
   /* x == 0 then x != 0.  */
   {
-    path_state ps;
-    ADD_SAT_CONSTRAINT (ps, x, EQ_EXPR, int_0);
-    ADD_UNSAT_CONSTRAINT (ps, x, NE_EXPR, int_0);
+    region_model model;
+    ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, int_0);
+    ADD_UNSAT_CONSTRAINT (model, x, NE_EXPR, int_0);
   }
 
   /* x == 0 then x > 0.  */
   {
-    path_state ps;
-    ADD_SAT_CONSTRAINT (ps, x, EQ_EXPR, int_0);
-    ADD_UNSAT_CONSTRAINT (ps, x, GT_EXPR, int_0);
+    region_model model;
+    ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, int_0);
+    ADD_UNSAT_CONSTRAINT (model, x, GT_EXPR, int_0);
   }
 
   /* x != y && x == y.  */
   {
-    path_state ps;
-    ADD_SAT_CONSTRAINT (ps, x, NE_EXPR, y);
-    ADD_UNSAT_CONSTRAINT (ps, x, EQ_EXPR, y);
+    region_model model;
+    ADD_SAT_CONSTRAINT (model, x, NE_EXPR, y);
+    ADD_UNSAT_CONSTRAINT (model, x, EQ_EXPR, y);
   }
 
   /* x <= y && x > y.  */
   {
-    path_state ps;
-    ADD_SAT_CONSTRAINT (ps, x, LE_EXPR, y);
-    ADD_UNSAT_CONSTRAINT (ps, x, GT_EXPR, y);
+    region_model model;
+    ADD_SAT_CONSTRAINT (model, x, LE_EXPR, y);
+    ADD_UNSAT_CONSTRAINT (model, x, GT_EXPR, y);
   }
 
+#endif
+
   // etc
 }
 
+#if 0
+
 /* FIXME.  */
 
 static void
 test_transitivity ()
 {
-  path_var int_42 (build_int_cst (integer_type_node, 42), 0);
-  path_var int_0 (build_int_cst (integer_type_node, 0), 0);
+  tree int_42 (build_int_cst (integer_type_node, 42), 0);
+  tree int_0 (build_int_cst (integer_type_node, 0), 0);
 
-  path_var a (build_decl (UNKNOWN_LOCATION, PARM_DECL,
+  tree a (build_decl (UNKNOWN_LOCATION, VAR_DECL,
 			  get_identifier ("a"),
-			  integer_type_node), 0);
-  path_var b (build_decl (UNKNOWN_LOCATION, PARM_DECL,
+			  integer_type_node);
+  tree b (build_decl (UNKNOWN_LOCATION, VAR_DECL,
 			  get_identifier ("b"),
-			  integer_type_node), 0);
-  path_var c (build_decl (UNKNOWN_LOCATION, PARM_DECL,
+			  integer_type_node);
+  tree c (build_decl (UNKNOWN_LOCATION, VAR_DECL,
 			  get_identifier ("c"),
-			  integer_type_node), 0);
-  path_var d (build_decl (UNKNOWN_LOCATION, PARM_DECL,
+			  integer_type_node);
+  tree d (build_decl (UNKNOWN_LOCATION, VAR_DECL,
 			  get_identifier ("d"),
-			  integer_type_node), 0);
+			  integer_type_node);
 
   /* a == b, then c == d, then c == b.  */
   {
-    path_state ps;
-    ASSERT_CONDITION_UNKNOWN (ps, a, EQ_EXPR, b);
-    ASSERT_CONDITION_UNKNOWN (ps, b, EQ_EXPR, c);
-    ASSERT_CONDITION_UNKNOWN (ps, c, EQ_EXPR, d);
-    ASSERT_CONDITION_UNKNOWN (ps, a, EQ_EXPR, d);
-
-    ADD_SAT_CONSTRAINT (ps, a, EQ_EXPR, b);
-    ASSERT_CONDITION_TRUE (ps, a, EQ_EXPR, b);
-
-    ADD_SAT_CONSTRAINT (ps, c, EQ_EXPR, d);
-    ASSERT_CONDITION_TRUE (ps, c, EQ_EXPR, d);
-    ASSERT_CONDITION_UNKNOWN (ps, a, EQ_EXPR, d);
-
-    ADD_SAT_CONSTRAINT (ps, c, EQ_EXPR, b);
-    ASSERT_CONDITION_TRUE (ps, c, EQ_EXPR, b);
-    ASSERT_CONDITION_TRUE (ps, a, EQ_EXPR, d);
+    region_model model;
+    ASSERT_CONDITION_UNKNOWN (model, a, EQ_EXPR, b);
+    ASSERT_CONDITION_UNKNOWN (model, b, EQ_EXPR, c);
+    ASSERT_CONDITION_UNKNOWN (model, c, EQ_EXPR, d);
+    ASSERT_CONDITION_UNKNOWN (model, a, EQ_EXPR, d);
+
+    ADD_SAT_CONSTRAINT (model, a, EQ_EXPR, b);
+    ASSERT_CONDITION_TRUE (model, a, EQ_EXPR, b);
+
+    ADD_SAT_CONSTRAINT (model, c, EQ_EXPR, d);
+    ASSERT_CONDITION_TRUE (model, c, EQ_EXPR, d);
+    ASSERT_CONDITION_UNKNOWN (model, a, EQ_EXPR, d);
+
+    ADD_SAT_CONSTRAINT (model, c, EQ_EXPR, b);
+    ASSERT_CONDITION_TRUE (model, c, EQ_EXPR, b);
+    ASSERT_CONDITION_TRUE (model, a, EQ_EXPR, d);
   }
 
   /* Transitivity: "a < b", "b < c" should imply "a < c".  */
   {
-    path_state ps;
-    ADD_SAT_CONSTRAINT (ps, a, LT_EXPR, b);
-    ADD_SAT_CONSTRAINT (ps, b, LT_EXPR, c);
+    region_model model;
+    ADD_SAT_CONSTRAINT (model, a, LT_EXPR, b);
+    ADD_SAT_CONSTRAINT (model, b, LT_EXPR, c);
 
-    ASSERT_CONDITION_TRUE (ps, a, LT_EXPR, c);
-    ASSERT_CONDITION_FALSE (ps, a, EQ_EXPR, c);
+    ASSERT_CONDITION_TRUE (model, a, LT_EXPR, c);
+    ASSERT_CONDITION_FALSE (model, a, EQ_EXPR, c);
   }
 
   /* Transitivity: "a <= b", "b < c" should imply "a < c".  */
   {
-    path_state ps;
-    ADD_SAT_CONSTRAINT (ps, a, LE_EXPR, b);
-    ADD_SAT_CONSTRAINT (ps, b, LT_EXPR, c);
+    region_model model;
+    ADD_SAT_CONSTRAINT (model, a, LE_EXPR, b);
+    ADD_SAT_CONSTRAINT (model, b, LT_EXPR, c);
 
-    ASSERT_CONDITION_TRUE (ps, a, LT_EXPR, c);
-    ASSERT_CONDITION_FALSE (ps, a, EQ_EXPR, c);
+    ASSERT_CONDITION_TRUE (model, a, LT_EXPR, c);
+    ASSERT_CONDITION_FALSE (model, a, EQ_EXPR, c);
   }
 
   /* Transitivity: "a <= b", "b <= c" should imply "a <= c".  */
   {
-    path_state ps;
-    ADD_SAT_CONSTRAINT (ps, a, LE_EXPR, b);
-    ADD_SAT_CONSTRAINT (ps, b, LE_EXPR, c);
+    region_model model;
+    ADD_SAT_CONSTRAINT (model, a, LE_EXPR, b);
+    ADD_SAT_CONSTRAINT (model, b, LE_EXPR, c);
 
-    ASSERT_CONDITION_TRUE (ps, a, LE_EXPR, c);
-    ASSERT_CONDITION_UNKNOWN (ps, a, EQ_EXPR, c);
+    ASSERT_CONDITION_TRUE (model, a, LE_EXPR, c);
+    ASSERT_CONDITION_UNKNOWN (model, a, EQ_EXPR, c);
   }
 
   /* Transitivity: "a > b", "b > c" should imply "a > c".  */
   {
-    path_state ps;
-    ADD_SAT_CONSTRAINT (ps, a, GT_EXPR, b);
-    ADD_SAT_CONSTRAINT (ps, b, GT_EXPR, c);
+    region_model model;
+    ADD_SAT_CONSTRAINT (model, a, GT_EXPR, b);
+    ADD_SAT_CONSTRAINT (model, b, GT_EXPR, c);
 
-    ASSERT_CONDITION_TRUE (ps, a, GT_EXPR, c);
-    ASSERT_CONDITION_FALSE (ps, a, EQ_EXPR, c);
+    ASSERT_CONDITION_TRUE (model, a, GT_EXPR, c);
+    ASSERT_CONDITION_FALSE (model, a, EQ_EXPR, c);
   }
 
   /* Transitivity: "a >= b", "b > c" should imply " a > c".  */
   {
-    path_state ps;
-    ADD_SAT_CONSTRAINT (ps, a, GE_EXPR, b);
-    ADD_SAT_CONSTRAINT (ps, b, GT_EXPR, c);
+    region_model model;
+    ADD_SAT_CONSTRAINT (model, a, GE_EXPR, b);
+    ADD_SAT_CONSTRAINT (model, b, GT_EXPR, c);
 
-    ASSERT_CONDITION_TRUE (ps, a, GT_EXPR, c);
-    ASSERT_CONDITION_FALSE (ps, a, EQ_EXPR, c);
+    ASSERT_CONDITION_TRUE (model, a, GT_EXPR, c);
+    ASSERT_CONDITION_FALSE (model, a, EQ_EXPR, c);
   }
 
   /* Transitivity: "a >= b", "b >= c" should imply "a >= c".  */
   {
-    path_state ps;
-    ADD_SAT_CONSTRAINT (ps, a, GE_EXPR, b);
-    ADD_SAT_CONSTRAINT (ps, b, GE_EXPR, c);
+    region_model model;
+    ADD_SAT_CONSTRAINT (model, a, GE_EXPR, b);
+    ADD_SAT_CONSTRAINT (model, b, GE_EXPR, c);
 
-    ASSERT_CONDITION_TRUE (ps, a, GE_EXPR, c);
-    ASSERT_CONDITION_UNKNOWN (ps, a, EQ_EXPR, c);
+    ASSERT_CONDITION_TRUE (model, a, GE_EXPR, c);
+    ASSERT_CONDITION_UNKNOWN (model, a, EQ_EXPR, c);
   }
 
   /* Transitivity: "(a < b)", "(c < d)", "(b < c)" should
@@ -2150,51 +2804,51 @@ test_transitivity ()
      but also that:
        (a < d).  */
   {
-    path_state ps;
-    ADD_SAT_CONSTRAINT (ps, a, LT_EXPR, b);
-    ADD_SAT_CONSTRAINT (ps, c, LT_EXPR, d);
-    ADD_SAT_CONSTRAINT (ps, b, LT_EXPR, c);
-
-    ASSERT_CONDITION_TRUE (ps, a, LT_EXPR, c);
-    ASSERT_CONDITION_TRUE (ps, b, LT_EXPR, d);
-    ASSERT_CONDITION_TRUE (ps, a, LT_EXPR, d);
+    region_model model;
+    ADD_SAT_CONSTRAINT (model, a, LT_EXPR, b);
+    ADD_SAT_CONSTRAINT (model, c, LT_EXPR, d);
+    ADD_SAT_CONSTRAINT (model, b, LT_EXPR, c);
+
+    ASSERT_CONDITION_TRUE (model, a, LT_EXPR, c);
+    ASSERT_CONDITION_TRUE (model, b, LT_EXPR, d);
+    ASSERT_CONDITION_TRUE (model, a, LT_EXPR, d);
   }
 
   /* Transitivity: "a >= b", "b >= a" should imply that a == b.  */
   {
-    path_state ps;
-    ADD_SAT_CONSTRAINT (ps, a, GE_EXPR, b);
-    ADD_SAT_CONSTRAINT (ps, b, GE_EXPR, a);
+    region_model model;
+    ADD_SAT_CONSTRAINT (model, a, GE_EXPR, b);
+    ADD_SAT_CONSTRAINT (model, b, GE_EXPR, a);
 
     // TODO:
-    ASSERT_CONDITION_TRUE (ps, a, EQ_EXPR, b);
+    ASSERT_CONDITION_TRUE (model, a, EQ_EXPR, b);
   }
 
   /* Transitivity: "a >= b", "b > a" should be impossible.  */
   {
-    path_state ps;
-    ADD_SAT_CONSTRAINT (ps, a, GE_EXPR, b);
-    ADD_UNSAT_CONSTRAINT (ps, b, GT_EXPR, a);
+    region_model model;
+    ADD_SAT_CONSTRAINT (model, a, GE_EXPR, b);
+    ADD_UNSAT_CONSTRAINT (model, b, GT_EXPR, a);
   }
 
   /* Transitivity: "a >= b", "b >= c", "c >= a" should imply
      that a == b == c.  */
   {
-    path_state ps;
-    ADD_SAT_CONSTRAINT (ps, a, GE_EXPR, b);
-    ADD_SAT_CONSTRAINT (ps, b, GE_EXPR, c);
-    ADD_SAT_CONSTRAINT (ps, c, GE_EXPR, a);
+    region_model model;
+    ADD_SAT_CONSTRAINT (model, a, GE_EXPR, b);
+    ADD_SAT_CONSTRAINT (model, b, GE_EXPR, c);
+    ADD_SAT_CONSTRAINT (model, c, GE_EXPR, a);
 
-    ASSERT_CONDITION_TRUE (ps, a, EQ_EXPR, c);
+    ASSERT_CONDITION_TRUE (model, a, EQ_EXPR, c);
   }
 
   /* Transitivity: "a > b", "b > c", "c > a"
      should be impossible.  */
   {
-    path_state ps;
-    ADD_SAT_CONSTRAINT (ps, a, GT_EXPR, b);
-    ADD_SAT_CONSTRAINT (ps, b, GT_EXPR, c);
-    ADD_UNSAT_CONSTRAINT (ps, c, GT_EXPR, a);
+    region_model model;
+    ADD_SAT_CONSTRAINT (model, a, GT_EXPR, b);
+    ADD_SAT_CONSTRAINT (model, b, GT_EXPR, c);
+    ADD_UNSAT_CONSTRAINT (model, c, GT_EXPR, a);
   }
 
 }
@@ -2204,51 +2858,51 @@ test_transitivity ()
 static void
 test_constant_comparisons ()
 {
-  path_var int_3 (build_int_cst (integer_type_node, 3), 0);
-  path_var int_4 (build_int_cst (integer_type_node, 4), 0);
-  path_var int_5 (build_int_cst (integer_type_node, 5), 0);
+  tree int_3 (build_int_cst (integer_type_node, 3), 0);
+  tree int_4 (build_int_cst (integer_type_node, 4), 0);
+  tree int_5 (build_int_cst (integer_type_node, 5), 0);
 
-  path_var int_1023 (build_int_cst (integer_type_node, 1023), 0);
-  path_var int_1024 (build_int_cst (integer_type_node, 1024), 0);
+  tree int_1023 (build_int_cst (integer_type_node, 1023), 0);
+  tree int_1024 (build_int_cst (integer_type_node, 1024), 0);
 
-  path_var a (build_decl (UNKNOWN_LOCATION, PARM_DECL,
+  tree a (build_decl (UNKNOWN_LOCATION, VAR_DECL,
 			  get_identifier ("a"),
-			  integer_type_node), 0);
-  path_var b (build_decl (UNKNOWN_LOCATION, PARM_DECL,
+			  integer_type_node);
+  tree b (build_decl (UNKNOWN_LOCATION, VAR_DECL,
 			  get_identifier ("b"),
-			  integer_type_node), 0);
+			  integer_type_node);
 
   /* Given a >= 1024, then a <= 1023 should be impossible.  */
   {
-    path_state ps;
-    ADD_SAT_CONSTRAINT (ps, a, GE_EXPR, int_1024);
-    ADD_UNSAT_CONSTRAINT (ps, a, LE_EXPR, int_1023);
+    region_model model;
+    ADD_SAT_CONSTRAINT (model, a, GE_EXPR, int_1024);
+    ADD_UNSAT_CONSTRAINT (model, a, LE_EXPR, int_1023);
   }
 
   /* a > 4.  */
   {
-    path_state ps;
-    ADD_SAT_CONSTRAINT (ps, a, GT_EXPR, int_4);
-    ASSERT_CONDITION_TRUE (ps, a, GT_EXPR, int_4);
-    ASSERT_CONDITION_TRUE (ps, a, NE_EXPR, int_3);
-    ASSERT_CONDITION_UNKNOWN (ps, a, NE_EXPR, int_5);
+    region_model model;
+    ADD_SAT_CONSTRAINT (model, a, GT_EXPR, int_4);
+    ASSERT_CONDITION_TRUE (model, a, GT_EXPR, int_4);
+    ASSERT_CONDITION_TRUE (model, a, NE_EXPR, int_3);
+    ASSERT_CONDITION_UNKNOWN (model, a, NE_EXPR, int_5);
   }
 
   /* a <= 4.  */
   {
-    path_state ps;
-    ADD_SAT_CONSTRAINT (ps, a, LE_EXPR, int_4);
-    ASSERT_CONDITION_FALSE (ps, a, GT_EXPR, int_4);
-    ASSERT_CONDITION_FALSE (ps, a, GT_EXPR, int_5);
-    ASSERT_CONDITION_UNKNOWN (ps, a, NE_EXPR, int_3);
+    region_model model;
+    ADD_SAT_CONSTRAINT (model, a, LE_EXPR, int_4);
+    ASSERT_CONDITION_FALSE (model, a, GT_EXPR, int_4);
+    ASSERT_CONDITION_FALSE (model, a, GT_EXPR, int_5);
+    ASSERT_CONDITION_UNKNOWN (model, a, NE_EXPR, int_3);
   }
 
   /* If "a > b" and "a == 3", then "b == 4" ought to be unsatisfiable.  */
   {
-    path_state ps;
-    ADD_SAT_CONSTRAINT (ps, a, GT_EXPR, b);
-    ADD_SAT_CONSTRAINT (ps, a, EQ_EXPR, int_3);
-    ADD_UNSAT_CONSTRAINT (ps, b, EQ_EXPR, int_4);
+    region_model model;
+    ADD_SAT_CONSTRAINT (model, a, GT_EXPR, b);
+    ADD_SAT_CONSTRAINT (model, a, EQ_EXPR, int_3);
+    ADD_UNSAT_CONSTRAINT (model, b, EQ_EXPR, int_4);
   }
 
   /* Various tests of int ranges where there is only one possible candidate.  */
@@ -2256,52 +2910,52 @@ test_constant_comparisons ()
     /* If "a <= 4" && "a > 3", then "a == 4",
        assuming a is of integral type.  */
     {
-      path_state ps;
-      ADD_SAT_CONSTRAINT (ps, a, LE_EXPR, int_4);
-      ADD_SAT_CONSTRAINT (ps, a, GT_EXPR, int_3);
-      ASSERT_CONDITION_TRUE (ps, a, EQ_EXPR, int_4);
+      region_model model;
+      ADD_SAT_CONSTRAINT (model, a, LE_EXPR, int_4);
+      ADD_SAT_CONSTRAINT (model, a, GT_EXPR, int_3);
+      ASSERT_CONDITION_TRUE (model, a, EQ_EXPR, int_4);
     }
 
     /* If "a > 3" && "a <= 4", then "a == 4",
        assuming a is of integral type.  */
     {
-      path_state ps;
-      ADD_SAT_CONSTRAINT (ps, a, GT_EXPR, int_3);
-      ADD_SAT_CONSTRAINT (ps, a, LE_EXPR, int_4);
-      ASSERT_CONDITION_TRUE (ps, a, EQ_EXPR, int_4);
+      region_model model;
+      ADD_SAT_CONSTRAINT (model, a, GT_EXPR, int_3);
+      ADD_SAT_CONSTRAINT (model, a, LE_EXPR, int_4);
+      ASSERT_CONDITION_TRUE (model, a, EQ_EXPR, int_4);
     }
     /* If "a > 3" && "a < 5", then "a == 4",
        assuming a is of integral type.  */
     {
-      path_state ps;
-      ADD_SAT_CONSTRAINT (ps, a, GT_EXPR, int_3);
-      ADD_SAT_CONSTRAINT (ps, a, LT_EXPR, int_5);
-      ASSERT_CONDITION_TRUE (ps, a, EQ_EXPR, int_4);
+      region_model model;
+      ADD_SAT_CONSTRAINT (model, a, GT_EXPR, int_3);
+      ADD_SAT_CONSTRAINT (model, a, LT_EXPR, int_5);
+      ASSERT_CONDITION_TRUE (model, a, EQ_EXPR, int_4);
     }
     /* If "a >= 4" && "a < 5", then "a == 4",
        assuming a is of integral type.  */
     {
-      path_state ps;
-      ADD_SAT_CONSTRAINT (ps, a, GE_EXPR, int_4);
-      ADD_SAT_CONSTRAINT (ps, a, LT_EXPR, int_5);
-      ASSERT_CONDITION_TRUE (ps, a, EQ_EXPR, int_4);
+      region_model model;
+      ADD_SAT_CONSTRAINT (model, a, GE_EXPR, int_4);
+      ADD_SAT_CONSTRAINT (model, a, LT_EXPR, int_5);
+      ASSERT_CONDITION_TRUE (model, a, EQ_EXPR, int_4);
     }
     /* If "a >= 4" && "a <= 4", then "a == 4".  */
     {
-      path_state ps;
-      ADD_SAT_CONSTRAINT (ps, a, GE_EXPR, int_4);
-      ADD_SAT_CONSTRAINT (ps, a, LE_EXPR, int_4);
-      ASSERT_CONDITION_TRUE (ps, a, EQ_EXPR, int_4);
+      region_model model;
+      ADD_SAT_CONSTRAINT (model, a, GE_EXPR, int_4);
+      ADD_SAT_CONSTRAINT (model, a, LE_EXPR, int_4);
+      ASSERT_CONDITION_TRUE (model, a, EQ_EXPR, int_4);
     }
   }
 
 #if 0
   /* As above, but for float.   */
   {
-    path_state ps;
-    ADD_SAT_CONSTRAINT (ps, f, GT_EXPR, float_3);
-    ADD_SAT_CONSTRAINT (ps, f, LE_EXPR, float_4);
-    ASSERT_CONDITION_UNKNOWN (ps, f, EQ_EXPR, int_4);
+    region_model model;
+    ADD_SAT_CONSTRAINT (model, f, GT_EXPR, float_3);
+    ADD_SAT_CONSTRAINT (model, f, LE_EXPR, float_4);
+    ASSERT_CONDITION_UNKNOWN (model, f, EQ_EXPR, int_4);
   }
 #endif
 }
@@ -2311,83 +2965,83 @@ test_constant_comparisons ()
 static void
 test_constraint_impl ()
 {
-  path_var int_42 (build_int_cst (integer_type_node, 42), 0);
-  path_var int_0 (build_int_cst (integer_type_node, 0), 0);
+  tree int_42 (build_int_cst (integer_type_node, 42), 0);
+  tree int_0 (build_int_cst (integer_type_node, 0), 0);
 
-  path_var x (build_decl (UNKNOWN_LOCATION, PARM_DECL,
+  tree x (build_decl (UNKNOWN_LOCATION, VAR_DECL,
 			  get_identifier ("x"),
-			  integer_type_node), 0);
-  path_var y (build_decl (UNKNOWN_LOCATION, PARM_DECL,
+			  integer_type_node);
+  tree y (build_decl (UNKNOWN_LOCATION, VAR_DECL,
 			  get_identifier ("y"),
-			  integer_type_node), 0);
-  path_var z (build_decl (UNKNOWN_LOCATION, PARM_DECL,
+			  integer_type_node);
+  tree z (build_decl (UNKNOWN_LOCATION, VAR_DECL,
 			  get_identifier ("z"),
-			  integer_type_node), 0);
+			  integer_type_node);
 
   /* x == y.  */
   {
-    path_state ps;
+    region_model model;
 
-    ADD_SAT_CONSTRAINT (ps, x, EQ_EXPR, y);
+    ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, y);
 
-    /* Assert various things about the insides of ps.  */
-    ASSERT_EQ (ps.m_constraints.length (), 0);
-    ASSERT_EQ (ps.m_equiv_classes.length (), 1);
+    /* Assert various things about the insides of model.  */
+    ASSERT_EQ (model.m_constraints.length (), 0);
+    ASSERT_EQ (model.m_equiv_classes.length (), 1);
   }
 
   /* y <= z; x == y.  */
   {
-    path_state ps;
-    ASSERT_CONDITION_UNKNOWN (ps, x, EQ_EXPR, y);
-    ASSERT_CONDITION_UNKNOWN (ps, x, GE_EXPR, z);
+    region_model model;
+    ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, y);
+    ASSERT_CONDITION_UNKNOWN (model, x, GE_EXPR, z);
 
-    ADD_SAT_CONSTRAINT (ps, y, GE_EXPR, z);
-    ASSERT_CONDITION_TRUE (ps, y, GE_EXPR, z);
-    ASSERT_CONDITION_UNKNOWN (ps, x, GE_EXPR, z);
+    ADD_SAT_CONSTRAINT (model, y, GE_EXPR, z);
+    ASSERT_CONDITION_TRUE (model, y, GE_EXPR, z);
+    ASSERT_CONDITION_UNKNOWN (model, x, GE_EXPR, z);
 
-    ADD_SAT_CONSTRAINT (ps, x, EQ_EXPR, y);
+    ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, y);
 
-    /* Assert various things about the insides of ps.  */
-    ASSERT_EQ (ps.m_constraints.length (), 1);
-    ASSERT_EQ (ps.m_equiv_classes.length (), 2);
+    /* Assert various things about the insides of model.  */
+    ASSERT_EQ (model.m_constraints.length (), 1);
+    ASSERT_EQ (model.m_equiv_classes.length (), 2);
 
     /* Ensure that we merged the constraints.  */
-    ASSERT_CONDITION_TRUE (ps, x, GE_EXPR, z);
+    ASSERT_CONDITION_TRUE (model, x, GE_EXPR, z);
   }
 
   /* y <= z; y == x.  */
   {
-    path_state ps;
-    ASSERT_CONDITION_UNKNOWN (ps, x, EQ_EXPR, y);
-    ASSERT_CONDITION_UNKNOWN (ps, x, GE_EXPR, z);
+    region_model model;
+    ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, y);
+    ASSERT_CONDITION_UNKNOWN (model, x, GE_EXPR, z);
 
-    ADD_SAT_CONSTRAINT (ps, y, GE_EXPR, z);
-    ASSERT_CONDITION_TRUE (ps, y, GE_EXPR, z);
-    ASSERT_CONDITION_UNKNOWN (ps, x, GE_EXPR, z);
+    ADD_SAT_CONSTRAINT (model, y, GE_EXPR, z);
+    ASSERT_CONDITION_TRUE (model, y, GE_EXPR, z);
+    ASSERT_CONDITION_UNKNOWN (model, x, GE_EXPR, z);
 
-    ADD_SAT_CONSTRAINT (ps, y, EQ_EXPR, x);
+    ADD_SAT_CONSTRAINT (model, y, EQ_EXPR, x);
 
-    /* Assert various things about the insides of ps.  */
-    ASSERT_EQ (ps.m_constraints.length (), 1);
-    ASSERT_EQ (ps.m_equiv_classes.length (), 2);
+    /* Assert various things about the insides of model.  */
+    ASSERT_EQ (model.m_constraints.length (), 1);
+    ASSERT_EQ (model.m_equiv_classes.length (), 2);
 
     /* Ensure that we merged the constraints.  */
-    ASSERT_CONDITION_TRUE (ps, x, GE_EXPR, z);
+    ASSERT_CONDITION_TRUE (model, x, GE_EXPR, z);
   }
 
   /* x == 0, then x != 42.  */
   {
-    path_state ps;
+    region_model model;
 
-    ADD_SAT_CONSTRAINT (ps, x, EQ_EXPR, int_0);
-    ADD_SAT_CONSTRAINT (ps, x, NE_EXPR, int_42);
+    ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, int_0);
+    ADD_SAT_CONSTRAINT (model, x, NE_EXPR, int_42);
 
-    /* Assert various things about the insides of ps.  */
-    ASSERT_EQ (ps.m_constraints.length (), 1);
-    ASSERT_EQ (ps.m_equiv_classes.length (), 2);
-    ASSERT_EQ (ps.m_constraints[0].m_lhs, ps.get_or_add_equiv_class (int_0));
-    ASSERT_EQ (ps.m_constraints[0].m_rhs, ps.get_or_add_equiv_class (int_42));
-    ASSERT_EQ (ps.m_constraints[0].m_op, CONSTRAINT_LT);
+    /* Assert various things about the insides of model.  */
+    ASSERT_EQ (model.m_constraints.length (), 1);
+    ASSERT_EQ (model.m_equiv_classes.length (), 2);
+    ASSERT_EQ (model.m_constraints[0].m_lhs, model.get_or_add_equiv_class (int_0));
+    ASSERT_EQ (model.m_constraints[0].m_rhs, model.get_or_add_equiv_class (int_42));
+    ASSERT_EQ (model.m_constraints[0].m_op, CONSTRAINT_LT);
   }
 
   // TODO: selftest for merging ecs "in the middle"
@@ -2401,21 +3055,21 @@ test_constraint_impl ()
 static void
 test_assignment ()
 {
-  path_var int_0 (build_int_cst (integer_type_node, 0), 0);
+  tree int_0 (build_int_cst (integer_type_node, 0), 0);
 
-  path_var x (build_decl (UNKNOWN_LOCATION, PARM_DECL,
+  tree x (build_decl (UNKNOWN_LOCATION, VAR_DECL,
 			  get_identifier ("x"),
-			  integer_type_node), 0);
-  path_var y (build_decl (UNKNOWN_LOCATION, PARM_DECL,
+			  integer_type_node);
+  tree y (build_decl (UNKNOWN_LOCATION, VAR_DECL,
 			  get_identifier ("y"),
-			  integer_type_node), 0);
+			  integer_type_node);
   /* "x == 0", then use of y, then "y = 0".  */
-  path_state ps;
-  ADD_SAT_CONSTRAINT (ps, x, EQ_EXPR, int_0);
-  ASSERT_CONDITION_UNKNOWN (ps, y, EQ_EXPR, int_0);
-  ps.on_assignment (y, int_0);
-  ASSERT_CONDITION_TRUE (ps, y, EQ_EXPR, int_0);
-  ASSERT_CONDITION_TRUE (ps, y, EQ_EXPR, x);
+  region_model model;
+  ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, int_0);
+  ASSERT_CONDITION_UNKNOWN (model, y, EQ_EXPR, int_0);
+  model.on_assignment (y, int_0);
+  ASSERT_CONDITION_TRUE (model, y, EQ_EXPR, int_0);
+  ASSERT_CONDITION_TRUE (model, y, EQ_EXPR, x);
 }
 
 /* FIXME.  */
@@ -2427,25 +3081,25 @@ test_stack_frames ()
   path_var int_0 (build_int_cst (integer_type_node, 0), 0);
 
   /* "a" in the parent frame.  */
-  path_var a (build_decl (UNKNOWN_LOCATION, PARM_DECL,
+  path_var a (build_decl (UNKNOWN_LOCATION, VAR_DECL,
 			  get_identifier ("a"),
-			  integer_type_node), 0);
+			  integer_type_node);
   /* "x" in a child frame.  */
-  path_var x (build_decl (UNKNOWN_LOCATION, PARM_DECL,
+  path_var x (build_decl (UNKNOWN_LOCATION, VAR_DECL,
 			  get_identifier ("x"),
 			  integer_type_node), 1);
 
   {
-    path_state ps;
-    ps.m_stack_depth = 1;
+    region_model model;
+    model.m_stack_depth = 1;
 
     /* x == a.  */
-    ADD_SAT_CONSTRAINT (ps, x, EQ_EXPR, a);
-    ASSERT_CONDITION_TRUE (ps, x, EQ_EXPR, a);
+    ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, a);
+    ASSERT_CONDITION_TRUE (model, x, EQ_EXPR, a);
 
     /* Pop the stack.  */
-    ps.pop_stack_frame ();
-    ASSERT_CONDITION_UNKNOWN (ps, x, EQ_EXPR, a);
+    model.pop_stack_frame ();
+    ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, a);
   }
 }
 
@@ -2455,35 +3109,35 @@ test_stack_frames ()
 static void
 test_equality ()
 {
-  path_var int_42 (build_int_cst (integer_type_node, 42), 0);
-  path_var int_0 (build_int_cst (integer_type_node, 0), 0);
+  tree int_42 (build_int_cst (integer_type_node, 42), 0);
+  tree int_0 (build_int_cst (integer_type_node, 0), 0);
 
-  path_var x (build_decl (UNKNOWN_LOCATION, PARM_DECL,
+  tree x (build_decl (UNKNOWN_LOCATION, VAR_DECL,
 			  get_identifier ("x"),
-			  integer_type_node), 0);
-  path_var y (build_decl (UNKNOWN_LOCATION, PARM_DECL,
+			  integer_type_node);
+  tree y (build_decl (UNKNOWN_LOCATION, VAR_DECL,
 			  get_identifier ("y"),
-			  integer_type_node), 0);
-  path_var z (build_decl (UNKNOWN_LOCATION, PARM_DECL,
+			  integer_type_node);
+  tree z (build_decl (UNKNOWN_LOCATION, VAR_DECL,
 			  get_identifier ("z"),
-			  integer_type_node), 0);
+			  integer_type_node);
 
   {
-    path_state ps0;
-    path_state ps1;
+    region_model model0;
+    region_model model1;
 
-    ASSERT_EQ (ps0.hash (), ps1.hash ());
-    ASSERT_EQ (ps0, ps1);
+    ASSERT_EQ (model0.hash (), model1.hash ());
+    ASSERT_EQ (model0, model1);
 
-    ADD_SAT_CONSTRAINT (ps1, x, EQ_EXPR, y);
-    ASSERT_NE (ps0.hash (), ps1.hash ());
-    ASSERT_NE (ps0, ps1);
+    ADD_SAT_CONSTRAINT (model1, x, EQ_EXPR, y);
+    ASSERT_NE (model0.hash (), model1.hash ());
+    ASSERT_NE (model0, model1);
 
-    path_state ps2;
-    /* Make the same change to ps2.  */
-    ADD_SAT_CONSTRAINT (ps2, x, EQ_EXPR, y);
-    ASSERT_EQ (ps1.hash (), ps2.hash ());
-    ASSERT_EQ (ps1, ps2);
+    region_model model2;
+    /* Make the same change to model2.  */
+    ADD_SAT_CONSTRAINT (model2, x, EQ_EXPR, y);
+    ASSERT_EQ (model1.hash (), model2.hash ());
+    ASSERT_EQ (model1, model2);
   }
 }
 
@@ -2506,82 +3160,82 @@ test_purging ()
   path_var int_42 (build_int_cst (integer_type_node, 42), 0);
   path_var int_0 (build_int_cst (integer_type_node, 0), 0);
 
-  path_var x (build_decl (UNKNOWN_LOCATION, PARM_DECL,
+  path_var x (build_decl (UNKNOWN_LOCATION, VAR_DECL,
 			  get_identifier ("x"),
-			  integer_type_node), 0);
-  path_var y (build_decl (UNKNOWN_LOCATION, PARM_DECL,
+			  integer_type_node);
+  path_var y (build_decl (UNKNOWN_LOCATION, VAR_DECL,
 			  get_identifier ("y"),
-			  integer_type_node), 0);
+			  integer_type_node);
 
   {
-    path_state ps0;
-    path_state ps1;
+    region_model model0;
+    region_model model1;
 
-    ADD_SAT_CONSTRAINT (ps1, x, EQ_EXPR, y);
-    ASSERT_NE (ps0, ps1);
+    ADD_SAT_CONSTRAINT (model1, x, EQ_EXPR, y);
+    ASSERT_NE (model0, model1);
 
     purge_one_path_var px (x);
-    ps1.purge (px);
+    model1.purge (px);
 
     purge_one_path_var py (y);
-    ps1.purge (py);
+    model1.purge (py);
 
-    ASSERT_EQ (ps0, ps1);
+    ASSERT_EQ (model0, model1);
   }
 
   {
-    path_state ps0;
-    path_state ps1;
+    region_model model0;
+    region_model model1;
 
-    ADD_SAT_CONSTRAINT (ps1, x, EQ_EXPR, int_42);
-    ASSERT_NE (ps0, ps1);
+    ADD_SAT_CONSTRAINT (model1, x, EQ_EXPR, int_42);
+    ASSERT_NE (model0, model1);
 
     purge_one_path_var px (x);
-    ps1.purge (px);
+    model1.purge (px);
 
-    ASSERT_EQ (ps0, ps1);
+    ASSERT_EQ (model0, model1);
   }
 
   {
-    path_state ps0;
-    path_state ps1;
+    region_model model0;
+    region_model model1;
 
-    ADD_SAT_CONSTRAINT (ps1, x, GE_EXPR, int_0);
-    ADD_SAT_CONSTRAINT (ps1, x, LE_EXPR, int_42);
-    ASSERT_NE (ps0, ps1);
+    ADD_SAT_CONSTRAINT (model1, x, GE_EXPR, int_0);
+    ADD_SAT_CONSTRAINT (model1, x, LE_EXPR, int_42);
+    ASSERT_NE (model0, model1);
 
     purge_one_path_var px (x);
-    ps1.purge (px);
+    model1.purge (px);
 
-    ASSERT_EQ (ps0, ps1);
+    ASSERT_EQ (model0, model1);
   }
 
   {
-    path_state ps0;
-    path_state ps1;
+    region_model model0;
+    region_model model1;
 
-    ADD_SAT_CONSTRAINT (ps1, x, NE_EXPR, int_42);
-    ADD_SAT_CONSTRAINT (ps1, y, NE_EXPR, int_0);
-    ASSERT_NE (ps0, ps1);
+    ADD_SAT_CONSTRAINT (model1, x, NE_EXPR, int_42);
+    ADD_SAT_CONSTRAINT (model1, y, NE_EXPR, int_0);
+    ASSERT_NE (model0, model1);
 
     purge_one_path_var px (x);
-    ps1.purge (px);
-    ASSERT_NE (ps0, ps1);
+    model1.purge (px);
+    ASSERT_NE (model0, model1);
 
-    ASSERT_CONDITION_TRUE (ps1, y, NE_EXPR, int_0);
+    ASSERT_CONDITION_TRUE (model1, y, NE_EXPR, int_0);
   }
 
   {
-    path_state ps0;
-    path_state ps1;
+    region_model model0;
+    region_model model1;
 
-    ADD_SAT_CONSTRAINT (ps1, x, NE_EXPR, int_42);
-    ADD_SAT_CONSTRAINT (ps1, y, NE_EXPR, int_0);
-    ASSERT_NE (ps0, ps1);
+    ADD_SAT_CONSTRAINT (model1, x, NE_EXPR, int_42);
+    ADD_SAT_CONSTRAINT (model1, y, NE_EXPR, int_0);
+    ASSERT_NE (model0, model1);
 
     purge_all_path_vars p;
-    ps1.purge (p);
-    ASSERT_EQ (ps0, ps1);
+    model1.purge (p);
+    ASSERT_EQ (model0, model1);
   }
 
 }
@@ -2594,8 +3248,9 @@ void
 analyzer_region_model_cc_tests ()
 {
   test_dump ();
-#if 0
+  test_unique_constants ();
   test_constraint_conditions ();
+#if 0
   test_transitivity ();
   test_constant_comparisons ();
   test_constraint_impl ();
diff --git a/gcc/analyzer/region-model.h b/gcc/analyzer/region-model.h
index 5a2a1b0..faf2cc5 100644
--- a/gcc/analyzer/region-model.h
+++ b/gcc/analyzer/region-model.h
@@ -31,6 +31,7 @@ class superedge;
 class svalue;
   class region_svalue;
   class constant_svalue;
+  class poisoned_svalue;
   class unknown_svalue;
 class region;
 class region_model;
@@ -49,6 +50,16 @@ public:
 
   svalue_id () : m_idx (-1) {}
 
+  bool operator== (const svalue_id &other) const
+  {
+    return m_idx == other.m_idx;
+  }
+
+  bool operator!= (const svalue_id &other) const
+  {
+    return m_idx != other.m_idx;
+  }
+
   bool null_p () const { return m_idx == -1; }
 
   static svalue_id from_int (int idx) { return svalue_id (idx); }
@@ -116,6 +127,8 @@ class svalue
 public:
   virtual ~svalue () {}
 
+  bool operator== (const svalue &other) const;
+
   virtual svalue *clone () const = 0;
 
   tree get_type () const { return m_type; }
@@ -136,6 +149,7 @@ public:
 
   virtual region_svalue *dyn_cast_region_svalue () { return NULL; }
   virtual constant_svalue *dyn_cast_constant_svalue () { return NULL; }
+  virtual poisoned_svalue *dyn_cast_poisoned_svalue () { return NULL; }
   virtual unknown_svalue *dyn_cast_unknown_svalue () { return NULL; }
 
  protected:
@@ -264,6 +278,8 @@ public:
 
   hashval_t hash () const FINAL OVERRIDE;
 
+  poisoned_svalue *dyn_cast_poisoned_svalue () FINAL OVERRIDE { return this; }
+
  private:
   void print_details (const region_model &model,
 		      svalue_id this_sid,
@@ -307,6 +323,8 @@ class region
 public:
   virtual ~region () {}
 
+  bool operator== (const region &other) const;
+
   virtual region *clone () const = 0;
 
   virtual enum region_kind get_kind () const = 0;
@@ -458,6 +476,7 @@ public:
 
   void push_frame (region_id frame_rid);
   region_id get_current_frame_id () const;
+  void pop_frame (region_model *model);
 
  private:
   void add_to_hash (inchash::hash &hstate) const FINAL OVERRIDE;
@@ -504,9 +523,12 @@ public:
 			 pretty_printer *pp) const
     FINAL OVERRIDE;
 
-  void push_frame (region_model *model, function *fun);
+  void push_frame (region_model *model, function *fun,
+		   vec<svalue_id> *arg_sids);
   region_id get_current_frame_id (const region_model &model) const;
+  void pop_frame (region_model *model);
 
+  region_id ensure_stack_region (region_model *model);
   region_id ensure_globals_region (region_model *model);
   region_id ensure_heap_region (region_model *model);
 
@@ -539,6 +561,25 @@ public:
 
 ////////////////////////////////////////////////////////////////////////////
 
+/* FIXME: a very simple implementation of constraints.  */
+
+struct svalue_constraint
+{
+  svalue_constraint (svalue_id lhs, enum tree_code op, svalue_id rhs)
+  : m_lhs (lhs), m_op (op), m_rhs (rhs)
+  {}
+
+  bool operator== (const svalue_constraint &other) const;
+
+  void print (const region_model &model, pretty_printer *pp) const;
+
+  svalue_id m_lhs;
+  enum tree_code m_op;
+  svalue_id m_rhs;
+};
+
+////////////////////////////////////////////////////////////////////////////
+
 /* A region_model encapsulates a representation of the state of memory, with
    a tree of regions, along with their associated values.
    The representation is graph-like because values can be pointers to
@@ -557,6 +598,8 @@ class region_model
   void print (pretty_printer *pp) const;
   std::string to_str () const;
 
+  void print_svalue (svalue_id sid, pretty_printer *pp) const;
+
   void dump_dot_to_pp (pretty_printer *pp) const;
   void dump_dot_to_file (FILE *fp) const;
   void dump_dot (const char *path) const;
@@ -569,14 +612,18 @@ class region_model
 
   void on_assignment (const gassign *stmt);
   void on_call (const gcall *stmt);
+  void on_return (const greturn *stmt);
+  void handle_phi (tree lhs, tree rhs);
 
   bool apply_constraints_for_edge (const superedge &edge,
 				   const gimple *last_stmt);
 
   root_region *get_root_region () const;
 
-  void push_frame (function *fun);
+  void push_frame (function *fun, vec<svalue_id> *arg_sids);
   region_id get_current_frame_id () const;
+  function * get_current_function () const;
+  void pop_frame ();
 
   svalue_id add_svalue (svalue *sval);
   void replace_svalue (svalue_id sid, svalue *new_sval);
@@ -605,20 +652,32 @@ class region_model
   region_id deref_rvalue (tree ptr);
 
   void set_value (region_id lhs_rid, svalue_id rhs_sid);
+  svalue_id set_to_new_unknown_value (region_id dst_rid, tree type);
 
   tristate eval_condition (svalue_id lhs,
 			   enum tree_code op,
 			   svalue_id rhs) const;
-
   tristate eval_condition (tree lhs,
 			   enum tree_code op,
 			   tree rhs);
+  bool add_constraint (tree lhs, enum tree_code op, tree rhs);
+
+  tree maybe_get_constant (svalue_id sid);
 
  private:
+  void update_for_call_superedge (const call_superedge &call_edge);
+  void update_for_return_superedge (const return_superedge &return_edge);
+  bool apply_constraints_for_gcond (const superedge &edge,
+				    const gcond *cond_stmt);
+  bool apply_constraints_for_gswitch (const superedge &edge,
+				      const gswitch *switch_stmt);
+
   auto_delete_vec<svalue> m_svalues;
  public: // FIXME:
   auto_delete_vec<region> m_regions;
   region_id m_root_rid;
+ private:
+  auto_vec<svalue_constraint> m_constraints; // TODO hash, copy-ctor, etc
 };
 
 namespace inchash
diff --git a/gcc/analyzer/supergraph.cc b/gcc/analyzer/supergraph.cc
index a3324b1..04cfa55 100644
--- a/gcc/analyzer/supergraph.cc
+++ b/gcc/analyzer/supergraph.cc
@@ -823,10 +823,26 @@ callgraph_superedge::dump_label_to_pp (pretty_printer *pp) const
 
 /* FIXME.  */
 
+function *
+callgraph_superedge::get_callee_function () const
+{
+  return m_cedge->callee->get_fun ();
+}
+
+/* FIXME.  */
+
+function *
+callgraph_superedge::get_caller_function () const
+{
+  return m_cedge->caller->get_fun ();
+}
+
+/* FIXME.  */
+
 tree
 callgraph_superedge::get_callee_decl () const
 {
-  return m_cedge->callee->get_fun ()->decl;
+  return get_callee_function ()->decl;
 }
 
 /* FIXME.  */
@@ -834,7 +850,7 @@ callgraph_superedge::get_callee_decl () const
 tree
 callgraph_superedge::get_caller_decl () const
 {
-  return m_cedge->caller->get_fun ()->decl;
+  return get_caller_function ()->decl;
 }
 
 /* FIXME.  */
diff --git a/gcc/analyzer/supergraph.h b/gcc/analyzer/supergraph.h
index 4c4e3b6..b01bc96 100644
--- a/gcc/analyzer/supergraph.h
+++ b/gcc/analyzer/supergraph.h
@@ -304,6 +304,8 @@ class callgraph_superedge : public superedge
 
   void dump_label_to_pp (pretty_printer *pp) const OVERRIDE;
 
+  function *get_callee_function () const;
+  function *get_caller_function () const;
   tree get_callee_decl () const;
   tree get_caller_decl () const;
   gcall *get_call_stmt () const { return m_cedge->call_stmt; }
diff --git a/gcc/testsuite/gcc.dg/analyzer/NOT_FOR_UPSTREAM-clang-paper-example-2.c b/gcc/testsuite/gcc.dg/analyzer/NOT_FOR_UPSTREAM-clang-paper-example-2.c
index 054e7da..93e7f1a 100644
--- a/gcc/testsuite/gcc.dg/analyzer/NOT_FOR_UPSTREAM-clang-paper-example-2.c
+++ b/gcc/testsuite/gcc.dg/analyzer/NOT_FOR_UPSTREAM-clang-paper-example-2.c
@@ -1,3 +1,5 @@
+/* { dg-additional-options "-fanalyzer-region-model" } */
+
 #include <stdlib.h>
 
 void test_2 (void)
@@ -11,8 +13,7 @@ void test_2 (void)
 
   char c = buf1[0];
 
-  __analyzer_eval (c == 0); /* { dg-warning "TRUE" "" { xfail *-*-* } } */
-  /* { dg-warning "UNKNOWN" "" { target *-*-* } .-1 } */
+  __analyzer_eval (c == 0); /* { dg-warning "TRUE" } */
 
   free (p);
 }
diff --git a/gcc/testsuite/gcc.dg/analyzer/NOT_FOR_UPSTREAM-clang-paper-example-3.c b/gcc/testsuite/gcc.dg/analyzer/NOT_FOR_UPSTREAM-clang-paper-example-3.c
index 57ed9dd..5310c38 100644
--- a/gcc/testsuite/gcc.dg/analyzer/NOT_FOR_UPSTREAM-clang-paper-example-3.c
+++ b/gcc/testsuite/gcc.dg/analyzer/NOT_FOR_UPSTREAM-clang-paper-example-3.c
@@ -1,3 +1,5 @@
+/* { dg-additional-options "-fanalyzer-region-model" } */
+
 #include <stdlib.h>
 
 struct s1
@@ -17,4 +19,6 @@ void test_3 (void)
   sp->p = &data; /* { dg-warning "use of possibly-NULL 'sp'" } */
   sp->p->d = 3;
   a[1] = data.d;
+  __analyzer_eval (a[1] == 3); /* { dg-warning "TRUE" } */
+
 } /* { dg-warning "leak of 'sp'" } */
diff --git a/gcc/testsuite/gcc.dg/analyzer/data-model-1.c b/gcc/testsuite/gcc.dg/analyzer/data-model-1.c
index 039a0e7..7583a1c 100644
--- a/gcc/testsuite/gcc.dg/analyzer/data-model-1.c
+++ b/gcc/testsuite/gcc.dg/analyzer/data-model-1.c
@@ -140,15 +140,10 @@ void test_12 (void)
   void *p = alloca (256);
   void *q = alloca (256);
 
-  __analyzer_eval (p == q); /* { dg-warning "FALSE" "" { xfail *-*-* } } */
-  /* { dg-warning "TRUE" "" { target *-*-* } .-1 } */
-  // TODO(xfail): alloca results should be unique
-  // FIXME: I think the region_model code isn't seeing the calls, and is treating them
-  // as uninitialized, and treating all uninit values
-  // as equal
+  /* alloca results should be unique.  */
+  __analyzer_eval (p == q); /* { dg-warning "FALSE" } */
 
   // FIXME: complain about uses of poisoned values
-  // FIXME: have a separate test for this
 }
 
 /* Use of uninit value.  */
@@ -239,11 +234,72 @@ void test_16 (void)
   /* { dg-warning "UNKNOWN" "" { target *-*-* } .-1 } */
   // TODO(xfail)
 
-  __analyzer_eval (strlen (msg) == 11); /* { dg-warning "TRUE" "" { xfail *-*-* } } */
+  __analyzer_eval (strlen (msg) == 11); /* { dg-warning "TRUE" } */
+}
+
+void test_16a (const char *msg)
+{
+  __analyzer_eval (strlen (msg) == 11); /* { dg-warning "UNKNOWN" } */
+}
+
+void test_16b (const char *msg)
+{
+  __analyzer_eval (strlen (msg) == strlen (msg)); /* { dg-warning "TRUE" "" { xfail *-*-* } } */
   /* { dg-warning "UNKNOWN" "" { target *-*-* } .-1 } */
   // TODO(xfail)
 }
 
+extern int unknown_result (void);
+
+void test_16c (int i)
+{
+  int j;
+
+  j = i;
+  __analyzer_eval (j == i); /* { dg-warning "TRUE" } */
+
+  j = unknown_result ();
+  __analyzer_eval (j == i); /* { dg-warning "UNKNOWN" } */
+}
+
+void test_16c_a (void)
+{
+  int i, j;
+
+  i = unknown_result ();
+  j = unknown_result ();
+  __analyzer_eval (i == j); /* { dg-warning "UNKNOWN" } */
+}
+
+int global_int_16d;
+
+void test_16d (int i)
+{
+  global_int_16d = i;
+  __analyzer_eval (global_int_16d == i); /* { dg-warning "TRUE" } */
+
+  global_int_16d = unknown_result ();
+  __analyzer_eval (global_int_16d == i); /* { dg-warning "UNKNOWN" } */
+}
+
+extern void might_write_to (int *);
+
+void test_16e (int i)
+{
+  int j;
+
+  j = i;
+  __analyzer_eval (j == i); /* { dg-warning "TRUE" } */
+
+  might_write_to (&j);
+  __analyzer_eval (j == i); /* { dg-warning "UNKNOWN" "" { xfail *-*-* } } */
+  /* { dg-warning "TRUE" "" { target *-*-* } .-1 } */
+  // TODO(xfail)
+}
+
+/* TODO: and more complicated graph-like examples, where anything that's
+   reachable from the pointer might be modified.  */
+
 void test_17 (int i)
 {
   int j = 42;
@@ -270,6 +326,401 @@ void test_18 (int i)
   __analyzer_eval (i < j); /* { dg-warning "FALSE" } */
 }
 
+void test_19 (void)
+{
+  int i, j;
+  /* Compare two uninitialized locals.  */
+    __analyzer_eval (i == j); /* { dg-warning "UNKNOWN" "" { xfail *-*-* } } */
+  /* { dg-warning "TRUE" "" { target *-*-* } .-1 } */
+  // TODO(xfail)
+}
+
+void test_20 (int i, int j)
+{
+  __analyzer_eval (i + 1); /* { dg-warning "UNKNOWN" } */
+  __analyzer_eval (i + j); /* { dg-warning "UNKNOWN" } */
+
+  __analyzer_eval (i - 1); /* { dg-warning "UNKNOWN" } */
+  __analyzer_eval (i - j); /* { dg-warning "UNKNOWN" } */
+
+  __analyzer_eval (i * 2); /* { dg-warning "UNKNOWN" } */
+  __analyzer_eval (i * j); /* { dg-warning "UNKNOWN" } */
+
+  __analyzer_eval (i / 2); /* { dg-warning "UNKNOWN" } */
+  __analyzer_eval (i / j); /* { dg-warning "UNKNOWN" } */
+
+  __analyzer_eval (i % 2); /* { dg-warning "UNKNOWN" } */
+  __analyzer_eval (i % j); /* { dg-warning "UNKNOWN" } */
+
+  __analyzer_eval (i & 1); /* { dg-warning "UNKNOWN" } */
+  __analyzer_eval (i & j); /* { dg-warning "UNKNOWN" } */
+
+  __analyzer_eval (i | 1); /* { dg-warning "UNKNOWN" } */
+  __analyzer_eval (i | j); /* { dg-warning "UNKNOWN" } */
+
+  __analyzer_eval (i ^ 1); /* { dg-warning "UNKNOWN" } */
+  __analyzer_eval (i ^ j); /* { dg-warning "UNKNOWN" } */
+
+  __analyzer_eval (i >> 1); /* { dg-warning "UNKNOWN" } */
+  __analyzer_eval (i >> j); /* { dg-warning "UNKNOWN" } */
+
+  __analyzer_eval (i << 1); /* { dg-warning "UNKNOWN" } */
+  __analyzer_eval (i << j); /* { dg-warning "UNKNOWN" } */
+
+  __analyzer_eval (i && 0); /* { dg-warning "FALSE" } */
+  __analyzer_eval (i && 1); /* { dg-warning "UNKNOWN" } */
+  __analyzer_eval (i && j); /* { dg-warning "UNKNOWN" "" { xfail *-*-* } } */
+  /* { dg-warning "FALSE" "" { target *-*-* } .-1 } */
+  /* { dg-warning "TRUE" "" { target *-*-* } .-2 } */
+  // TODO(xfail): ^^^ this implicitly generates control flow edges
+
+  __analyzer_eval (i || 0); /* { dg-warning "UNKNOWN" } */
+  __analyzer_eval (i || 1); /* { dg-warning "TRUE" } */
+  __analyzer_eval (i || j); /* { dg-warning "UNKNOWN" "" { xfail *-*-* } } */
+  /* { dg-warning "FALSE" "" { target *-*-* } .-1 } */
+  /* { dg-warning "TRUE" "" { target *-*-* } .-2 } */
+  // TODO(xfail): ^^^ this implicitly generates control flow edges
+
+  __analyzer_eval (~i); /* { dg-warning "UNKNOWN" } */
+  __analyzer_eval (-i); /* { dg-warning "UNKNOWN" } */
+  __analyzer_eval (+i); /* { dg-warning "UNKNOWN" } */
+
+  /* TODO:
+     - division by zero
+     - any other operators?  */
+  // etc
+
+  /* Anything added above should be added to the next function also.  */
+}
+
+/* As above, but where the values are known due to the region model,
+   but not known to GCC's regular optimizations (folding and SSA).  */
+
+void test_21 (void)
+{
+  int i, j, zero;
+  int *pi = &i;
+  int *pj = &j;
+  int *pzero = &zero;
+  *pi = 5;
+  *pj = 3;
+  *pzero = 0;
+
+  __analyzer_eval (i + j == 8); /* { dg-warning "TRUE" } */
+  __analyzer_eval (i - j == 2); /* { dg-warning "TRUE" } */
+  __analyzer_eval (i * j == 15); /* { dg-warning "TRUE" } */
+  __analyzer_eval (i / j == 1); /* { dg-warning "TRUE" } */
+  __analyzer_eval (i % j == 2); /* { dg-warning "TRUE" } */
+
+  /* Division by zero.  */
+  // TODO: should we warn for this?
+  __analyzer_eval (i / zero); /* { dg-warning "UNKNOWN" } */
+  __analyzer_eval (i % zero); /* { dg-warning "UNKNOWN" } */
+
+  __analyzer_eval ((i & 1) == (5 & 1)); /* { dg-warning "TRUE" } */
+  __analyzer_eval ((i & j) == (5 & 3)); /* { dg-warning "TRUE" } */
+  __analyzer_eval ((i | 1) == (5 | 1)); /* { dg-warning "TRUE" } */
+  __analyzer_eval ((i | j) == (5 | 3)); /* { dg-warning "TRUE" } */
+  __analyzer_eval ((i ^ 1) == (5 ^ 1)); /* { dg-warning "TRUE" } */
+  __analyzer_eval ((i ^ j) == (5 ^ 3)); /* { dg-warning "TRUE" } */
+  __analyzer_eval ((i >> 1) == (5 >> 1)); /* { dg-warning "TRUE" } */
+  __analyzer_eval ((i >> j) == (5 >> 3)); /* { dg-warning "TRUE" } */
+  __analyzer_eval ((i << 1) == (5 << 1)); /* { dg-warning "TRUE" } */
+  __analyzer_eval ((i << j) == (5 << 3)); /* { dg-warning "TRUE" } */
+  __analyzer_eval (i && 0); /* { dg-warning "FALSE" } */
+  __analyzer_eval (i && 1); /* { dg-warning "TRUE" } */
+  __analyzer_eval (i && j); /* { dg-warning "TRUE" } */
+
+  __analyzer_eval (i || 0); /* { dg-warning "TRUE" } */
+  __analyzer_eval (i || 1); /* { dg-warning "TRUE" } */
+  __analyzer_eval (i || j); /* { dg-warning "TRUE" } */
+
+  __analyzer_eval (~i == ~5); /* { dg-warning "TRUE" } */
+  __analyzer_eval (-i == -5); /* { dg-warning "TRUE" } */
+  __analyzer_eval (+i == +5); /* { dg-warning "TRUE" } */
+}
+
+void test_22 (int i, int j)
+{
+  __analyzer_eval (i + j == i + j); /* { dg-warning "TRUE" } */
+  // FIXME: this is getting folded; can we build a non-folded equivalent?
+}
+
+void test_23 (struct foo *f, struct foo *g)
+{
+  int i, j, k;
+  i = f->i + g->i;
+  j = f->i + g->i;
+  k = f->i * g->i;
+  __analyzer_eval (i == j); /* { dg-warning "TRUE" "" { xfail *-*-* } } */
+  /* { dg-warning "UNKNOWN" "" { target *-*-* } .-1 } */
+  /* TODO(xfail): we'd need to record that the two unknown values are both
+     the sum of the two unknown input values (and thus are the same); not
+     yet sure if we want arbitrary expression trees in the representation
+     (analysis termination concerns).  */
+
+  __analyzer_eval (i == k); /* { dg-warning "UNKNOWN" } */
+}
+
+void test_24 (struct foo *f)
+{
+  struct foo g;
+  g.i = 42;
+  __analyzer_eval (g.i == 42); /* { dg-warning "TRUE" } */
+
+  /* Overwriting a whole struct should invalidate our knowledge
+     about fields within it.  */
+  g = *f;
+  __analyzer_eval (g.i == 42); /* { dg-warning "UNKNOWN" "" { xfail *-*-* } } */
+  /* { dg-warning "TRUE" "" { target *-*-* } .-1 } */
+  // TODO(xfail)
+}
+
+void test_25 (struct foo *f)
+{
+  struct foo g;
+  g.i = 42;
+  f->i = 43;
+  __analyzer_eval (f->i == 43); /* { dg-warning "TRUE" } */
+  __analyzer_eval (g.i == 42); /* { dg-warning "TRUE" } */
+
+  /* Overwriting a whole struct where we know things about the
+     source value should update our knowledge about fields within
+     the dest value.  */     
+  g = *f;
+  __analyzer_eval (g.i == 43); /* { dg-warning "TRUE" "" { xfail *-*-* } } */
+  /* { dg-warning "FALSE" "" { target *-*-* } .-1 } */
+  // TODO(xfail)
+}
+
+void test_26 (struct coord *p, struct coord *q)
+{
+  p->x = 42;
+  q->y = 17;
+  __analyzer_eval (p->x == 42); /* { dg-warning "TRUE" } */
+  __analyzer_eval (p->y); /* { dg-warning "UNKNOWN" } */
+  __analyzer_eval (q->x); /* { dg-warning "UNKNOWN" } */
+  __analyzer_eval (q->y == 17); /* { dg-warning "TRUE" } */
+
+  /* Overwriting a whole struct where we know some things about the
+     source value should update our knowledge about fields within
+     the dest value.  */     
+  *p = *q;
+  __analyzer_eval (p->x); /* { dg-warning "UNKNOWN" "" { xfail *-*-* } } */
+  /* { dg-warning "TRUE" "" { target *-*-* } .-1 } */
+  // TODO(xfail): should have been overwritten
+  __analyzer_eval (p->y == 17); /* { dg-warning "TRUE" "" { xfail *-*-* } } */
+  /* { dg-warning "UNKNOWN" "" { target *-*-* } .-1 } */
+  // TODO(xfail): should have been overwritten with q->y 
+
+  __analyzer_eval (q->x); /* { dg-warning "UNKNOWN" } */
+  __analyzer_eval (q->y == 17); /* { dg-warning "TRUE" } */
+}
+
+void test_27 (struct coord *p)
+{
+  memset (p, 0, sizeof (struct coord));
+  __analyzer_eval (p->x == 0); /* { dg-warning "TRUE" "" { xfail *-*-* } } */
+  /* { dg-warning "UNKNOWN" "" { target *-*-* } .-1 } */
+  // TODO(xfail):
+  __analyzer_eval (p->y == 0); /* { dg-warning "TRUE" "" { xfail *-*-* } } */
+  /* { dg-warning "UNKNOWN" "" { target *-*-* } .-1 } */
+  // TODO(xfail):
+}
+
+void test_28 (struct coord *p)
+{
+  memset (p, 0, sizeof (struct coord) * 10);
+  __analyzer_eval (p[0].x == 0); /* { dg-warning "TRUE" "" { xfail *-*-* } } */
+  /* { dg-warning "UNKNOWN" "" { target *-*-* } .-1 } */
+  // TODO(xfail):
+  __analyzer_eval (p[0].y == 0); /* { dg-warning "TRUE" "" { xfail *-*-* } } */
+  /* { dg-warning "UNKNOWN" "" { target *-*-* } .-1 } */
+  // TODO(xfail):
+
+  __analyzer_eval (p[9].x == 0); /* { dg-warning "TRUE" "" { xfail *-*-* } } */
+  /* { dg-warning "UNKNOWN" "" { target *-*-* } .-1 } */
+  // TODO(xfail):
+  __analyzer_eval (p[9].y == 0); /* { dg-warning "TRUE" "" { xfail *-*-* } } */
+  /* { dg-warning "UNKNOWN" "" { target *-*-* } .-1 } */
+  // TODO(xfail):
+
+  __analyzer_eval (p[10].x == 0); /* { dg-warning "UNKNOWN" } */
+  __analyzer_eval (p[10].y == 0); /* { dg-warning "UNKNOWN" } */
+}
+
+void test_29 (struct coord *p)
+{
+  struct coord *q;
+
+  p[0].x = 100024;
+  p[0].y = 100025;
+
+  p[7].x = 107024;
+  p[7].y = 107025;
+
+  p[9].x = 109024;
+  p[9].y = 109025;
+
+  __analyzer_eval (p[0].x == 100024); /* { dg-warning "TRUE" } */
+  __analyzer_eval (p[0].y == 100025); /* { dg-warning "TRUE" } */
+
+  __analyzer_eval (p[7].x == 107024); /* { dg-warning "TRUE" } */
+  __analyzer_eval (p[7].y == 107025); /* { dg-warning "TRUE" } */
+
+  __analyzer_eval (p[9].x == 109024); /* { dg-warning "TRUE" } */
+  __analyzer_eval (p[9].y == 109025); /* { dg-warning "TRUE" } */
+
+  __analyzer_eval (p[10].x == 0); /* { dg-warning "UNKNOWN" } */
+  __analyzer_eval (p[10].y == 0); /* { dg-warning "UNKNOWN" } */
+
+  q = &p[7];
+
+  __analyzer_eval (q->x == 107024); /* { dg-warning "TRUE" } */
+  __analyzer_eval (q->y == 107025); /* { dg-warning "TRUE" } */
+
+  __analyzer_eval (q[2].x == 109024); /* { dg-warning "TRUE" "" { xfail *-*-* } } */
+  /* { dg-warning "UNKNOWN" "" { target *-*-* } .-1 } */
+  // TODO(xfail):
+  __analyzer_eval (q[2].y == 109025); /* { dg-warning "TRUE" "" { xfail *-*-* } } */
+  /* { dg-warning "UNKNOWN" "" { target *-*-* } .-1 } */
+  // TODO(xfail):
+
+  q += 2;
+
+  __analyzer_eval (q->x == 109024); /* { dg-warning "TRUE" "" { xfail *-*-* } } */
+  /* { dg-warning "UNKNOWN" "" { target *-*-* } .-1 } */
+  // TODO(xfail):
+  __analyzer_eval (q->y == 109025); /* { dg-warning "TRUE" "" { xfail *-*-* } } */
+  /* { dg-warning "UNKNOWN" "" { target *-*-* } .-1 } */
+  // TODO(xfail):  
+}
+
+void test_30 (void *ptr)
+{
+  struct coord *p = (struct coord *)ptr;
+  struct coord *q = (struct coord *)ptr;
+
+  p->x = 42;
+
+  __analyzer_eval (p->x == 42); /* { dg-warning "TRUE" } */
+}
+
+void test_31 (unsigned i)
+{
+  int j, k;
+
+  j = i < 100 ? i : 100; /* MIN_EXPR.  */
+  k = i < 100 ? 100 : i; /* MAX_EXPR.  */
+}
+
+enum color
+{
+  RED,
+  GREEN,
+  BLUE
+};
+
+void test_32 (enum color c)
+{
+  __analyzer_eval (c == GREEN); /* { dg-warning "UNKNOWN" } */
+
+  c = RED;
+
+  __analyzer_eval (c == RED); /* { dg-warning "TRUE" } */
+  __analyzer_eval (c == GREEN); /* { dg-warning "FALSE" } */
+}
+
+void test_33 (void)
+{
+  static int s;
+
+  __analyzer_eval (s == 42); /* { dg-warning "UNKNOWN" } */
+
+  s = 42;
+
+  __analyzer_eval (s == 42); /* { dg-warning "TRUE" } */
+}
+
+static int __attribute__((noinline))
+only_called_by_test_34 (int parm)
+{
+  __analyzer_eval (parm == 42); /* { dg-warning "TRUE" } */
+
+  return parm * 2;
+}
+
+void test_34 (void)
+{
+  int result = only_called_by_test_34 (42);
+  __analyzer_eval (result == 84); /* { dg-warning "TRUE" } */
+}
+
+void test_35 (int i, int j)
+{
+  __analyzer_eval (&i == &i); /* { dg-warning "TRUE" } */
+  __analyzer_eval (&i != &j); /* { dg-warning "TRUE" } */
+}
+
+static void __attribute__((noinline))
+write_through_ptr (int *dst, int val)
+{
+  *dst = val;
+}
+
+void test_36 (int i)
+{
+  __analyzer_eval (i == 42); /* { dg-warning "UNKNOWN" } */
+
+  write_through_ptr (&i, 42);
+
+  __analyzer_eval (i == 42); /* { dg-warning "TRUE" } */
+}
+
+// TODO: this currently crashes the analyzer
+#if 0
+int test_37 (void)
+{
+  /* Read through uninitialized pointer.  */
+  int *ptr;
+  return *ptr;
+}
+#endif
+
+// TODO: this currently crashes the analyzer
+#if 0
+int test_38 (void)
+{
+  /* Read through NULL pointer.  */
+  int *ptr = NULL;
+  return *ptr;
+}
+#endif
+
+// TODO: this currently crashes the analyzer
+#if 0
+int test_39 (void)
+{
+  /* Read through non-NULL constant pointer.  */
+  int *ptr = (int *)0x1000;
+  return *ptr;
+}
+#endif
+
+int test_40 (int flag)
+{
+  int i;
+  if (flag)
+    i = 43;
+  else
+    i = 17;
+
+  if (flag)
+    __analyzer_eval (i == 43); /* { dg-warning "TRUE" } */
+  else
+    __analyzer_eval (i == 17); /* { dg-warning "TRUE" } */
+}
+
 // TODO:
 
 struct link
@@ -285,23 +736,31 @@ union u
   int *ptr;
 };
 
-/* DONE:
+/* Coverage:
+
+   DONE (perhaps with xfail):
+   - pointers
+   - structs
+   - enums
+   - static variables
+   - interprocedural
+   - null pointer dereference
+   - constant pointer dereference (but not zero)
+   - deref of uninit pointer
 
    TODO:
+   - phi nodes
    - constraints
    - alloca
    - malloc
    - char
    - float/double
    - string constants
-   - pointers
    - arrays
    - aliasing
-   - structs
    - unions
    - bitfield operations
    - globals
-   - static variables
    - memcpy, memmove, bcopy, memccpy, meppcpy, strcpy, etc from <string.h>
    - loops
    - goto
@@ -311,8 +770,9 @@ union u
    - pointer arithmetic
    - casting from pointer to integer
    - casting from integer to pointer
+   - widening and narrowing conversions
+   - int <-> float conversions
    - other casts
    - try it on a bunch of real-world code
    - C++
-   - interprocedural
    etc.  */
-- 
1.8.5.3

