From c2fddf9628c348276c7eea1d10f03f5bddd63ffb Mon Sep 17 00:00:00 2001
From: David Malcolm <dmalcolm@redhat.com>
Date: Mon, 13 May 2019 14:18:06 -0400
Subject: [PATCH 50/67] FIXME: WIP on better memory model

---
 gcc/analyzer/Make-lang.in                          |    1 +
 gcc/analyzer/analyzer-plugin.cc                    |    1 +
 gcc/analyzer/analyzer.h                            |    1 +
 gcc/analyzer/impl-4.cc                             |   79 +-
 gcc/analyzer/region-model.cc                       | 1334 ++++++++++++++++++++
 gcc/analyzer/region-model.h                        |  294 +++++
 gcc/common.opt                                     |    4 +
 .../NOT_FOR_UPSTREAM-clang-paper-example-1.c       |   11 +
 .../NOT_FOR_UPSTREAM-clang-paper-example-2.c       |   18 +
 .../NOT_FOR_UPSTREAM-clang-paper-example-3.c       |   20 +
 .../NOT_FOR_UPSTREAM-clang-paper-example-4.c       |   14 +
 gcc/testsuite/gcc.dg/analyzer/data-model-1.c       |   38 +
 12 files changed, 1803 insertions(+), 12 deletions(-)
 create mode 100644 gcc/analyzer/region-model.cc
 create mode 100644 gcc/analyzer/region-model.h
 create mode 100644 gcc/testsuite/gcc.dg/analyzer/NOT_FOR_UPSTREAM-clang-paper-example-1.c
 create mode 100644 gcc/testsuite/gcc.dg/analyzer/NOT_FOR_UPSTREAM-clang-paper-example-2.c
 create mode 100644 gcc/testsuite/gcc.dg/analyzer/NOT_FOR_UPSTREAM-clang-paper-example-3.c
 create mode 100644 gcc/testsuite/gcc.dg/analyzer/NOT_FOR_UPSTREAM-clang-paper-example-4.c
 create mode 100644 gcc/testsuite/gcc.dg/analyzer/data-model-1.c

diff --git a/gcc/analyzer/Make-lang.in b/gcc/analyzer/Make-lang.in
index f742b9d..516e3de 100644
--- a/gcc/analyzer/Make-lang.in
+++ b/gcc/analyzer/Make-lang.in
@@ -69,6 +69,7 @@ ANALYZER_PLUGIN_SO_OBJS = \
 	analyzer/hardcoded-state-machine-taint.o \
 	analyzer/impl-3.o \
 	analyzer/impl-4.o \
+	analyzer/region-model.o \
 	analyzer/supergraph.o \
 	analyzer/tristate.o \
 
diff --git a/gcc/analyzer/analyzer-plugin.cc b/gcc/analyzer/analyzer-plugin.cc
index 17b69bd..254b589 100644
--- a/gcc/analyzer/analyzer-plugin.cc
+++ b/gcc/analyzer/analyzer-plugin.cc
@@ -41,6 +41,7 @@ analyzer_selftests (void */*gcc_data*/, void */*user_data*/)
   analyzer_constraints_cc_tests ();
   analyzer_engine_cc_tests ();
   analyzer_impl_4_cc_tests ();
+  analyzer_region_model_cc_tests ();
 }
 
 } /* end of namespace selftest.  */
diff --git a/gcc/analyzer/analyzer.h b/gcc/analyzer/analyzer.h
index 32a6ab9..7287ec4 100644
--- a/gcc/analyzer/analyzer.h
+++ b/gcc/analyzer/analyzer.h
@@ -54,6 +54,7 @@ extern void analyzer_checker_script_cc_tests ();
 extern void analyzer_constraints_cc_tests ();
 extern void analyzer_engine_cc_tests ();
 extern void analyzer_impl_4_cc_tests ();
+extern void analyzer_region_model_cc_tests ();
 
 } /* end of namespace selftest.  */
 
diff --git a/gcc/analyzer/impl-4.cc b/gcc/analyzer/impl-4.cc
index 7b30e0e..0fadd06 100644
--- a/gcc/analyzer/impl-4.cc
+++ b/gcc/analyzer/impl-4.cc
@@ -49,6 +49,7 @@
 #include "tree-ssanames.h"
 #include "tree-phinodes.h"
 #include "ssa-iterators.h"
+#include "region-model.h"
 
 /* Overview:
 
@@ -658,13 +659,13 @@ private:
    Currently this is a combination of:
    - a path_state giving a set of equivalence classes of path_vars and
      inequalities between them
+   - an optional region_model, for when -fanalyzer-region-model is enabled
    - sm_state_maps per state machine, giving a sparse mapping of
      path_vars to states.  */
 
 class program_state
 {
 public:
-  program_state (int num_checkers);
   program_state (const extrinsic_state &ext_state);
   program_state (const program_state &other);
   program_state& operator= (const program_state &other);
@@ -694,6 +695,8 @@ public:
   //private:
   path_state m_path_state;
 
+  region_model *m_region_model;
+
   auto_delete_vec<sm_state_map> m_checker_states;
 };
 
@@ -2188,18 +2191,13 @@ public:
 /* FIXME.  */
 
 program_state::program_state (const extrinsic_state &ext_state)
-: m_path_state ()
+: m_path_state (),
+  m_region_model (NULL)
 {
-  int num_states = ext_state.m_checkers.length ();
-  for (int i = 0; i < num_states; i++)
-    m_checker_states.safe_push (new sm_state_map ());
-}
+  if (flag_analyzer_region_model)
+    m_region_model = new region_model ();
 
-/* FIXME.  */
-
-program_state::program_state (int num_states)
-: m_path_state ()
-{
+  int num_states = ext_state.m_checkers.length ();
   for (int i = 0; i < num_states; i++)
     m_checker_states.safe_push (new sm_state_map ());
 }
@@ -2207,7 +2205,10 @@ program_state::program_state (int num_states)
 /* FIXME.  */
 
 program_state::program_state (const program_state &other)
-: m_path_state (other.m_path_state)
+: m_path_state (other.m_path_state),
+  m_region_model (other.m_region_model
+		  ? new region_model (*other.m_region_model)
+		  : NULL)
 {
   int i;
   sm_state_map *smap;
@@ -2222,6 +2223,12 @@ program_state::operator= (const program_state &other)
 {
   m_path_state = other.m_path_state;
 
+  delete m_region_model;
+  if (other.m_region_model)
+    m_region_model = new region_model (*other.m_region_model);
+  else
+    m_region_model = NULL;
+
   // TODO: eliminate existing things
   gcc_assert (m_checker_states.length () == 0);
 
@@ -2239,6 +2246,10 @@ hashval_t
 program_state::hash () const
 {
   hashval_t result = m_path_state.hash ();
+
+  if (m_region_model)
+    result ^= m_region_model->hash ();
+
   int i;
   sm_state_map *smap;
   FOR_EACH_VEC_ELT (m_checker_states, i, smap)
@@ -2253,6 +2264,17 @@ program_state::operator== (const program_state &other) const
 {
   if (!(m_path_state == other.m_path_state))
     return false;
+
+  if (m_region_model)
+    {
+      if (other.m_region_model == NULL)
+	return false;
+      if (!(*m_region_model == *other.m_region_model))
+	return false;
+    }
+  else if (other.m_region_model)
+    return false;
+
   int i;
   sm_state_map *smap;
   FOR_EACH_VEC_ELT (m_checker_states, i, smap)
@@ -2270,6 +2292,13 @@ program_state::print (const extrinsic_state &ext_state,
   pp_printf (pp, "ps: %s", m_path_state.to_str ().c_str ());
   pp_newline (pp);
 
+  if (m_region_model)
+    {
+      pp_printf (pp, "rmodel: ");
+      m_region_model->print (pp);
+      pp_newline (pp);
+    }
+
   int i;
   sm_state_map *smap;
   FOR_EACH_VEC_ELT (m_checker_states, i, smap)
@@ -2405,6 +2434,8 @@ void
 program_state::validate () const
 {
   m_path_state.validate ();
+  if (m_region_model)
+    m_region_model->validate ();
 }
 
 
@@ -2717,6 +2748,9 @@ exploded_node::on_assignment (const exploded_graph &eg,
 
   new_state->m_path_state.on_assignment (lhs, rhs);
 
+  if (new_state->m_region_model)
+    new_state->m_region_model->on_assignment (lhs.m_tree, rhs.m_tree);
+
   copy_sm_state (eg, lhs, rhs, old_state, new_state);
 }
 
@@ -3107,6 +3141,15 @@ program_state::on_edge (exploded_graph &eg,
       return false;
     }
 
+  if (m_region_model)
+    if (!m_region_model->apply_constraints_for_edge (*succ,
+						     last_stmt))
+      {
+	eg.log ("edge to SN: %i is impossible due to region_model constraints",
+		succ->m_dest->m_index);
+	return false;
+      }
+
   /* FIXME: the above is setting ECs for args/params on calls, but not
      updating states.  should we call on_assignment instead.
      Also, where should it happen for return values at returns?
@@ -4062,6 +4105,8 @@ 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);
 
   add_edge (m_origin, get_or_create_node (point, state), NULL);
 }
@@ -4089,6 +4134,8 @@ exploded_graph::get_or_create_node (const program_point &point,
      avoiding generating redundant nodes.  */
   program_state pruned_state = state.prune_for_point (*this, point);
 
+  pruned_state.validate ();
+
   if (get_logger ())
     log ("pruned_state: %s", pruned_state.to_str (m_ext_state).c_str ());
 
@@ -4122,6 +4169,14 @@ exploded_graph::get_or_create_node (const program_point &point,
       log ("pruned_state: %s", pruned_state.to_str (m_ext_state).c_str ());
     }
 
+  if (pruned_state.m_region_model)
+    {
+      pretty_printer pp;
+      pp_printf (&pp, "%s.EN-%i.rmodel.dot",
+		 dump_base_name, node->m_index);
+      pruned_state.m_region_model->dump_dot (pp_formatted_text (&pp));
+    }
+
   /* Add the new node to the worlist.  */
   m_worklist.safe_push (node);
   return node;
diff --git a/gcc/analyzer/region-model.cc b/gcc/analyzer/region-model.cc
new file mode 100644
index 0000000..8de5625
--- /dev/null
+++ b/gcc/analyzer/region-model.cc
@@ -0,0 +1,1334 @@
+/* FIXME.  */
+#include "config.h"
+#include "gcc-plugin.h"
+#include "system.h"
+#include "coretypes.h"
+#include "tree.h"
+#include "tm.h"
+#include "toplev.h"
+#include "hash-table.h"
+#include "vec.h"
+#include "ggc.h"
+#include "basic-block.h"
+#include "tree-ssa-alias.h"
+#include "internal-fn.h"
+#include "gimple-fold.h"
+#include "tree-eh.h"
+#include "gimple-expr.h"
+#include "is-a.h"
+#include "gimple.h"
+#include "tree-pass.h"
+#include "intl.h"
+#include "context.h"
+#include "diagnostic.h"
+#include "bitmap.h"
+#include "gimple.h"
+#include "gimple-iterator.h"
+#include "gimple-pretty-print.h"
+#include "tree-pretty-print.h"
+#include "analyzer.h"
+#include "graphviz.h"
+#include "cgraph.h"
+#include "diagnostic-path.h"
+#include "gcc-rich-location.h"
+#include "tree-dfa.h"
+#include <string>
+#include "analyzer-logging.h"
+#include "stringpool.h"
+#include "selftest.h"
+#include "fold-const.h"
+#include "tristate.h"
+#include "constraints.h"
+#include "supergraph.h"
+#include "region-model.h"
+
+void
+svalue_id::dump_node_name_to_pp (pretty_printer *pp) const
+{
+  pp_printf (pp, "svalue_%i", m_idx);
+}
+
+void
+region_id::dump_node_name_to_pp (pretty_printer *pp) const
+{
+  pp_printf (pp, "region_%i", m_idx);
+}
+
+/* class region_svalue : public svalue.  */
+
+/* FIXME.  */
+
+void
+region_svalue::dump_dot_to_pp (pretty_printer *pp) const
+{
+// TODO
+}
+
+/* class poisoned_svalue : public svalue.  */
+
+/* FIXME.  */
+
+void
+poisoned_svalue::dump_dot_to_pp (pretty_printer *pp) const
+{
+// TODO
+}
+
+/* class region.  */
+
+void
+region::dump_dot_to_pp (const region_model &model,
+			region_id this_rid,
+			pretty_printer *pp) const
+{
+  impl_dump_dot_to_pp (model, this_rid, pp);
+
+  /* Add edge to svalue.  */
+  if (!m_sval_id.null_p ())
+    {
+      this_rid.dump_node_name_to_pp (pp);
+      pp_string (pp, " -> ");
+      m_sval_id.dump_node_name_to_pp (pp);
+      pp_string (pp, ";");
+      pp_newline (pp);
+    }
+
+  /* Add edge to parent.  */
+  if (!m_parent_rid.null_p ())
+    {
+      this_rid.dump_node_name_to_pp (pp);
+      pp_string (pp, " -> ");
+      m_parent_rid.dump_node_name_to_pp (pp);
+      pp_string (pp, ";");
+      pp_newline (pp);
+  }
+}
+
+/* class map_region : public region.  */
+
+/* FIXME.  */
+
+void
+map_region::impl_dump_dot_to_pp (const region_model &model,
+				 region_id this_rid,
+				 pretty_printer *pp) const
+{
+// TODO
+  this_rid.dump_node_name_to_pp (pp);
+  pp_printf (pp, " [shape=%s,style=filled,fillcolor=%s,label=\"",
+	     "record", "lightgrey");
+  pp_left_brace (pp);
+  pp_string (pp, "map region");
+  pp_write_text_to_stream (pp);
+  pp_right_brace (pp);
+  pp_string (pp, "\"];");
+  pp_newline (pp);
+
+}
+
+/* FIXME.  */
+
+region *
+frame_region::clone () const
+{
+  return new frame_region (*this);
+}
+
+/* class stack_region : public region.  */
+
+/* FIXME.  */
+
+stack_region::stack_region (const stack_region &other)
+: region (other),
+  m_frame_rids ()
+{
+  int i;
+  region_id *frame_rid;
+  FOR_EACH_VEC_ELT (other.m_frame_rids, i, frame_rid)
+    m_frame_rids.safe_push (*frame_rid);
+}
+
+/* FIXME.  */
+
+region *
+stack_region::clone () const
+{
+  return new stack_region (*this);
+}
+
+/* FIXME.  */
+
+void
+stack_region::impl_dump_dot_to_pp (const region_model &model,
+				   region_id this_rid,
+				   pretty_printer *pp) const
+{
+  this_rid.dump_node_name_to_pp (pp);
+  pp_printf (pp, " [shape=%s,style=filled,fillcolor=%s,label=\"",
+	     "record", "lightgrey");
+  pp_left_brace (pp);
+  pp_string (pp, "stack region");
+  pp_write_text_to_stream (pp);
+  pp_right_brace (pp);
+  pp_string (pp, "\"];");
+  pp_newline (pp);
+}
+
+/* FIXME.  */
+
+void
+stack_region::push_frame (region_id frame_rid)
+{
+  m_frame_rids.safe_push (frame_rid);
+}
+
+/* class root_region : public region.  */
+
+/* FIXME.  */
+
+root_region::root_region ()
+: region (region_id::null (),
+	  svalue_id::null ())
+{
+#if 0
+  m_stack_rid (model.add_region (new stack_model ())),
+  m_globals_rid (model.add_region (new globals ())),
+#endif
+}
+
+/* FIXME.  */
+
+root_region::root_region (const root_region &other)
+: region (other),
+  m_stack_rid (other.m_stack_rid),
+  m_globals_rid (other.m_globals_rid)
+{
+}
+
+/* FIXME.  */
+
+region *
+root_region::clone () const
+{
+  return new root_region (*this);
+}
+/* FIXME.  */
+
+void
+root_region::impl_dump_dot_to_pp (const region_model &model,
+				  region_id this_rid,
+				  pretty_printer *pp) const
+{
+  this_rid.dump_node_name_to_pp (pp);
+  pp_printf (pp, " [shape=%s,style=filled,fillcolor=%s,label=\"",
+	     "record", "lightgrey");
+  pp_left_brace (pp);
+  pp_string (pp, "root region");
+  pp_write_text_to_stream (pp);
+  pp_right_brace (pp);
+  pp_string (pp, "\"];");
+  pp_newline (pp);
+
+#if 0
+  model.get_region (m_stack_rid).dump_dot_to_pp (pp);
+  m_globals.dump_dot_to_pp (pp);
+#endif
+}
+
+void
+root_region::push_frame (region_model *model, function *fun)
+{
+  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));
+    }
+  frame_region *region = new frame_region (m_stack_rid, fun);
+  region_id frame_rid = model->add_region (region);
+
+  stack_region *stack = model->get_region <stack_region> (m_stack_rid);
+  stack->push_frame (frame_rid);
+}
+
+/* class region_model.  */
+
+/* FIXME.  */
+
+region_model::region_model ()
+{
+  m_root_rid = add_region (new root_region ());
+  // TODO
+}
+
+/* FIXME.  */
+
+region_model::region_model (const region_model &other)
+: m_root_rid (other.m_root_rid)
+{
+  /* Clone the svalues and regions.  */
+  int i;
+
+  svalue *svalue;
+  FOR_EACH_VEC_ELT (other.m_svalues, i, svalue)
+    m_svalues.safe_push (svalue->clone ());
+
+  region *region;
+  FOR_EACH_VEC_ELT (other.m_regions, i, region)
+    m_regions.safe_push (region->clone ());
+}
+
+/* FIXME.  */
+
+bool
+region_model::operator== (const region_model &other) const
+{
+  // TODO
+  return true; // FIXME
+}
+
+/* FIXME.  */
+
+hashval_t
+region_model::hash () const
+{
+  // TODO
+  return 0; // FIXME
+}
+
+/* FIXME.  */
+
+void
+region_model::print (pretty_printer *pp) const
+{
+  // TODO
+}
+
+/* FIXME.  */
+
+std::string
+region_model::to_str () const
+{
+  pretty_printer pp;
+  print (&pp);
+  return pp_formatted_text (&pp);
+}
+
+/* FIXME.  */
+
+void
+region_model::dump_dot_to_pp (pretty_printer *pp) const
+{
+  graphviz_out gv (pp);
+
+  pp_string (pp, "digraph \"");
+  pp_write_text_to_stream (pp);
+  pp_write_text_as_dot_label_to_stream (pp, /*for_record=*/false);
+  pp_string (pp, "\" {\n");
+
+  gv.indent ();
+
+  pp_string (pp, "overlap=false;\n");
+  pp_string (pp, "compound=true;\n");
+
+  int i;
+  region *region;
+  FOR_EACH_VEC_ELT (m_regions, i, region)
+    region->dump_dot_to_pp (*this, region_id::from_int (i), pp);
+
+  /* Terminate "digraph" */
+  gv.outdent ();
+  pp_string (pp, "}");
+  pp_newline (pp);
+}
+
+/* FIXME.  */
+
+void
+region_model::dump_dot_to_file (FILE *fp) const
+{
+  pretty_printer pp;
+  pp.buffer->stream = fp;
+  dump_dot_to_pp (&pp);
+  pp_flush (&pp);
+}
+
+/* FIXME.  */
+
+void
+region_model::dump_dot (const char *path) const
+{
+  FILE *fp = fopen (path, "w");
+  dump_dot_to_file (fp);
+  fclose (fp);
+}
+
+/* FIXME.  */
+
+void
+region_model::validate () const
+{
+  // TODO: skip this in a release build
+}
+
+/* FIXME.  */
+
+void
+region_model::on_assignment (tree lhs, tree rhs)
+{
+}
+
+/* FIXME.  */
+
+bool
+region_model::apply_constraints_for_edge (const superedge &edge,
+					  const gimple *last_stmt)
+{
+  return true;
+}
+
+/* FIXME.  */
+
+void
+region_model::push_frame (function *fun)
+{
+  get_region<root_region> (m_root_rid)->push_frame (this, fun);
+}
+
+/* FIXME.  */
+
+svalue_id
+region_model::add_svalue (svalue *sval)
+{
+  gcc_assert (sval);
+  m_svalues.safe_push (sval);
+  return svalue_id::from_int (m_svalues.length () - 1);
+}
+
+/* FIXME.  */
+
+region_id
+region_model::add_region (region *r)
+{
+  gcc_assert (r);
+  m_regions.safe_push (r);
+  return region_id::from_int (m_regions.length () - 1);
+}
+
+/* FIXME.  */
+
+svalue *
+region_model::get_svalue (svalue_id sval_id) const
+{
+  if (sval_id.null_p ())
+    return NULL;
+  return m_svalues[sval_id.as_int ()];
+}
+
+/* FIXME.  */
+
+region *
+region_model::get_region (region_id rid) const
+{
+  if (rid.null_p ())
+    return NULL;
+  return m_regions[rid.as_int ()];
+}
+
+// FIXME:
+void
+debug (const region_model &rmodel)
+{
+  fprintf (stderr, "%s\n", rmodel.to_str ().c_str ());
+}
+
+#if CHECKING_P
+
+namespace selftest {
+
+#if 0
+
+/* Attempt to add the constraint (LHS OP RHS) to PS.
+   Verify that PS remains satisfiable.  */
+
+#define ADD_SAT_CONSTRAINT(PS, LHS, OP, RHS)				\
+  SELFTEST_BEGIN_STMT							\
+    bool sat = (PS).add_constraint (LHS, OP, RHS);			\
+    ASSERT_TRUE (sat);							\
+  SELFTEST_END_STMT
+
+/* Attempt to add the constraint (LHS OP RHS) to PS.
+   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);							\
+  SELFTEST_END_STMT
+
+static void
+assert_condition (const location &loc,
+		  path_state &ps,
+		  path_var lhs, tree_code op, path_var 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);
+  ASSERT_EQ_AT (loc, actual, expected);
+}
+
+#define ASSERT_CONDITION_TRUE(PATH_STATE, LHS, OP, RHS) \
+  SELFTEST_BEGIN_STMT							\
+  assert_condition (SELFTEST_LOCATION, PATH_STATE, LHS, OP, RHS,	\
+		    tristate (tristate::TS_TRUE));		\
+  SELFTEST_END_STMT
+
+#define ASSERT_CONDITION_FALSE(PATH_STATE, LHS, OP, RHS) \
+  SELFTEST_BEGIN_STMT							\
+  assert_condition (SELFTEST_LOCATION, PATH_STATE, LHS, OP, RHS,	\
+		    tristate (tristate::TS_FALSE));		\
+  SELFTEST_END_STMT
+
+#define ASSERT_CONDITION_UNKNOWN(PATH_STATE, LHS, OP, RHS) \
+  SELFTEST_BEGIN_STMT							\
+  assert_condition (SELFTEST_LOCATION, PATH_STATE, LHS, OP, RHS,	\
+		    tristate (tristate::TS_UNKNOWN));		\
+  SELFTEST_END_STMT
+
+/* FIXME.  */
+
+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);
+
+  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);
+
+  /* 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);
+  }
+
+  /* x == y.  */
+  {
+    path_state ps;
+    ASSERT_CONDITION_UNKNOWN (ps, x, EQ_EXPR, y);
+
+    ADD_SAT_CONSTRAINT (ps, 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);
+
+    /* 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);
+
+    /* 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);
+  }
+
+  /* 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);
+  }
+
+  /* x != y.  */
+  {
+    path_state ps;
+
+    ADD_SAT_CONSTRAINT (ps, 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);
+
+    /* 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);
+
+    /* 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);
+  }
+
+  /* x < y.  */
+  {
+    path_state ps;
+
+    ADD_SAT_CONSTRAINT (ps, 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);
+
+    /* 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);
+  }
+
+  /* x <= y.  */
+  {
+    path_state ps;
+
+    ADD_SAT_CONSTRAINT (ps, 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);
+
+    /* 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);
+  }
+
+  /* x > y.  */
+  {
+    path_state ps;
+
+    ADD_SAT_CONSTRAINT (ps, 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);
+
+    /* 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);
+  }
+
+  /* x >= y.  */
+  {
+    path_state ps;
+
+    ADD_SAT_CONSTRAINT (ps, 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);
+
+    /* 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);
+  }
+
+  // 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);
+  }
+
+  /* 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);
+  }
+
+  /* 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);
+  }
+
+  /* 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);
+  }
+
+  /* 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);
+  }
+
+  /* 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);
+  }
+
+  /* x != y && x == y.  */
+  {
+    path_state ps;
+    ADD_SAT_CONSTRAINT (ps, x, NE_EXPR, y);
+    ADD_UNSAT_CONSTRAINT (ps, 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);
+  }
+
+  // etc
+}
+
+/* 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);
+
+  path_var a (build_decl (UNKNOWN_LOCATION, PARM_DECL,
+			  get_identifier ("a"),
+			  integer_type_node), 0);
+  path_var b (build_decl (UNKNOWN_LOCATION, PARM_DECL,
+			  get_identifier ("b"),
+			  integer_type_node), 0);
+  path_var c (build_decl (UNKNOWN_LOCATION, PARM_DECL,
+			  get_identifier ("c"),
+			  integer_type_node), 0);
+  path_var d (build_decl (UNKNOWN_LOCATION, PARM_DECL,
+			  get_identifier ("d"),
+			  integer_type_node), 0);
+
+  /* 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);
+  }
+
+  /* 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);
+
+    ASSERT_CONDITION_TRUE (ps, a, LT_EXPR, c);
+    ASSERT_CONDITION_FALSE (ps, 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);
+
+    ASSERT_CONDITION_TRUE (ps, a, LT_EXPR, c);
+    ASSERT_CONDITION_FALSE (ps, 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);
+
+    ASSERT_CONDITION_TRUE (ps, a, LE_EXPR, c);
+    ASSERT_CONDITION_UNKNOWN (ps, 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);
+
+    ASSERT_CONDITION_TRUE (ps, a, GT_EXPR, c);
+    ASSERT_CONDITION_FALSE (ps, 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);
+
+    ASSERT_CONDITION_TRUE (ps, a, GT_EXPR, c);
+    ASSERT_CONDITION_FALSE (ps, 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);
+
+    ASSERT_CONDITION_TRUE (ps, a, GE_EXPR, c);
+    ASSERT_CONDITION_UNKNOWN (ps, a, EQ_EXPR, c);
+  }
+
+  /* Transitivity: "(a < b)", "(c < d)", "(b < c)" should
+     imply the easy cases:
+       (a < c)
+       (b < d)
+     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);
+  }
+
+  /* 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);
+
+    // TODO:
+    ASSERT_CONDITION_TRUE (ps, 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);
+  }
+
+  /* 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);
+
+    ASSERT_CONDITION_TRUE (ps, 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);
+  }
+
+}
+
+/* FIXME.  */
+
+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);
+
+  path_var int_1023 (build_int_cst (integer_type_node, 1023), 0);
+  path_var int_1024 (build_int_cst (integer_type_node, 1024), 0);
+
+  path_var a (build_decl (UNKNOWN_LOCATION, PARM_DECL,
+			  get_identifier ("a"),
+			  integer_type_node), 0);
+  path_var b (build_decl (UNKNOWN_LOCATION, PARM_DECL,
+			  get_identifier ("b"),
+			  integer_type_node), 0);
+
+  /* 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);
+  }
+
+  /* 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);
+  }
+
+  /* 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);
+  }
+
+  /* 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);
+  }
+
+  /* Various tests of int ranges where there is only one possible candidate.  */
+  {
+    /* 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);
+    }
+
+    /* 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);
+    }
+    /* 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);
+    }
+    /* 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);
+    }
+    /* 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);
+    }
+  }
+
+#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);
+  }
+#endif
+}
+
+/* FIXME.  */
+
+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);
+
+  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);
+
+  /* x == y.  */
+  {
+    path_state ps;
+
+    ADD_SAT_CONSTRAINT (ps, 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);
+  }
+
+  /* y <= z; x == y.  */
+  {
+    path_state ps;
+    ASSERT_CONDITION_UNKNOWN (ps, x, EQ_EXPR, y);
+    ASSERT_CONDITION_UNKNOWN (ps, 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 (ps, 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);
+
+    /* Ensure that we merged the constraints.  */
+    ASSERT_CONDITION_TRUE (ps, 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);
+
+    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 (ps, 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);
+
+    /* Ensure that we merged the constraints.  */
+    ASSERT_CONDITION_TRUE (ps, x, GE_EXPR, z);
+  }
+
+  /* x == 0, then x != 42.  */
+  {
+    path_state ps;
+
+    ADD_SAT_CONSTRAINT (ps, x, EQ_EXPR, int_0);
+    ADD_SAT_CONSTRAINT (ps, 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);
+  }
+
+  // TODO: selftest for merging ecs "in the middle"
+  // where a non-final one gets overwritten
+
+  // TODO: selftest where there are pre-existing constraints
+}
+
+/* FIXME.  */
+
+static void
+test_assignment ()
+{
+  path_var int_0 (build_int_cst (integer_type_node, 0), 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);
+  /* "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);
+}
+
+/* FIXME.  */
+
+static void
+test_stack_frames ()
+{
+  path_var int_42 (build_int_cst (integer_type_node, 42), 0);
+  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,
+			  get_identifier ("a"),
+			  integer_type_node), 0);
+  /* "x" in a child frame.  */
+  path_var x (build_decl (UNKNOWN_LOCATION, PARM_DECL,
+			  get_identifier ("x"),
+			  integer_type_node), 1);
+
+  {
+    path_state ps;
+    ps.m_stack_depth = 1;
+
+    /* x == a.  */
+    ADD_SAT_CONSTRAINT (ps, x, EQ_EXPR, a);
+    ASSERT_CONDITION_TRUE (ps, x, EQ_EXPR, a);
+
+    /* Pop the stack.  */
+    ps.pop_stack_frame ();
+    ASSERT_CONDITION_UNKNOWN (ps, x, EQ_EXPR, a);
+  }
+}
+
+/* Check that operator== and hashing works as expected for the
+   various types.  */
+
+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);
+
+  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);
+
+  {
+    path_state ps0;
+    path_state ps1;
+
+    ASSERT_EQ (ps0.hash (), ps1.hash ());
+    ASSERT_EQ (ps0, ps1);
+
+    ADD_SAT_CONSTRAINT (ps1, x, EQ_EXPR, y);
+    ASSERT_NE (ps0.hash (), ps1.hash ());
+    ASSERT_NE (ps0, ps1);
+
+    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);
+  }
+}
+
+/* A subclass of purge_criteria for selftests: purge all path_var instances.  */
+
+class purge_all_path_vars : public purge_criteria
+{
+public:
+  bool should_purge_p (path_var) const FINAL OVERRIDE
+  {
+    return true;
+  }
+};
+
+/* Check that path_state objects can "forget".  */
+
+static void
+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,
+			  get_identifier ("x"),
+			  integer_type_node), 0);
+  path_var y (build_decl (UNKNOWN_LOCATION, PARM_DECL,
+			  get_identifier ("y"),
+			  integer_type_node), 0);
+
+  {
+    path_state ps0;
+    path_state ps1;
+
+    ADD_SAT_CONSTRAINT (ps1, x, EQ_EXPR, y);
+    ASSERT_NE (ps0, ps1);
+
+    purge_one_path_var px (x);
+    ps1.purge (px);
+
+    purge_one_path_var py (y);
+    ps1.purge (py);
+
+    ASSERT_EQ (ps0, ps1);
+  }
+
+  {
+    path_state ps0;
+    path_state ps1;
+
+    ADD_SAT_CONSTRAINT (ps1, x, EQ_EXPR, int_42);
+    ASSERT_NE (ps0, ps1);
+
+    purge_one_path_var px (x);
+    ps1.purge (px);
+
+    ASSERT_EQ (ps0, ps1);
+  }
+
+  {
+    path_state ps0;
+    path_state ps1;
+
+    ADD_SAT_CONSTRAINT (ps1, x, GE_EXPR, int_0);
+    ADD_SAT_CONSTRAINT (ps1, x, LE_EXPR, int_42);
+    ASSERT_NE (ps0, ps1);
+
+    purge_one_path_var px (x);
+    ps1.purge (px);
+
+    ASSERT_EQ (ps0, ps1);
+  }
+
+  {
+    path_state ps0;
+    path_state ps1;
+
+    ADD_SAT_CONSTRAINT (ps1, x, NE_EXPR, int_42);
+    ADD_SAT_CONSTRAINT (ps1, y, NE_EXPR, int_0);
+    ASSERT_NE (ps0, ps1);
+
+    purge_one_path_var px (x);
+    ps1.purge (px);
+    ASSERT_NE (ps0, ps1);
+
+    ASSERT_CONDITION_TRUE (ps1, y, NE_EXPR, int_0);
+  }
+
+  {
+    path_state ps0;
+    path_state ps1;
+
+    ADD_SAT_CONSTRAINT (ps1, x, NE_EXPR, int_42);
+    ADD_SAT_CONSTRAINT (ps1, y, NE_EXPR, int_0);
+    ASSERT_NE (ps0, ps1);
+
+    purge_all_path_vars p;
+    ps1.purge (p);
+    ASSERT_EQ (ps0, ps1);
+  }
+
+}
+#endif
+
+
+/* Run all of the selftests within this file.  */
+
+void
+analyzer_region_model_cc_tests ()
+{
+#if 0
+  test_constraint_conditions ();
+  test_transitivity ();
+  test_constant_comparisons ();
+  test_constraint_impl ();
+  test_assignment ();
+  test_stack_frames ();
+  test_equality ();
+  test_purging ();
+#endif
+}
+
+} // namespace selftest
+
+#endif /* CHECKING_P */
diff --git a/gcc/analyzer/region-model.h b/gcc/analyzer/region-model.h
new file mode 100644
index 0000000..d6707bc
--- /dev/null
+++ b/gcc/analyzer/region-model.h
@@ -0,0 +1,294 @@
+/* FIXME.
+   Copyright (C) 2019 Free Software Foundation, Inc.
+   Contributed by David Malcolm <dmalcolm@redhat.com>.
+
+This file is part of GCC.
+
+GCC is free software; you can redistribute it and/or modify it
+under the terms of the GNU General Public License as published by
+the Free Software Foundation; either version 3, or (at your option)
+any later version.
+
+GCC is distributed in the hope that it will be useful, but
+WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
+General Public License for more details.
+
+You should have received a copy of the GNU General Public License
+along with GCC; see the file COPYING3.  If not see
+<http://www.gnu.org/licenses/>.  */
+
+#ifndef GCC_ANALYZER_REGION_MODEL_H
+#define GCC_ANALYZER_REGION_MODEL_H
+
+/* Implemention of the region-based ternary model described in:
+     "A Memory Model for Static Analysis of C Programs"
+      (Zhongxing Xu, Ted Kremenek, and Jian Zhang)
+     http://lcs.ios.ac.cn/~xuzb/canalyze/memmodel.pdf  */
+
+class superedge;
+class region;
+class region_model;
+
+/* A region_model is effectively a graph of regions and symbolic values.
+   We store per-model IDs rather than pointers to make it easier to clone
+   and to compare graphs.  */
+
+class svalue_id
+{
+public:
+  static svalue_id null () { return svalue_id (-1); }
+
+  svalue_id () : m_idx (-1) {}
+
+  bool null_p () const { return m_idx == -1; }
+
+  static svalue_id from_int (int idx) { return svalue_id (idx); }
+  int as_int () const { return m_idx; }
+
+  void dump_node_name_to_pp (pretty_printer *pp) const;
+
+private:
+  svalue_id (int idx) : m_idx (idx) {}
+
+  int m_idx;
+};
+
+class region_id
+{
+public:
+  static region_id null () { return region_id (-1); }
+
+  region_id () : m_idx (-1) {}
+
+  bool null_p () const { return m_idx == -1; }
+
+  static region_id from_int (int idx) { return region_id (idx); }
+  int as_int () const { return m_idx; }
+
+  void dump_node_name_to_pp (pretty_printer *pp) const;
+
+private:
+  region_id (int idx) : m_idx (idx) {}
+
+  int m_idx;
+};
+
+/* FIXME.  */
+
+class svalue
+{
+public:
+  virtual ~svalue () {}
+
+  virtual svalue *clone () const = 0;
+
+  virtual void dump_dot_to_pp (pretty_printer *pp) const = 0;
+
+private:
+  int m_index;
+};
+
+/* FIXME.  */
+
+class region_svalue : public svalue
+{
+public:
+  region_svalue (region_id rid) : m_rid (rid) {}
+
+  svalue *clone () const FINAL OVERRIDE
+  { return new region_svalue (m_rid); }
+
+  void dump_dot_to_pp (pretty_printer *pp) const
+    FINAL OVERRIDE;
+
+  region_id m_rid;
+};
+
+/* FIXME.  */
+
+enum poison_kind
+{
+  POISON_KIND_UNINIT,
+  POISON_KIND_FREED
+};
+
+/* FIXME.  */
+
+class poisoned_svalue : public svalue
+{
+public:
+  poisoned_svalue (enum poison_kind kind) : m_kind (kind) {}
+
+  svalue *clone () const FINAL OVERRIDE
+  { return new poisoned_svalue (m_kind); }
+
+  void dump_dot_to_pp (pretty_printer *pp) const
+    FINAL OVERRIDE;
+
+  enum poison_kind m_kind;
+};
+
+/* FIXME.  */
+
+class region
+{
+public:
+  region (region_id parent_rid, svalue_id sval_id)
+  : m_parent_rid (parent_rid), m_sval_id (sval_id) {}
+
+  region (const region &other)
+  : m_parent_rid (other.m_parent_rid), m_sval_id (other.m_sval_id)
+  {
+  }
+
+  virtual ~region () {}
+
+  virtual region *clone () const = 0;
+
+  void dump_dot_to_pp (const region_model &model,
+		       region_id this_rid,
+		       pretty_printer *pp) const;
+  virtual void impl_dump_dot_to_pp (const region_model &model,
+				    region_id this_rid,
+				    pretty_printer *pp) const = 0;
+
+public:
+  region_id m_parent_rid;
+  svalue_id m_sval_id;
+};
+
+/* FIXME.  */
+
+class map_region : public region
+{
+public:
+  map_region (region_id parent_rid)
+  : region (parent_rid, svalue_id::null ())
+  {}
+
+  map_region (const map_region &other)
+  : region (other)
+  {
+    // TODO
+  }
+
+  void impl_dump_dot_to_pp (const region_model &model,
+			    region_id this_rid,
+			    pretty_printer *pp) const
+    FINAL OVERRIDE;
+
+  // FIXME: mapping from tree to child region
+  typedef hash_map<tree, region_id> map_t;
+  map_t m_map;
+};
+
+/* FIXME.  */
+
+class frame_region : public map_region
+{
+public:
+  frame_region (region_id parent_rid, function *fun)
+  : map_region (parent_rid), m_fun (fun)
+  {}
+
+  frame_region (const frame_region &other)
+  : map_region (other), m_fun (other.m_fun)
+  {
+  }
+
+  region *clone () const FINAL OVERRIDE;
+
+  function *m_fun;
+};
+
+class stack_region : public region
+{
+public:
+  stack_region (region_id parent_rid, svalue_id sval_id)
+  : region (parent_rid, sval_id/*new poisoned_svalue (POISON_KIND_UNINIT)*/)
+  {}
+
+  stack_region (const stack_region &other);
+
+  region *clone () const FINAL OVERRIDE;
+
+  void impl_dump_dot_to_pp (const region_model &model,
+			    region_id this_rid,
+			    pretty_printer *pp) const
+    FINAL OVERRIDE;
+
+  void push_frame (region_id frame_rid);
+
+  auto_vec<region_id> m_frame_rids;
+};
+
+class root_region : public region
+{
+public:
+  root_region ();
+  root_region (const root_region &other);
+
+  region *clone () const FINAL OVERRIDE;
+
+  void impl_dump_dot_to_pp (const region_model &model,
+			    region_id this_rid,
+			    pretty_printer *pp) const
+    FINAL OVERRIDE;
+
+  void push_frame (region_model *model, function *fun);
+
+private:
+  region_id m_stack_rid;
+  region_id m_globals_rid;
+};
+
+/* FIXME.  */
+
+class region_model
+{
+ public:
+  region_model ();
+  region_model (const region_model &other);
+
+  bool operator== (const region_model &other) const;
+
+  hashval_t hash () const;
+
+  void print (pretty_printer *pp) const;
+  std::string to_str () 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;
+
+  void validate () const;
+
+  void on_assignment (tree lhs, tree rhs);
+
+  bool apply_constraints_for_edge (const superedge &edge,
+				   const gimple *last_stmt);
+
+  void push_frame (function *fun);
+
+  svalue_id add_svalue (svalue *sval);
+  region_id add_region (region *r);
+
+  svalue *get_svalue (svalue_id sval_id) const;
+  region *get_region (region_id rid) const;
+
+  template <typename Subclass>
+  Subclass *get_region (region_id rid) const
+  {
+    return (Subclass *)get_region (rid); // TODO: checking
+  }
+
+  // private:
+  auto_delete_vec<svalue> m_svalues;
+  auto_delete_vec<region> m_regions;
+  region_id m_root_rid;
+};
+
+extern void debug (const region_model &rmodel);
+
+#endif /* GCC_ANALYZER_REGION_MODEL_H */
diff --git a/gcc/common.opt b/gcc/common.opt
index 5c1e98c..0ff88fe9 100644
--- a/gcc/common.opt
+++ b/gcc/common.opt
@@ -1396,6 +1396,10 @@ fanalyzer-verbose-state-changes
 Common Var(flag_analyzer_verbose_state_changes) Init(0)
 FIXME
 
+fanalyzer-region-model
+Common Var(flag_analyzer_region_model) Init(0)
+FIXME
+
 fdump-final-insns
 Driver RejectNegative
 
diff --git a/gcc/testsuite/gcc.dg/analyzer/NOT_FOR_UPSTREAM-clang-paper-example-1.c b/gcc/testsuite/gcc.dg/analyzer/NOT_FOR_UPSTREAM-clang-paper-example-1.c
new file mode 100644
index 0000000..c5444bc
--- /dev/null
+++ b/gcc/testsuite/gcc.dg/analyzer/NOT_FOR_UPSTREAM-clang-paper-example-1.c
@@ -0,0 +1,11 @@
+void test_1 (void)
+{
+  int x, y;
+  int *p = &x;
+  x = 3;
+  *p = 4;
+  y = x;
+
+  __analyzer_eval (y == 4); /* { dg-warning "TRUE" "" { xfail *-*-* } } */
+  /* { dg-warning "UNKNOWN" "" { target *-*-* } .-1 } */  
+}
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
new file mode 100644
index 0000000..054e7da
--- /dev/null
+++ b/gcc/testsuite/gcc.dg/analyzer/NOT_FOR_UPSTREAM-clang-paper-example-2.c
@@ -0,0 +1,18 @@
+#include <stdlib.h>
+
+void test_2 (void)
+{
+  void *p = malloc (10);
+  char *buf1 = (char*)p;
+  buf1[0] = 'a'; /* { dg-warning "use of possibly-NULL 'buf1'" } */
+
+  int *buf2 = (int*)p;
+  buf2[0] = 0;
+
+  char c = buf1[0];
+
+  __analyzer_eval (c == 0); /* { dg-warning "TRUE" "" { xfail *-*-* } } */
+  /* { dg-warning "UNKNOWN" "" { target *-*-* } .-1 } */
+
+  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
new file mode 100644
index 0000000..57ed9dd
--- /dev/null
+++ b/gcc/testsuite/gcc.dg/analyzer/NOT_FOR_UPSTREAM-clang-paper-example-3.c
@@ -0,0 +1,20 @@
+#include <stdlib.h>
+
+struct s1
+{
+  int d;
+};
+struct s2
+{
+  struct s1 *p;
+};
+void test_3 (void)
+{
+  struct s1 data;
+  struct s2 *sp;
+  int a[2];
+  sp = malloc(sizeof(struct s2));
+  sp->p = &data; /* { dg-warning "use of possibly-NULL 'sp'" } */
+  sp->p->d = 3;
+  a[1] = data.d;
+} /* { dg-warning "leak of 'sp'" } */
diff --git a/gcc/testsuite/gcc.dg/analyzer/NOT_FOR_UPSTREAM-clang-paper-example-4.c b/gcc/testsuite/gcc.dg/analyzer/NOT_FOR_UPSTREAM-clang-paper-example-4.c
new file mode 100644
index 0000000..8516837
--- /dev/null
+++ b/gcc/testsuite/gcc.dg/analyzer/NOT_FOR_UPSTREAM-clang-paper-example-4.c
@@ -0,0 +1,14 @@
+#include <stddef.h>
+
+struct s { int data[2]; };
+void test_4 (struct s buf)
+{
+  int i = 3, *q = NULL;
+  struct s* p;
+  if (buf.data[1] == 1)
+    q = &i;
+  p = &buf;
+  if (p->data[1] == 1)
+    p->data[0] = *q; /* { dg-bogus "use of NULL 'q'" "" { xfail *-*-* } } */
+  return;
+}
diff --git a/gcc/testsuite/gcc.dg/analyzer/data-model-1.c b/gcc/testsuite/gcc.dg/analyzer/data-model-1.c
new file mode 100644
index 0000000..f04574b
--- /dev/null
+++ b/gcc/testsuite/gcc.dg/analyzer/data-model-1.c
@@ -0,0 +1,38 @@
+/* { dg-additional-options "-fanalyzer-region-model" } */
+
+struct foo
+{
+  int i;
+};
+
+void test_1 (void)
+{
+  struct foo f;
+  f.i = 42;
+  __analyzer_eval (f.i == 42); /* { dg-warning "TRUE" "" { xfail *-*-* } } */
+  /* { dg-warning "UNKNOWN" "" { target *-*-* } .-1 } */
+  /* TODO(xfail^^^): need to model field values.  */
+}
+
+void test_2 (struct foo *f)
+{
+  f->i = 42;
+  __analyzer_eval (f->i == 42); /* { dg-warning "TRUE" "" { xfail *-*-* } } */
+  /* { dg-warning "UNKNOWN" "" { target *-*-* } .-1 } */
+  /* TODO(xfail^^^): need to model field values.  */
+}
+
+void test_3 (void)
+{
+  int i;
+  int *p = &i;
+  i = 1;
+  *p = 2;
+  __analyzer_eval (i == 2); /* { dg-warning "TRUE" "" { xfail *-*-* } } */
+  /* { dg-warning "UNKNOWN" "" { target *-*-* } .-1 } */
+}
+
+struct link
+{
+  struct link *next;
+};
-- 
1.8.5.3

