From 6d17cfc548213dc9487fd1d309e8705081780251 Mon Sep 17 00:00:00 2001
From: David Malcolm <dmalcolm@redhat.com>
Date: Wed, 27 Mar 2019 16:18:25 -0400
Subject: [PATCH 157/161] FIXME: impl-2: WIP

FIXME: malloc-ipa-8.c: remove -fdiagnostics-path-summary-format=none; add -fdiagnostics-show-line-numbers -fdiagnostics-nn-line-numbers

FIXME: split malloc-ipa-8.c into two cases

FIXME: fix validation crashes

FIXME: implement malloc_leak::describe_final_event

FIXME: introduce pending_diagnostic::formatted_print

FIXME: use default_tree_printer when logging

FIXME: engine::prune_path: update var for phi nodes

FIXME: set up cfun/input_location

FIXME: WIP on better constraints

FIXME: recursive transitivity for constraints

FIXME: handle (a >= b) and (b >=a) implying (a == b) and similar

FIXME: handle comparisons against constants

FIXME: more test coverage

FIXME: constraints.cc to_str readability tweaks

FIXME: add comment

FIXME: partial implementation of integral ranges with just one possible element

FIXME: more on integral ranges that have just one possible element

FIXME: improve precision of "free of alloca" messages

FIXME: fix false memory leak report

FIXME: add another leak test

FIXME: consolidate leak-printing by EC

FIXME: fix constraints ICE seen with zlib

FIXME: WIP on reproducing CVE-2005-1689

FIXME: move a comment
---
 foo.sh                                             |  13 +
 gcc/analyzer/analyzer-logging.cc                   |   7 +-
 gcc/analyzer/constraints.cc                        | 605 +++++++++++++++++++--
 gcc/analyzer/constraints.h                         |  50 ++
 gcc/analyzer/engine.cc                             | 187 +++++--
 gcc/analyzer/hardcoded-state-machine-malloc.cc     |  80 ++-
 gcc/analyzer/hardcoded-state-machine.cc            |  25 +
 gcc/analyzer/hardcoded-state-machine.h             |   3 +
 gcc/analyzer/supergraph.cc                         |  20 +
 gcc/analyzer/supergraph.h                          |   2 +
 .../gcc.dg/analyzer/CVE-2005-1689-minimal.c        |  30 +
 gcc/testsuite/gcc.dg/analyzer/conditionals.c       | 121 ++++-
 gcc/testsuite/gcc.dg/analyzer/function-ptr-3.c     |  17 +
 gcc/testsuite/gcc.dg/analyzer/gzio-2.c             |  11 +
 gcc/testsuite/gcc.dg/analyzer/gzio.c               |  15 +
 gcc/testsuite/gcc.dg/analyzer/malloc-1.c           |  71 ++-
 .../gcc.dg/analyzer/malloc-ipa-8-double-free.c     | 163 ++++++
 .../gcc.dg/analyzer/malloc-ipa-8-unchecked.c       |  65 +++
 gcc/testsuite/gcc.dg/analyzer/malloc-ipa-8.c       |  70 ---
 gcc/testsuite/gcc.dg/analyzer/malloc-paths-7.c     |   2 +-
 gcc/testsuite/gcc.dg/analyzer/malloc-paths-8.c     |  18 +
 gcc/testsuite/gcc.dg/analyzer/switch.c             |   6 +-
 22 files changed, 1381 insertions(+), 200 deletions(-)
 create mode 100755 foo.sh
 create mode 100644 gcc/testsuite/gcc.dg/analyzer/CVE-2005-1689-minimal.c
 create mode 100644 gcc/testsuite/gcc.dg/analyzer/function-ptr-3.c
 create mode 100644 gcc/testsuite/gcc.dg/analyzer/gzio-2.c
 create mode 100644 gcc/testsuite/gcc.dg/analyzer/gzio.c
 create mode 100644 gcc/testsuite/gcc.dg/analyzer/malloc-ipa-8-double-free.c
 create mode 100644 gcc/testsuite/gcc.dg/analyzer/malloc-ipa-8-unchecked.c
 delete mode 100644 gcc/testsuite/gcc.dg/analyzer/malloc-ipa-8.c

diff --git a/foo.sh b/foo.sh
new file mode 100755
index 0000000..39a740a
--- /dev/null
+++ b/foo.sh
@@ -0,0 +1,13 @@
+#!/bin/bash
+
+TESTFILE=$1
+
+GCC_BUILD_DIR=~/more-coding/gcc-git-analysis-output/build/gcc
+
+#echo "TESTFILE: $TESTFILE"
+
+( $GCC_BUILD_DIR/xgcc \
+    -B $GCC_BUILD_DIR \
+    -S $TESTFILE \
+    --analyzer \
+  2>&1) | grep "internal compiler error: in operator\\[\\], at vec.h:845" || exit 1
diff --git a/gcc/analyzer/analyzer-logging.cc b/gcc/analyzer/analyzer-logging.cc
index c616ad4..179d3a3 100644
--- a/gcc/analyzer/analyzer-logging.cc
+++ b/gcc/analyzer/analyzer-logging.cc
@@ -23,6 +23,8 @@ along with GCC; see the file COPYING3.  If not see
 #include "coretypes.h"
 #include "toplev.h" /* for print_version */
 #include "pretty-print.h" /* for print_version */
+#include "diagnostic.h"
+#include "tree-diagnostic.h"
 
 #include "analyzer-logging.h"
 
@@ -44,9 +46,12 @@ logger::logger (FILE *f_out,
   pp_show_color (m_pp) = 0;
   pp_buffer (m_pp)->stream = f_out;
 
+  /* %qE in logs for SSA_NAMEs should show the ssa names, rather than
+     trying to prettify things by showing the underlying var.  */
+  pp_format_decoder (m_pp) = default_tree_printer;
+
   /* Begin the log by writing the GCC version.  */
   print_version (f_out, "", false);
-
 }
 
 /* The destructor for gcc::jit::logger, invoked via
diff --git a/gcc/analyzer/constraints.cc b/gcc/analyzer/constraints.cc
index c7a0844..1fd3792 100644
--- a/gcc/analyzer/constraints.cc
+++ b/gcc/analyzer/constraints.cc
@@ -108,7 +108,10 @@ void
 equiv_class::add (path_var v)
 {
   if (CONSTANT_CLASS_P (v.m_tree))
-    m_constant = v.m_tree;
+    {
+      gcc_assert (m_constant == NULL_TREE);
+      m_constant = v.m_tree;
+    }
   else
     {
       m_vars.safe_push (v);
@@ -171,6 +174,21 @@ equiv_class::purge_stack_frame (int callee_stack_depth)
   // FIXME: doesn't need to preserve order
 }
 
+/* Get a representative member of this class, for handling cases
+   where the IDs can change mid-traversal.  */
+
+path_var
+equiv_class::get_representative () const
+{
+  if (m_constant)
+    return path_var (m_constant, 0);
+  else
+    {
+      gcc_assert (m_vars.length () > 0);
+      return m_vars[0];
+    }
+}
+
 /* FIXME.  */
 
 const char *
@@ -186,7 +204,9 @@ constraint_op_code (enum constraint_op c_op)
     }
 }
 
-/* FIXME.  */
+/* Given "lhs C_OP rhs", determine "lhs T_OP rhs".
+
+   For example, given "x < y", then "x > y" is false.  */
 
 static tristate
 eval_constraint_op_for_op (enum constraint_op c_op, enum tree_code t_op)
@@ -224,7 +244,9 @@ constraint::to_str (const path_state &ps) const
 {
   return (m_lhs.to_str () + ": "
 	  + m_lhs.get_obj (ps).to_str ()
+	  + " "
 	  + constraint_op_code (m_op)
+	  + " "
 	  + m_rhs.to_str () + ": "
 	  + m_rhs.get_obj (ps).to_str ());
 }
@@ -285,7 +307,7 @@ path_state::to_str () const
       result += equiv_class_id (i).to_str () + ": ";
       result += ec->to_str ();
     }
-  result += "|";
+  result += "  |  ";
   constraint *c;
   FOR_EACH_VEC_ELT (m_constraints, i, c)
     {
@@ -483,7 +505,16 @@ path_state::add_constraint (path_var lhs, enum tree_code op, path_var rhs)
 {
   equiv_class_id lhs_ec_id = get_or_add_equiv_class (lhs);
   equiv_class_id rhs_ec_id = get_or_add_equiv_class (rhs);
+  return add_constraint (lhs_ec_id, op,rhs_ec_id);
+}
 
+/* FIXME.  */
+
+bool
+path_state::add_constraint (equiv_class_id lhs_ec_id,
+			    enum tree_code op,
+			    equiv_class_id rhs_ec_id)
+{
   tristate t = eval_condition (lhs_ec_id, op, rhs_ec_id);
 
   /* Discard constraints that are already known.  */
@@ -547,19 +578,19 @@ path_state::add_constraint (path_var lhs, enum tree_code op, path_var rhs)
       }
       break;
     case GE_EXPR:
-      m_constraints.safe_push (constraint (rhs_ec_id, CONSTRAINT_LE, lhs_ec_id));
+      add_constraint_internal (rhs_ec_id, CONSTRAINT_LE, lhs_ec_id);
       break;
     case LE_EXPR:
-      m_constraints.safe_push (constraint (lhs_ec_id, CONSTRAINT_LE, rhs_ec_id));
+      add_constraint_internal (lhs_ec_id, CONSTRAINT_LE, rhs_ec_id);
       break;
     case NE_EXPR:
-      m_constraints.safe_push (constraint (lhs_ec_id, CONSTRAINT_NE, rhs_ec_id));
+      add_constraint_internal (lhs_ec_id, CONSTRAINT_NE, rhs_ec_id);
       break;
     case GT_EXPR:
-      m_constraints.safe_push (constraint (rhs_ec_id, CONSTRAINT_LT, lhs_ec_id));
+      add_constraint_internal (rhs_ec_id, CONSTRAINT_LT, lhs_ec_id);
       break;
     case LT_EXPR:
-      m_constraints.safe_push (constraint (lhs_ec_id, CONSTRAINT_LT, rhs_ec_id));
+      add_constraint_internal (lhs_ec_id, CONSTRAINT_LT, rhs_ec_id);
       break;
     default:
       /* do nothing.  */
@@ -570,12 +601,215 @@ path_state::add_constraint (path_var lhs, enum tree_code op, path_var rhs)
 
 /* FIXME.  */
 
+void
+bound::ensure_closed (bool is_upper)
+{
+  if (!m_closed)
+    {
+      /* Offset by 1 in the appropriate direction.
+	 For example, convert 3 < x into 4 <= x,
+	 and convert x < 5 into x <= 4.  */
+      gcc_assert (CONSTANT_CLASS_P (m_constant));
+      m_constant = fold_build2 (is_upper ? MINUS_EXPR : PLUS_EXPR,
+				TREE_TYPE (m_constant),
+				m_constant, integer_one_node);
+      gcc_assert (CONSTANT_CLASS_P (m_constant));
+      m_closed = true;
+    }
+}
+
+/* FIXME.  */
+
+std::string
+range::to_str () const
+{
+  std::string result = expr_to_string (m_lower_bound.m_constant);
+  result += " <";
+  if (m_lower_bound.m_closed)
+    result += "=";
+  result += " x <";
+  if (m_upper_bound.m_closed)
+    result += "=";
+  result += " ";
+  result += expr_to_string (m_upper_bound.m_constant);
+  return result;  // TODO
+}
+
+/* FIXME.  */
+
+bool
+range::constrained_to_single_element (tree *out)
+{
+  if (!INTEGRAL_TYPE_P (TREE_TYPE (m_lower_bound.m_constant)))
+    return false;
+  if (!INTEGRAL_TYPE_P (TREE_TYPE (m_upper_bound.m_constant)))
+    return false;
+  // FIXME: also check the endpoint
+
+  /* Convert any open bounds to closed bounds.  */
+  m_lower_bound.ensure_closed (false);
+  m_upper_bound.ensure_closed (true);
+
+  // Are they equal?
+  tree comparison
+    = fold_build2 (EQ_EXPR, boolean_type_node,
+		   m_lower_bound.m_constant,
+		   m_upper_bound.m_constant);
+  if (comparison == boolean_true_node)
+    {
+      *out = m_lower_bound.m_constant;
+      return true;
+    }
+  else
+    return false;
+}
+
+
+/* FIXME.  */
+
+void
+path_state::add_constraint_internal (equiv_class_id lhs_id,
+				     enum constraint_op c_op,
+				     equiv_class_id rhs_id)
+{
+  /* Add the constraint.  */
+  m_constraints.safe_push (constraint (lhs_id, c_op, rhs_id));
+
+  if (c_op != CONSTRAINT_NE)
+    {
+      /* The following can potentially add EQ_EXPR facts, which could lead
+	 to ECs being merged, which would change the meaning of the EC IDs.
+	 Hence we need to do this via path vars.  */
+      path_var lhs = lhs_id.get_obj (*this).get_representative ();
+      path_var rhs = rhs_id.get_obj (*this).get_representative ();
+
+      /* We have LHS </<= RHS */
+
+      /* Handle transitivity of ordering by adding additional constraints
+	 based on what we already knew.
+
+	 So if we have already have:
+	   (a < b)
+	   (c < d)
+	 Then adding:
+	   (b < c)
+	 will also add:
+	   (a < c)
+	   (b < d)
+	 We need to recurse to ensure we also add:
+	   (a < d).
+	 We call the checked add_constraint to avoid adding constraints
+	 that are already present.  Doing so also ensures termination
+	 in the case of cycles.
+
+	 We also check for single-element ranges, adding EQ_EXPR facts
+	 where we discover them.  For example 3 < x < 5 implies
+	 that x == 4 (if x is an integer).  */
+      for (unsigned i = 0; i < m_constraints.length (); i++)
+	{
+	  const constraint *other = &m_constraints[i];
+	  if (other->is_ordering_p ())
+	    {
+	      /* Refresh the EC IDs, in case any mergers have happened.  */
+	      lhs_id = get_or_add_equiv_class (lhs);
+	      rhs_id = get_or_add_equiv_class (rhs);
+
+	      tree lhs_const = lhs_id.get_obj (*this).m_constant;
+	      tree rhs_const = rhs_id.get_obj (*this).m_constant;
+	      tree other_lhs_const
+		= other->m_lhs.get_obj (*this).m_constant;
+	      tree other_rhs_const
+		= other->m_rhs.get_obj (*this).m_constant;
+
+	      /* We have "LHS </<= RHS" and "other.lhs </<= other.rhs".  */
+
+	      /* If we have LHS </<= RHS and RHS </<= LHS, then we have a
+		 cycle.  */
+	      if (rhs_id == other->m_lhs
+		  && other->m_rhs == lhs_id)
+		{
+		  /* We must have equality for this to be possible.  */
+		  gcc_assert (c_op == CONSTRAINT_LE
+			      && other->m_op == CONSTRAINT_LE);
+		  add_constraint (lhs_id, EQ_EXPR, rhs_id);
+		  /* Adding an equality will merge the two ECs and potentially
+		     reorganize the constraints.  Stop iterating.  */
+		  return;
+		}
+	      /* Otherwise, check for transitivity.  */
+	      if (rhs_id == other->m_lhs)
+		{
+		  /* With RHS == other.lhs, we have:
+		     "LHS </<= (RHS, other.lhs) </<= other.rhs"
+		     and thus this implies "LHS </<= other.rhs".  */
+
+		  /* Do we have a tightly-constrained range?  */
+		  if (lhs_const
+		      && !rhs_const
+		      && INTEGRAL_TYPE_P (TREE_TYPE (rhs.m_tree))
+		      && other_rhs_const)
+		    {
+		      range r (bound (lhs_const, c_op == CONSTRAINT_LE),
+			       bound (other_rhs_const,
+				      other->m_op == CONSTRAINT_LE));
+		      tree constant;
+		      if (r.constrained_to_single_element (&constant))
+			{
+			  add_constraint
+			    (rhs_id, EQ_EXPR,
+			     get_or_add_equiv_class (path_var (constant, 0)));
+			  return;
+			}
+		    }
+		  /* Otherwise, add the constraint implied by transitivity.  */
+		  enum tree_code new_op
+		    = ((c_op == CONSTRAINT_LE && other->m_op == CONSTRAINT_LE)
+		       ? LE_EXPR : LT_EXPR);
+		  add_constraint (lhs_id, new_op, other->m_rhs);
+		}
+	      else if (other->m_rhs == lhs_id)
+		{
+		  /* With other.rhs == LHS, we have:
+		     "other.lhs </<= (other.rhs, LHS) </<= RHS"
+		     and thus this implies "other.lhs </<= RHS".  */
+
+		  /* Do we have a tightly-constrained range?  */
+		  if (other_lhs_const
+		      && !lhs_const
+		      && INTEGRAL_TYPE_P (TREE_TYPE (lhs.m_tree))
+		      && rhs_const)
+		    {
+		      range r (bound (other_lhs_const,
+				      other->m_op == CONSTRAINT_LE),
+			       bound (rhs_const,
+				      c_op == CONSTRAINT_LE));
+		      tree constant;
+		      if (r.constrained_to_single_element (&constant))
+			{
+			  add_constraint
+			    (lhs_id, EQ_EXPR,
+			     get_or_add_equiv_class (path_var (constant, 0)));
+			  return;
+			}
+		    }
+		  /* Otherwise, add the constraint implied by transitivity.  */
+		  enum tree_code new_op
+		    = ((c_op == CONSTRAINT_LE && other->m_op == CONSTRAINT_LE)
+		       ? LE_EXPR : LT_EXPR);
+		  add_constraint (other->m_lhs, new_op, rhs_id);
+		}
+	    }
+	}
+    }
+}
+
+/* FIXME.  */
+
 bool
 path_state::get_equiv_class (path_var pv, equiv_class_id *out) const
 {
   gcc_assert (pv.m_tree);
 
-  /* FIXME: probably should be a map, rather than these lookups.  */
   if (CONSTANT_CLASS_P (pv.m_tree))
     {
       // FIXME: we want to ensure that constants that are equal are treated as equal here
@@ -590,6 +824,7 @@ path_state::get_equiv_class (path_var pv, equiv_class_id *out) const
     }
   else
     {
+      /* FIXME: probably should be a map, rather than these lookups.  */
       int i;
       equiv_class *ec;
       FOR_EACH_VEC_ELT (m_equiv_classes, i, ec)
@@ -622,7 +857,43 @@ path_state::get_or_add_equiv_class (path_var pv)
   equiv_class *new_ec = new equiv_class ();
   new_ec->add (pv);
   m_equiv_classes.safe_push (new_ec);
-  return equiv_class_id (m_equiv_classes.length () - 1);
+
+  equiv_class_id new_id (m_equiv_classes.length () - 1);
+
+  if (CONSTANT_CLASS_P (pv.m_tree))
+    {
+      /* If we have a new EC for a constant, add constraints comparing this
+	 to other constants we may have (so that we accumulate the transitive
+	 closure of all constraints on constants as the constants are
+	 added).  */
+      for (equiv_class_id other_id (0); other_id.m_idx < new_id.m_idx;
+	   other_id.m_idx++)
+	{
+	  const equiv_class &other_ec = other_id.get_obj (*this);
+	  if (other_ec.m_constant)
+	    {
+	      /* If we have two ECs, both with constants, the constants must be
+		 non-equal (or they would be in the same EC).
+		 Determine the direction of the inequality, and record that
+		 fact.  */
+	      tree lt
+		= fold_build2 (LT_EXPR, boolean_type_node,
+			       new_ec->m_constant, other_ec.m_constant);
+	      //gcc_assert (lt == boolean_true_node || lt == boolean_false_node);
+	      // not true for int vs float comparisons
+	      if (lt == boolean_true_node)
+		add_constraint_internal (new_id, CONSTRAINT_LT, other_id);
+	      else if (lt == boolean_false_node)
+		add_constraint_internal (other_id, CONSTRAINT_LT, new_id);
+	      /* Refresh new_id, in case ECs were merged.  PV should always
+		 be present by now, so this should never lead to a
+		 recursion.  */
+	      new_id = get_or_add_equiv_class (pv);
+	    }
+	}
+    }
+
+  return new_id;
 }
 
 /* FIXME.  */
@@ -701,36 +972,75 @@ path_state::eval_condition (equiv_class_id lhs_ec,
 	}
     }
 
-#if 0
-  // TODO: what about implied orderings?
-  // transitivity:
-  // Only makes sense for inequalities
-  // e.g. x < z
-  if (op != EQ_EXPR && op != NE_EXPR)
+  return tristate (tristate::TS_UNKNOWN);
+}
+
+/* Mark EC_ID as having escaped; walk other ECs that haven't yet been marked
+   as escaped, and determine if they've now escaped, if so, mark them,
+   recursively.
+   e.g. if we know "ptr" escapes, then "ptr->foo" escapes.  */
+
+void
+path_state::recursively_mark_as_escaping (equiv_class_id ec_id)
+{
+  equiv_class &ec = ec_id.get_obj (*this);
+  if (ec.m_escaped)
     {
-      int i;
-      constraint *c;
-      FOR_EACH_VEC_ELT (m_constraints, i, c)
+      /* Nothing to do.  */
+      return;
+    }
+
+  ec.m_escaped = true;
+
+  /* Look for other ECs that haven't yet been marked as escaped.  */
+  int other_ec_idx;
+  equiv_class *other_ec;
+  FOR_EACH_VEC_ELT (m_equiv_classes, other_ec_idx, other_ec)
+    {
+      if (other_ec->m_escaped)
+	continue;
+
+      int var_idx;
+      path_var *v;
+      FOR_EACH_VEC_ELT (other_ec->m_vars, var_idx, v)
 	{
-	  /* If we have "lhs OP mid", then
-	     consider comparisons with "mid", recursively.  */
-	  // FIXME: exactly what should the ops be?
-	  if (c->m_lhs == lhs_ec)
-	    if (op == LT_EXPR && c->m_op == CONSTRAINT_LT)
-	      {
-		tristate result_for_mid
-		  = eval_condition (c->m_rhs, op, rhs_ec);
-		if (result_for_mid.is_known ())
-		  return result_for_mid;
-	      }
-	  // FIXME: this is O(N^2)
-	  // FIXME: what about the other way around?
-	  // FIXME: other ops?  etc
+	  gcc_assert (!CONSTANT_CLASS_P (v->m_tree));
+	  if (calc_escaped_p (*v))
+	    {
+	      recursively_mark_as_escaping (other_ec_idx);
+	      break;
+	    }
 	}
     }
-#endif
 
-  return tristate (tristate::TS_UNKNOWN);
+  // TODO: selftests
+  // TODO: selftest involving a cycle
+}
+
+/* Determine if PV (or something that points to it) has been marked as
+   having escaped.  */
+
+bool
+path_state::calc_escaped_p (path_var pv)
+{
+  switch (TREE_CODE (pv.m_tree))
+    {
+    case COMPONENT_REF:
+    case MEM_REF:
+      return calc_escaped_p (path_var (TREE_OPERAND (pv.m_tree, 0),
+				       pv.m_stack_depth));
+    case SSA_NAME:
+      {
+	equiv_class_id ec_id (-1);
+	if (get_equiv_class (pv, &ec_id))
+	  return ec_id.get_obj (*this).m_escaped;
+      }
+      break;
+    default:
+      return false;
+    }
+
+  return false;
 }
 
 // FIXME:
@@ -1063,7 +1373,7 @@ test_constraint_conditions ()
 /* FIXME.  */
 
 static void
-test_constraint_conditions_2 ()
+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);
@@ -1101,14 +1411,225 @@ test_constraint_conditions_2 ()
     ASSERT_CONDITION_TRUE (ps, a, EQ_EXPR, d);
   }
 
-#if 0
-  /* Transitivity: a < b, then b < c.  */
+  /* 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
 }
@@ -1190,8 +1711,11 @@ test_constraint_impl ()
     ADD_SAT_CONSTRAINT (ps, x, NE_EXPR, int_42);
 
     /* Assert various things about the insides of ps.  */
-    ASSERT_EQ (ps.m_constraints.length (), 0);
+    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"
@@ -1245,7 +1769,8 @@ void
 analyzer_constraints_cc_tests ()
 {
   test_constraint_conditions ();
-  test_constraint_conditions_2 ();
+  test_transitivity ();
+  test_constant_comparisons ();
   test_constraint_impl ();
   test_assignment ();
   test_stack_frames ();
diff --git a/gcc/analyzer/constraints.h b/gcc/analyzer/constraints.h
index 97149ba..0c2e032 100644
--- a/gcc/analyzer/constraints.h
+++ b/gcc/analyzer/constraints.h
@@ -24,6 +24,36 @@ along with GCC; see the file COPYING3.  If not see
 class superedge;
 class call_superedge;
 
+/* One of the end-points of a range.  */
+
+struct bound
+{
+  bound () : m_constant (NULL_TREE), m_closed (false) {}
+  bound (tree constant, bool closed)
+  : m_constant (constant), m_closed (closed) {}
+
+  void ensure_closed (bool is_upper);
+
+  tree m_constant;
+  bool m_closed;
+};
+
+/* FIXME.  */
+
+struct range
+{
+  range () : m_lower_bound (), m_upper_bound () {}
+  range (const bound &lower, const bound &upper)
+  : m_lower_bound (lower), m_upper_bound (upper) {}
+
+  std::string to_str () const;
+
+  bool constrained_to_single_element (tree *out);
+
+  bound m_lower_bound;
+  bound m_upper_bound;
+};
+
 /* A tree, extended with stack frame information for locals, so that
    we can distinguish between different values of locals within a potentially
    recursive callstack.  */
@@ -68,6 +98,8 @@ public:
 
   void purge_stack_frame (int callee_stack_depth);
 
+  path_var get_representative () const;
+
   /* An equivalence class can contain at most one constant.  */
   tree m_constant;
 
@@ -120,6 +152,12 @@ class constraint {
 
   std::string to_str (const path_state &ps) const;
 
+  /* Is this an ordering, rather than a "!=".  */
+  bool is_ordering_p () const
+  {
+    return m_op != CONSTRAINT_NE;
+  }
+
   equiv_class_id m_lhs;
   enum constraint_op m_op;
   equiv_class_id m_rhs;
@@ -158,6 +196,10 @@ public:
 
   bool add_constraint (path_var lhs, enum tree_code op, path_var rhs);
 
+  bool add_constraint (equiv_class_id lhs_ec_id,
+		       enum tree_code op,
+		       equiv_class_id rhs_ec_id);
+
   //private:
   bool apply_constraints_for_call (const call_superedge& edge);
 
@@ -178,9 +220,17 @@ public:
   /* For implementing "__analyzer_eval".  */
   tristate dump_condition (tree lhs, enum tree_code op, tree rhs);
 
+  void recursively_mark_as_escaping (equiv_class_id ec_id);
+  bool calc_escaped_p (path_var pv);
+
   auto_vec<equiv_class *> m_equiv_classes;
   auto_vec<constraint> m_constraints;
   int m_stack_depth;
+
+ private:
+  void add_constraint_internal (equiv_class_id lhs_id,
+				enum constraint_op c_op,
+				equiv_class_id rhs_id);
 };
 
 
diff --git a/gcc/analyzer/engine.cc b/gcc/analyzer/engine.cc
index b07d177..2ccb48d 100644
--- a/gcc/analyzer/engine.cc
+++ b/gcc/analyzer/engine.cc
@@ -576,6 +576,15 @@ public:
   {
     m_pending_diagnostic = pd;
     m_emission_id = emission_id;
+
+    /* Call get_desc now, to ensure that any side-effects take place
+       before pending_diagnostic::emit is called.
+       In particular, state_change_event::get_desc can call
+       pending_diagnostic::describe_critical_state_change;
+       free_of_non_heap can use this to tweak the message.
+       (Would be neater to simply capture this within the state).  */
+    label_text desc = get_desc ();
+    desc.maybe_free ();
   }
 
   enum event_kind m_kind;
@@ -809,6 +818,12 @@ public:
       }
   }
 
+  const cfg_superedge& get_cfg_superedge () const
+  {
+    gcc_assert (m_edge->m_kind == SUPEREDGE_CFG_EDGE);
+    return *m_edge->dyn_cast_cfg_superedge ();
+  }
+
   const call_superedge& get_call_superedge () const
   {
     gcc_assert (m_edge->m_kind != SUPEREDGE_CFG_EDGE);
@@ -1248,9 +1263,21 @@ engine::validate_sm_instance (const sm_instance &sm_inst,
 void
 engine::validate_tree (tree var, const supernode *node)
 {
-  // FIXME: this is showing up for taint-1.c; should it?
-  if (TREE_CODE (var) == ADDR_EXPR)
-    var = TREE_OPERAND (var, 0);
+  if (CONSTANT_CLASS_P (var))
+    return;
+
+  if (TREE_CODE (var) == MEM_REF)
+    {
+      validate_tree (TREE_OPERAND (var, 0), node);
+      validate_tree (TREE_OPERAND (var, 1), node);
+      return;
+    }
+  if (TREE_CODE (var) == COMPONENT_REF
+      || TREE_CODE (var) == ADDR_EXPR)
+    {
+      validate_tree (TREE_OPERAND (var, 0), node);
+      return;
+    }
 
   /* If we have an SSA_NAME for a temporary, verify that the
      def_stmt is in the same function as NODE.  */
@@ -1617,6 +1644,9 @@ engine::dfs_traverse (sm_instance sm_inst,
       log ("path_state: %s", ps.to_str ().c_str ());
     }
 
+  auto_cfun sentinel (node->m_fun);
+  input_location = node->get_start_location ();
+
   validate_sm_instance (sm_inst, node);
   validate_sm_instance (sm_inst_from_returning_call, node);
 
@@ -1665,6 +1695,7 @@ engine::dfs_traverse (sm_instance sm_inst,
   FOR_EACH_VEC_ELT (node->m_stmts, i, stmt)
     {
       sm_instance per_stmt_old_sm_inst = sm_inst;
+      input_location = stmt->location;
       on_stmt (node, stmt, &sm_inst, &per_stmt_old_sm_inst,
 	       b, &b.m_path, &ps);
     }
@@ -1777,25 +1808,13 @@ engine::on_phi (const supernode *node, const gphi *phi,
       log ("phi: %s", pp_formatted_text (&pp));
       log ("sm_inst: %s", sm_inst->to_str (m_sm).c_str ());
     }
-  
+
   gcc_assert (last_edge);
   const cfg_superedge *last_cfg_superedge = last_edge->dyn_cast_cfg_superedge ();
   gcc_assert (last_cfg_superedge);
   // FIXME: this ought to be an as_a<>
 
-  /* How to get from edge to phi arg?
-     PP shows: gimple_phi_arg_edge (phi, i)->src;
-     which is EDGE_PRED (gimple_bb (phi), i);
-     i.e. a lookup by index within bb->preds based on index within 
-     Aha:
-       gimple_phi_arg_location_from_edge (gphi *phi, edge e)
-       {
-         return gimple_phi_arg (phi, e->dest_idx)->locus;
-       }
-       which implies we can use the e->dest_idx to get at the phi arg.  */
-
-  size_t index = last_cfg_superedge->m_cfg_edge->dest_idx;
-  tree src = gimple_phi_arg_def (const_cast <gphi *> (phi), index); // FIXME const_cast
+  tree src = last_cfg_superedge->get_phi_arg (phi);
   tree lhs = gimple_phi_result (phi);
   on_assignment (node, phi, sm_inst, old_sm_inst, ps->make_path_var (lhs),
 		 ps->make_path_var (src), b, ps);
@@ -2528,6 +2547,54 @@ get_stmt_for_leak (tree var, const backtrace &b)
   return NULL;
 }
 
+/* A measurement of how good EXPR is for presenting to the user, so
+   that e.g. we can say prefer printing
+     "leak of 'tmp.m_ptr'"
+   over:
+     leak of '<unknown>'.  */
+
+static int
+readability (tree expr)
+{
+  switch (TREE_CODE (expr))
+    {
+    case COMPONENT_REF:
+    case MEM_REF:
+      return readability (TREE_OPERAND (expr, 0)) - 1;
+
+    case SSA_NAME:
+      {
+	if (tree var = SSA_NAME_VAR (expr))
+	  return readability (var);
+	return -1;
+      }
+      break;
+
+    case VAR_DECL:
+      return 256;
+
+    default:
+      return 0;
+    }
+
+  return 0;
+}
+
+/* A qsort comparator for var_state_t for use by engine::detect_leaks,
+   to sort them into most user-readable to least user-readable.  */
+
+static int
+leak_comparator (const void *p1, const void *p2)
+{
+  const var_state_t *vs1 = (const var_state_t *)p1;
+  const var_state_t *vs2 = (const var_state_t *)p2;
+
+  int r1 = readability (vs1->m_var);
+  int r2 = readability (vs2->m_var);
+
+  return r2 - r1;
+}
+
 /* FIXME.  */
 
 void
@@ -2549,13 +2616,18 @@ engine::detect_leaks (const supernode *node, const sm_instance &sm_inst,
     tree result = DECL_RESULT (node->m_fun->decl);
     if (result)
       {
+	log ("new_ps before escapes: %s", new_ps.to_str ().c_str ());
 	// FIXME: stack depth:
-	equiv_class_id ec_id = new_ps.get_or_add_equiv_class (path_var (result, 0));
-	equiv_class &ec = ec_id.get_obj (new_ps);
-	ec.m_escaped = true;
+	equiv_class_id ec_id
+	  = new_ps.get_or_add_equiv_class (path_var (result, 0));
+	new_ps.recursively_mark_as_escaping (ec_id);
+	log ("new_ps after escapes: %s", new_ps.to_str ().c_str ());
       }
   }
 
+  /* Gather all leaks into a vec so we can sort them.   */
+  auto_vec<var_state_t> leaks;
+
   for (hash_set<var_state_t>::iterator iter
 	 = sm_inst.m_active_vars.m_set.begin ();
        iter != sm_inst.m_active_vars.m_set.end ();
@@ -2566,10 +2638,25 @@ engine::detect_leaks (const supernode *node, const sm_instance &sm_inst,
       if (get_logger ())
 	log ("considering %s", (*iter).to_str (m_sm).c_str ());
 
-      /* Did this var's equivalence class escape?  If so, don't complain
+     leaks.safe_push (*iter);
+    }
+
+  /* Sort the leaks into most human-readable first, through
+     to least user-readable.  Given that we only emit one
+     leak per EC, this ought to ensure that we pick the most
+     user-readable description of each leaking EC.  */
+  leaks.qsort (leak_comparator);
+
+  /* Iterate through the sorted leaks, potentially emitting them.  */
+  int i;
+  var_state_t *vs;
+  FOR_EACH_VEC_ELT (leaks, i, vs)
+    {
+       /* Did this var's equivalence class escape?  If so, don't complain
 	 about it leaking.  */
       // FIXME: stack depth:
-      equiv_class_id ec_id = new_ps.get_or_add_equiv_class (path_var ((*iter).m_var, 0));
+      equiv_class_id ec_id
+	= new_ps.get_or_add_equiv_class (path_var (vs->m_var, 0));
       equiv_class &ec = ec_id.get_obj (new_ps);
       if (get_logger ())
 	log ("within %s", ec.to_str ().c_str ());
@@ -2587,7 +2674,7 @@ engine::detect_leaks (const supernode *node, const sm_instance &sm_inst,
 	}
 
       // TODO: determine most appropriate stmt
-      const gimple *stmt = get_stmt_for_leak ((*iter).m_var, b);
+      const gimple *stmt = get_stmt_for_leak (vs->m_var, b);
 
       // FIXME: various redundant copies here:
       checker_path p (b.m_path);
@@ -2596,7 +2683,11 @@ engine::detect_leaks (const supernode *node, const sm_instance &sm_inst,
 			      &new_sm_inst,
 			      &sm_inst,
 			      &p, &new_ps);
-      m_sm.on_leak (&ctxt, node, stmt, (*iter).m_var, (*iter).m_state);
+      m_sm.on_leak (&ctxt, node, stmt, vs->m_var, vs->m_state);
+
+      /* Mark this EC as having escaped, to suppress further leak warnings
+	 from it.  */
+      ec.m_escaped = true;
     }
 }
 
@@ -3151,16 +3242,44 @@ engine::prune_path (checker_path *path,
 	    switch (event->m_edge->m_kind)
 	      {
 	      case SUPEREDGE_CFG_EDGE:
-		/* TODO: is this edge significant to var?
-		   See if var can be in other states in the dest, but not
-		   in other states in the src?
-		   Must have multiple sibling edges.  */
-		// TODO: for now, filter all intraprocedural edges:
-		if (m_verbosity < 2)
-		  {
-		    log ("filtering event %i: CFG edge", idx);
-		    path->delete_event (idx);
-		  }
+		{
+		  const cfg_superedge& cfg_superedge
+		    = event->get_cfg_superedge ();
+		  const supernode *dest = event->m_edge->m_dest;
+		  /* Do we have an SSA_NAME defined via a phi node in
+		     the dest CFG node?  */
+		  if (TREE_CODE (var) == SSA_NAME)
+		    if (SSA_NAME_DEF_STMT (var)->bb == dest->m_bb)
+		      {
+			if (const gphi *phi
+			    = dyn_cast <gphi *> (SSA_NAME_DEF_STMT (var)))
+			  {
+			    /* Update var based on its phi node.  */
+			    tree old_var = var;
+			    var = cfg_superedge.get_phi_arg (phi);
+			    log ("updating from %qE to %qE based on phi node",
+				 old_var, var);
+			    if (get_logger ())
+			      {
+				pretty_printer pp;
+				pp_gimple_stmt_1 (&pp, (gimple *)phi, 0, (dump_flags_t)0);
+				// FIXME: const_cast!
+				log ("  phi: %s", pp_formatted_text (&pp));
+			      }
+			  }
+		      }
+
+		  /* TODO: is this edge significant to var?
+		     See if var can be in other states in the dest, but not
+		     in other states in the src?
+		     Must have multiple sibling edges.  */
+		  // TODO: for now, filter all intraprocedural edges:
+		  if (m_verbosity < 2)
+		    {
+		      log ("filtering event %i: CFG edge", idx);
+		      path->delete_event (idx);
+		    }
+		}
 		break;
 
 	      case SUPEREDGE_CALL:
diff --git a/gcc/analyzer/hardcoded-state-machine-malloc.cc b/gcc/analyzer/hardcoded-state-machine-malloc.cc
index cdc7307..cf61b0d 100644
--- a/gcc/analyzer/hardcoded-state-machine-malloc.cc
+++ b/gcc/analyzer/hardcoded-state-machine-malloc.cc
@@ -91,11 +91,8 @@ public:
   {
     if (new_state == m_sm.m_free)
       {
-	pretty_printer pp;
-	pp_printf (&pp, "first %qs here", "free");
 	m_first_free_event = event_id;
-	return label_text::take (xstrdup (pp_formatted_text (&pp)));
-	// TODO: using appropriate colorization etc
+	return formatted_print ("first %qs here", "free");
       }
     return label_text ();
   }
@@ -106,10 +103,7 @@ public:
      tree expr ATTRIBUTE_UNUSED,
      state_machine::state_t state ATTRIBUTE_UNUSED)
   {
-    pretty_printer pp;
-    pp_printf (&pp, "second %qs here", "free");
-    return label_text::take (xstrdup (pp_formatted_text (&pp)));
-    // TODO: using appropriate colorization etc
+    return formatted_print ("second %qs here", "free");
   }
 
   /* FIXME: maybe also something like this.  */
@@ -157,10 +151,7 @@ public:
      tree expr,
      state_machine::state_t state ATTRIBUTE_UNUSED)
   {
-    pretty_printer *pp = global_dc->printer;
-    pp_printf (pp, "%qE could be NULL", expr);
-    return label_text::take (xstrdup (pp_formatted_text (pp)));
-    // FIXME: warning due to use of 'E' format code; move to a support function?
+    return formatted_print ("%qE could be NULL", expr);
   }
 
 };
@@ -230,23 +221,47 @@ public:
       return label_text::borrow ("allocated here");
     return label_text ();
   }
+
+  /* FIXME.  */
+  label_text describe_final_event
+    (/*diagnostic_context *ctxt, */
+     tree expr ATTRIBUTE_UNUSED,
+     state_machine::state_t state ATTRIBUTE_UNUSED)
+  {
+    return formatted_print ("%qE leaks here", expr);
+  }
+
 };
 
 class free_of_non_heap : public malloc_diagnostic
 {
 public:
   free_of_non_heap (const malloc_state_machine &sm, tree arg)
-  : malloc_diagnostic (sm, arg)
-  {}
+  : malloc_diagnostic (sm, arg), m_kind (KIND_UNKNOWN)
+  {
+  }
 
   void emit (rich_location *rich_loc) FINAL OVERRIDE
   {
     auto_diagnostic_group d;
     metadata m;
     m.add_cwe (590); /* CWE-590: Free of Memory not on the Heap.  */
-    warning_at (rich_loc, m,
-		"free of %qE which points to memory not on the heap", m_arg);
-    // FIXME: ideally would distinguish the cases in the error message
+    switch (m_kind)
+      {
+      default:
+	gcc_unreachable ();
+      case KIND_UNKNOWN:
+	warning_at (rich_loc, m,
+		    "free of %qE which points to memory not on the heap",
+		    m_arg);
+	break;
+      case KIND_ALLOCA:
+	warning_at (rich_loc, m,
+		    "free of memory allocated on the stack by %qs (%qE)"
+		    " will corrupt the heap",
+		    "alloca", m_arg);
+	break;
+      }
   }
 
   label_text describe_critical_state_change
@@ -256,7 +271,23 @@ public:
      event_id_t event_id)
     FINAL OVERRIDE
   {
-    return label_text::borrow ("pointer is from here"); // TODO
+    /* Attempt to reconstruct what kind of pointer it is.
+       (It seems neater for this to be a part of the state, though).  */
+    if (TREE_CODE (expr) == SSA_NAME)
+      {
+	gimple *def_stmt = SSA_NAME_DEF_STMT (expr);
+	if (gcall *call = dyn_cast <gcall *> (def_stmt))
+	  {
+	    if (is_named_call_p (call, "alloca", 1)
+		|| is_named_call_p (call, "__builtin_alloca", 1))
+	      {
+		m_kind = KIND_ALLOCA;
+		return label_text::borrow
+		  ("memory is allocated on the stack here");
+	      }
+	  }
+      }
+    return label_text::borrow ("pointer is from here");
   }
 
   /* FIXME.  */
@@ -265,11 +296,16 @@ public:
      tree expr ATTRIBUTE_UNUSED,
      state_machine::state_t state ATTRIBUTE_UNUSED)
   {
-    pretty_printer pp;
-    pp_printf (&pp, "call to %qs here", "free");
-    return label_text::take (xstrdup (pp_formatted_text (&pp)));
-    // TODO: using appropriate colorization etc
+    return formatted_print ("call to %qs here", "free");
   }
+
+private:
+  enum kind
+  {
+    KIND_UNKNOWN,
+    KIND_ALLOCA
+  };
+  enum kind m_kind;
 };
 
 ////////////////////////////////////////////////////////////////////////////
diff --git a/gcc/analyzer/hardcoded-state-machine.cc b/gcc/analyzer/hardcoded-state-machine.cc
index fcfb6d7..fa69b6c 100644
--- a/gcc/analyzer/hardcoded-state-machine.cc
+++ b/gcc/analyzer/hardcoded-state-machine.cc
@@ -110,6 +110,31 @@ state_machine::get_state_name (state_t s) const
 
 ////////////////////////////////////////////////////////////////////////////
 
+label_text
+pending_diagnostic::formatted_print (const char *fmt, ...)
+{
+  pretty_printer *pp = global_dc->printer->clone ();
+
+  text_info ti;
+  rich_location rich_loc (line_table, UNKNOWN_LOCATION);
+  va_list ap;
+  va_start (ap, fmt);
+  ti.format_spec = _(fmt);
+  ti.args_ptr = &ap;
+  ti.err_no = 0;
+  ti.x_data = NULL;
+  ti.m_richloc = &rich_loc;
+  pp_format (pp, &ti);
+  pp_output_formatted_text (pp);
+  va_end (ap);
+
+  label_text result = label_text::take (xstrdup (pp_formatted_text (pp)));
+  delete pp;
+  return result;
+}
+
+////////////////////////////////////////////////////////////////////////////
+
 void
 make_checkers (auto_delete_vec <state_machine> &out, logger *logger)
 {
diff --git a/gcc/analyzer/hardcoded-state-machine.h b/gcc/analyzer/hardcoded-state-machine.h
index f9b9c9d..bdc79e0 100644
--- a/gcc/analyzer/hardcoded-state-machine.h
+++ b/gcc/analyzer/hardcoded-state-machine.h
@@ -163,6 +163,9 @@ class pending_diagnostic
     /* Default no-op implementation.  */
     return label_text ();
   }
+
+  static label_text formatted_print (const char *fmt, ...)
+    ATTRIBUTE_GCC_DIAG(1,2);
 };
 
 #if 0
diff --git a/gcc/analyzer/supergraph.cc b/gcc/analyzer/supergraph.cc
index 1596c7c..860d704 100644
--- a/gcc/analyzer/supergraph.cc
+++ b/gcc/analyzer/supergraph.cc
@@ -694,6 +694,26 @@ cfg_superedge::dump_label_to_pp (pretty_printer *pp) const
 
 /* FIXME.  */
 
+tree
+cfg_superedge::get_phi_arg (const gphi *phi) const
+{
+  /* How to get from edge to phi arg?
+     PP shows: gimple_phi_arg_edge (phi, i)->src;
+     which is EDGE_PRED (gimple_bb (phi), i);
+     i.e. a lookup by index within bb->preds based on index within
+     Aha:
+       gimple_phi_arg_location_from_edge (gphi *phi, edge e)
+       {
+         return gimple_phi_arg (phi, e->dest_idx)->locus;
+       }
+       which implies we can use the e->dest_idx to get at the phi arg.  */
+
+  size_t index = m_cfg_edge->dest_idx;
+  return gimple_phi_arg_def (const_cast <gphi *> (phi), index); // FIXME const_cast
+}
+
+/* FIXME.  */
+
 void
 switch_cfg_superedge::dump_label_to_pp (pretty_printer *pp) const
 {
diff --git a/gcc/analyzer/supergraph.h b/gcc/analyzer/supergraph.h
index 782543a..c68411f 100644
--- a/gcc/analyzer/supergraph.h
+++ b/gcc/analyzer/supergraph.h
@@ -300,6 +300,8 @@ class cfg_superedge : public superedge
   int true_value_p () const { return get_flags () & EDGE_TRUE_VALUE; }
   int false_value_p () const { return get_flags () & EDGE_FALSE_VALUE; }
 
+  tree get_phi_arg (const gphi *phi) const;
+
   ::edge m_cfg_edge;
 };
 
diff --git a/gcc/testsuite/gcc.dg/analyzer/CVE-2005-1689-minimal.c b/gcc/testsuite/gcc.dg/analyzer/CVE-2005-1689-minimal.c
new file mode 100644
index 0000000..f19f5a7
--- /dev/null
+++ b/gcc/testsuite/gcc.dg/analyzer/CVE-2005-1689-minimal.c
@@ -0,0 +1,30 @@
+#include <stdlib.h>
+
+typedef struct _krb5_data {
+  char *data;
+} krb5_data;
+
+void
+test_1 (krb5_data inbuf, int flag)
+{
+  free(inbuf.data);
+  free(inbuf.data); // FIXME: double-free here
+}
+
+void
+test_2 (krb5_data inbuf, int flag)
+{
+  if (flag) {
+    free(inbuf.data);
+  }
+  free(inbuf.data); // FIXME: double-free here
+}
+
+void
+test_3 (krb5_data inbuf, int flag)
+{
+  if (flag) {
+    free((char *)inbuf.data);
+  }
+  free((char *)inbuf.data); // FIXME: double-free here
+}
diff --git a/gcc/testsuite/gcc.dg/analyzer/conditionals.c b/gcc/testsuite/gcc.dg/analyzer/conditionals.c
index ffaf9bc..578a9b8 100644
--- a/gcc/testsuite/gcc.dg/analyzer/conditionals.c
+++ b/gcc/testsuite/gcc.dg/analyzer/conditionals.c
@@ -1,18 +1,15 @@
-void test (int i)
+void test (int i, int j)
 {
   if (i > 4)
     {
       __analyzer_eval (i > 4); /* { dg-warning "TRUE" } */
       __analyzer_eval (i <= 4); /* { dg-warning "FALSE" } */
-      __analyzer_eval (i > 3); /* { dg-warning "TRUE" "" { xfail *-*-* } } */
-      /* { dg-warning "UNKNOWN" "" { target *-*-* } .-1 } */
+      __analyzer_eval (i > 3); /* { dg-warning "TRUE" } */
 
       __analyzer_eval (i > 5); /* { dg-warning "UNKNOWN" } */
-      __analyzer_eval (i != 3); /* { dg-warning "TRUE" "" { xfail *-*-* } } */
-      /* { dg-warning "UNKNOWN" "" { target *-*-* } .-1 } */
+      __analyzer_eval (i != 3); /* { dg-warning "TRUE" } */
 
-      __analyzer_eval (i == 3); /* { dg-warning "FALSE" "" { xfail *-*-* } } */
-      /* { dg-warning "UNKNOWN" "" { target *-*-* } .-1 } */
+      __analyzer_eval (i == 3); /* { dg-warning "FALSE" } */
 
       __analyzer_eval (i != 4); /* { dg-warning "TRUE" } */
       __analyzer_eval (i == 4); /* { dg-warning "FALSE" } */
@@ -20,32 +17,108 @@ void test (int i)
       __analyzer_eval (i != 5); /* { dg-warning "UNKNOWN" } */
       __analyzer_eval (i < 5); /* { dg-warning "FALSE" } */
       __analyzer_eval (i <= 5); /* { dg-warning "UNKNOWN" } */
+
+      /* Tests of transitivity.  */
+      if (j < i)
+	{
+	  __analyzer_eval (j < i); /* { dg-warning "TRUE" } */
+	  __analyzer_eval (j <= 4); /* { dg-warning "UNKNOWN" } */
+	}
+      else
+	{
+	  __analyzer_eval (j >= i); /* { dg-warning "TRUE" } */
+	  __analyzer_eval (j > 4); /* { dg-warning "TRUE" } */
+	}
     }
   else
     {
       __analyzer_eval (i > 4); /* { dg-warning "FALSE" } */
       __analyzer_eval (i <= 4); /* { dg-warning "TRUE" } */
-      __analyzer_eval (i > 3); /* { dg-warning "FALSE" "" { xfail *-*-* } } */
-      /* { dg-warning "UNKNOWN" "" { target *-*-* } .-1 } */
-
-      __analyzer_eval (i > 5); /* { dg-warning "UNKNOWN" } */
-      __analyzer_eval (i != 3); /* { dg-warning "FALSE" "" { xfail *-*-* } } */
-      /* { dg-warning "UNKNOWN" "" { target *-*-* } .-1 } */
+      __analyzer_eval (i > 3); /* { dg-warning "UNKNOWN" } */
 
-      __analyzer_eval (i == 3); /* { dg-warning "TRUE" "" { xfail *-*-* } } */
-      /* { dg-warning "UNKNOWN" "" { target *-*-* } .-1 } */
+      __analyzer_eval (i > 5); /* { dg-warning "FALSE" } */
+      __analyzer_eval (i != 3); /* { dg-warning "UNKNOWN" } */
 
-      __analyzer_eval (i != 4); /* { dg-warning "FALSE" "" { xfail *-*-* } } */
-      /* { dg-warning "UNKNOWN" "" { target *-*-* } .-1 } */
+      __analyzer_eval (i == 3); /* { dg-warning "UNKNOWN" } */
 
-      __analyzer_eval (i == 4); /* { dg-warning "TRUE" "" { xfail *-*-* } } */
-      /* { dg-warning "UNKNOWN" "" { target *-*-* } .-1 } */
-
-      __analyzer_eval (i == 5); /* { dg-warning "UNKNOWN" } */
-      __analyzer_eval (i != 5); /* { dg-warning "UNKNOWN" } */
+      __analyzer_eval (i != 4); /* { dg-warning "UNKNOWN" } */
+      __analyzer_eval (i == 4); /* { dg-warning "UNKNOWN" } */
+      __analyzer_eval (i == 5); /* { dg-warning "FALSE" } */
+      __analyzer_eval (i != 5); /* { dg-warning "TRUE" } */
       __analyzer_eval (i < 5); /* { dg-warning "TRUE" } */
-      __analyzer_eval (i <= 5); /* { dg-warning "UNKNOWN" } */
+      __analyzer_eval (i <= 5); /* { dg-warning "TRUE" } */
+    }
+}
+
+void test_2 (int i, int j, int k)
+{
+  if (i >= j)
+    {
+      __analyzer_eval (i == k); /* { dg-warning "UNKNOWN" } */
+      if (j >= k)
+	{
+	  __analyzer_eval (i >= k); /* { dg-warning "TRUE" } */
+	  __analyzer_eval (i == k); /* { dg-warning "UNKNOWN" } */
+	  if (k >= i)
+	    __analyzer_eval (i == k); /* { dg-warning "TRUE" } */
+	}
     }
 }
 
-/* TODO: The various xfails here involve implications of conditionals.  */
+void test_range_int_gt_lt (int i)
+{
+  if (i > 3)
+    if (i < 5)
+      __analyzer_eval (i == 4); /* { dg-warning "TRUE" } */
+}
+
+void test_range_float_gt_lt (float f)
+{
+  if (f > 3)
+    if (f < 5)
+      __analyzer_eval (f == 4); /* { dg-warning "UNKNOWN" } */
+}
+
+void test_range_int_ge_lt (int i)
+{
+  if (i >= 4)
+    if (i < 5)
+      __analyzer_eval (i == 4); /* { dg-warning "TRUE" } */
+}
+
+void test_range_float_ge_lt (float f)
+{
+  if (f >= 4)
+    if (f < 5)
+      __analyzer_eval (f == 4); /* { dg-warning "UNKNOWN" } */
+}
+
+void test_range_int_gt_le (int i)
+{
+  if (i > 3)
+    if (i <= 4)
+      __analyzer_eval (i == 4); /* { dg-warning "TRUE" } */
+}
+
+void test_range_float_gt_le (float f)
+{
+  if (f > 3)
+    if (f <= 4)
+      __analyzer_eval (f == 4); /* { dg-warning "UNKNOWN" "" { xfail *-*-* } } */
+      /* { dg-warning "FALSE" "" { target *-*-* } .-1 } */
+}
+
+void test_range_int_ge_le (int i)
+{
+  if (i >= 4)
+    if (i <= 4)
+      __analyzer_eval (i == 4); /* { dg-warning "TRUE" } */
+}
+
+void test_range_float_ge_le (float f)
+{
+  if (f >= 4)
+    if (f <= 4)
+      __analyzer_eval (f == 4); /* { dg-warning "TRUE" "" { xfail *-*-* } } */
+      /* { dg-warning "FALSE" "" { target *-*-* } .-1 } */
+}
diff --git a/gcc/testsuite/gcc.dg/analyzer/function-ptr-3.c b/gcc/testsuite/gcc.dg/analyzer/function-ptr-3.c
new file mode 100644
index 0000000..348ee4a
--- /dev/null
+++ b/gcc/testsuite/gcc.dg/analyzer/function-ptr-3.c
@@ -0,0 +1,17 @@
+#include <stdlib.h>
+
+typedef void *(*alloc_func_t) (size_t);
+typedef void (*free_func_t) (void *);
+
+typedef struct callbacks
+{
+  alloc_func_t alloc_cb;
+  free_func_t dealloc_cb;
+} callbacks_t;
+
+void test (void)
+{
+  callbacks_t cb;
+  cb.alloc_cb = (alloc_func_t)0;
+  cb.dealloc_cb = (free_func_t)0;
+}
diff --git a/gcc/testsuite/gcc.dg/analyzer/gzio-2.c b/gcc/testsuite/gcc.dg/analyzer/gzio-2.c
new file mode 100644
index 0000000..855ecc8
--- /dev/null
+++ b/gcc/testsuite/gcc.dg/analyzer/gzio-2.c
@@ -0,0 +1,11 @@
+void gzseek (long offset, int whence)
+{
+  if (whence == 2)
+    return;
+  if (whence == 0)
+    offset -= 1;
+  if (offset < 0)
+    return;
+  while (offset > 0) {
+  }
+}
diff --git a/gcc/testsuite/gcc.dg/analyzer/gzio.c b/gcc/testsuite/gcc.dg/analyzer/gzio.c
new file mode 100644
index 0000000..3a036d1
--- /dev/null
+++ b/gcc/testsuite/gcc.dg/analyzer/gzio.c
@@ -0,0 +1,15 @@
+#include <stdlib.h>
+typedef struct z_stream_s {
+  unsigned char *next_out;
+} z_stream;
+typedef struct gz_stream {
+  z_stream stream;
+  unsigned char *outbuf;
+} gz_stream;
+gz_stream *s;
+static void gz_open(const char *path)
+{
+  s->stream.next_out = s->outbuf = (unsigned char *)malloc(16384);
+}
+void gzopen(const char *path)
+{ return gz_open(path); }
diff --git a/gcc/testsuite/gcc.dg/analyzer/malloc-1.c b/gcc/testsuite/gcc.dg/analyzer/malloc-1.c
index 5914d65..128dfe9 100644
--- a/gcc/testsuite/gcc.dg/analyzer/malloc-1.c
+++ b/gcc/testsuite/gcc.dg/analyzer/malloc-1.c
@@ -253,9 +253,8 @@ int *test_23 (int n)
 
 int test_24 (void)
 {
-  void *ptr = alloca (sizeof (int)); /* { dg-message "pointer is from here" } */
-  free (ptr); /* { dg-warning "free of 'ptr' which points to memory not on the heap \\\[CWE-590\\\]" } */
-  /* TODO: more precise messages here.  */
+  void *ptr = alloca (sizeof (int)); /* { dg-message "memory is allocated on the stack here" } */
+  free (ptr); /* { dg-warning "free of memory allocated on the stack by 'alloca' \\('ptr'\\) will corrupt the heap \\\[CWE-590\\\]" } */
 }
 
 int test_25 (void)
@@ -301,3 +300,69 @@ struct coord *test_28 (void)
 
   return p;
 }
+
+struct link
+{
+  struct link *m_ptr;
+};
+
+struct link *test_29 (void)
+{
+  struct link *res = (struct link *)malloc (sizeof (struct link));
+  if (!res)
+    return NULL;
+  res->m_ptr = (struct link *)malloc (sizeof (struct link));
+  return res;
+}
+
+#if 0
+/* FIXME: this is showing a leak.  */
+struct link *test_30 (void)
+{
+  struct link *res = (struct link *)malloc (sizeof (struct link));
+  if (!res)
+    return NULL;
+  res->m_ptr = (struct link *)malloc (sizeof (struct link));
+  if (!res->m_ptr)
+    {
+      free (res);
+      return NULL;
+    }
+  res->m_ptr->m_ptr = (struct link *)malloc (sizeof (struct link));
+  return res;
+}
+#endif
+
+/* Without consolidation by EC, this one used to show two leaks:
+     warning: leak of '<unknown>'
+     warning: leak of 'tmp.m_ptr' 
+   We should only show the latter (favoring the most user-readable
+   expression in the equivalence class).  */
+void test_30 (void)
+{
+  struct link tmp;
+  tmp.m_ptr = (struct link *)malloc (sizeof (struct link));
+} /* { dg-warning "leak of 'tmp.m_ptr'" } */ 
+
+void test_31 (void)
+{
+  struct link tmp;
+  void *ptr = malloc (sizeof (struct link));
+  tmp.m_ptr = (struct link *)ptr;
+} /* { dg-warning "leak of 'ptr'" } */ 
+
+#if 0
+void test_31 (void *p)
+{
+  void *q = realloc (p, 1024);
+  free (p); /* FIXME: this is a double-free.  */
+  free (q);
+}
+
+void test_32 (void)
+{
+  void *p = malloc (64);
+  p = realloc (p, 1024); /* FIXME: this leaks if it fails.  */
+  free (p);
+}
+#endif
diff --git a/gcc/testsuite/gcc.dg/analyzer/malloc-ipa-8-double-free.c b/gcc/testsuite/gcc.dg/analyzer/malloc-ipa-8-double-free.c
new file mode 100644
index 0000000..62e7302
--- /dev/null
+++ b/gcc/testsuite/gcc.dg/analyzer/malloc-ipa-8-double-free.c
@@ -0,0 +1,163 @@
+/* Example of a multilevel wrapper around malloc/free, with a double-free.  */
+
+/* { dg-options "--analyzer -fdiagnostics-show-line-numbers -fdiagnostics-nn-line-numbers -fdump-analyzer-summaries -fanalyzer-checker=malloc -fanalyzer-verbose-state-changes" } */
+
+#include <stdlib.h>
+
+void *wrapped_malloc (size_t size) /* { dg-warning "summary: add: '<return-value>': 'start' -> 'unchecked'" } */
+{
+  return malloc (size);
+}
+
+void wrapped_free (void *ptr) /* { dg-warning "summary: add: 'ptr': 'start' -> 'free'" } */
+/* { dg-warning "summary: transition: 'ptr': 'nonnull' -> 'free'" "" { target *-*-* } .-1 } */
+/* { dg-warning "summary: transition: 'ptr': 'free' -> 'stop'" "" { target *-*-* } .-2 } */
+{
+  free (ptr); /* { dg-warning "double-free of 'ptr' \\\[CWE-415\\\]" } */
+  /* FIXME: unchecked -> free is correct, but start -> free should be pruned
+     from the path.  */
+}
+
+typedef struct boxed_int
+{
+  int i;
+} boxed_int;
+
+boxed_int *
+make_boxed_int (int i) /* { dg-warning "summary: add: '<return-value>': 'start' -> 'nonnull'" } */
+{
+  boxed_int *result = (boxed_int *)wrapped_malloc (sizeof (boxed_int));
+  if (!result)
+    abort ();
+  result->i = i;
+  return result;
+}
+
+void
+free_boxed_int (boxed_int *bi) /* { dg-warning "summary: add: 'bi': 'start' -> 'free'" } */
+/* { dg-warning "summary: add: 'bi': 'start' -> 'stop'" "" { target *-*-* } .-1 } */
+{
+  wrapped_free (bi);
+  /* FIXME: events here are wrong; they refer to ptr, not bi.
+     (was "state of 'ptr': 'start' -> 'free'")
+     Also, they should be just start->free, or be skipped.  */
+}
+
+void test (int i)
+{
+  boxed_int *obj = make_boxed_int (i);
+
+  free_boxed_int (obj);
+
+  free_boxed_int (obj);
+}
+
+/* TODO: various strange entries in the path.  */
+
+/* Double-free.  */
+/* { dg-begin-multiline-output "" }
+  'test': events 1-2
+     |
+     |   NN | void test (int i)
+     |      |      ^~~~
+     |      |      |
+     |      |      (1) entry to 'test'
+     |   NN | {
+     |   NN |   boxed_int *obj = make_boxed_int (i);
+     |      |                    ~~~~~~~~~~~~~~~~~~
+     |      |                    |
+     |      |                    (2) calling 'make_boxed_int' from 'test'
+     |
+     +--> 'make_boxed_int': event 3
+                  |
+                  |   NN | make_boxed_int (int i)
+                  |      | ^~~~~~~~~~~~~~
+                  |      | |
+                  |      | (3) entry to 'make_boxed_int'
+                  |
+          'wrapped_malloc': event 4
+                  |
+                  |   NN | void *wrapped_malloc (size_t size)
+                  |      |       ^~~~~~~~~~~~~~
+                  |      |       |
+                  |      |       (4) entry to 'wrapped_malloc'
+                  |
+     <------------+
+     |
+  'test': events 5-6
+     |
+     |   NN |   boxed_int *obj = make_boxed_int (i);
+     |      |                    ^~~~~~~~~~~~~~~~~~
+     |      |                    |
+     |      |                    (5) returning to 'test' from 'make_boxed_int'
+     |   NN | 
+     |   NN |   free_boxed_int (obj);
+     |      |   ~~~~~~~~~~~~~~~~~~~~
+     |      |   |
+     |      |   (6) calling 'free_boxed_int' from 'test'
+     |
+     +--> 'free_boxed_int': events 7-9
+                  |
+                  |   NN | free_boxed_int (boxed_int *bi)
+                  |      | ^~~~~~~~~~~~~~
+                  |      | |
+                  |      | (7) entry to 'free_boxed_int'
+                  |......
+                  |   NN |   wrapped_free (bi);
+                  |      |   ~~~~~~~~~~~~~~~~~
+                  |      |   |
+                  |      |   (8) state of 'ptr': 'start' -> 'nonnull' (origin: NULL)
+                  |      |   (9) first 'free' here (state of 'ptr': 'start' -> 'free', origin: NULL)
+                  |
+          'wrapped_free': events 10-12
+                 |
+                 |   NN | void wrapped_free (void *ptr)
+                 |      |      ^~~~~~~~~~~~
+                 |      |      |
+                 |      |      (10) entry to 'wrapped_free'
+                 |......
+                 |   NN |   free (ptr);
+                 |      |   ~~~~~~~~~~
+                 |      |   |
+                 |      |   (11) first 'free' here (state of 'ptr': 'start' -> 'free', origin: NULL)
+                 |      |   (12) first 'free' here (state of 'ptr': 'nonnull' -> 'free', origin: NULL)
+                 |
+     <-----------+
+     |
+  'test': events 13-14
+     |
+     |   NN |   free_boxed_int (obj);
+     |      |   ^~~~~~~~~~~~~~~~~~~~
+     |      |   |
+     |      |   (13) returning to 'test' from 'free_boxed_int'
+     |   NN | 
+     |   NN |   free_boxed_int (obj);
+     |      |   ~~~~~~~~~~~~~~~~~~~~
+     |      |   |
+     |      |   (14) calling 'free_boxed_int' from 'test'
+     |
+     +--> 'free_boxed_int': events 15-16
+                  |
+                  |   NN | free_boxed_int (boxed_int *bi)
+                  |      | ^~~~~~~~~~~~~~
+                  |      | |
+                  |      | (15) entry to 'free_boxed_int'
+                  |......
+                  |   NN |   wrapped_free (bi);
+                  |      |   ~~~~~~~~~~~~~~~~~
+                  |      |   |
+                  |      |   (16) calling 'wrapped_free' from 'free_boxed_int'
+                  |
+                  +--> 'wrapped_free': events 17-18
+                              |
+                              |   NN | void wrapped_free (void *ptr)
+                              |      |      ^~~~~~~~~~~~
+                              |      |      |
+                              |      |      (17) entry to 'wrapped_free'
+                              |......
+                              |   NN |   free (ptr);
+                              |      |   ~~~~~~~~~~
+                              |      |   |
+                              |      |   (18) second 'free' here ('ptr' is in state 'free')
+                              |
+   { dg-end-multiline-output "" } */
diff --git a/gcc/testsuite/gcc.dg/analyzer/malloc-ipa-8-unchecked.c b/gcc/testsuite/gcc.dg/analyzer/malloc-ipa-8-unchecked.c
new file mode 100644
index 0000000..48680e0
--- /dev/null
+++ b/gcc/testsuite/gcc.dg/analyzer/malloc-ipa-8-unchecked.c
@@ -0,0 +1,65 @@
+/* Example of an  multilevel wrapper around malloc, with an unchecked write.  */
+
+/* { dg-options "--analyzer -fdiagnostics-show-line-numbers -fdiagnostics-nn-line-numbers -fdump-analyzer-summaries -fanalyzer-checker=malloc -fanalyzer-verbose-state-changes" } */
+
+#include <stdlib.h>
+
+void *wrapped_malloc (size_t size) /* { dg-warning "summary: add: '<return-value>': 'start' -> 'unchecked'" } */
+{
+  return malloc (size); /* { dg-message "this call could return NULL" } */
+}
+
+typedef struct boxed_int
+{
+  int i;
+} boxed_int;
+
+boxed_int *
+make_boxed_int (int i) /* { dg-warning "summary: add: '<return-value>': 'start' -> 'nonnull'" } */
+{
+  boxed_int *result = (boxed_int *)wrapped_malloc (sizeof (boxed_int));
+  result->i = i; /* { dg-warning "use of possibly-NULL 'result'" } */
+  /* { dg-message "\\(.*\\) 'result' could be NULL" "" { target *-*-* } .-1 } */
+  return result;
+}
+
+/* "use of possibly-NULL 'result' [CWE-690]".  */
+/* { dg-begin-multiline-output "" }
+  'make_boxed_int': events 1-2
+          |
+          |   NN | make_boxed_int (int i)
+          |      | ^~~~~~~~~~~~~~
+          |      | |
+          |      | (1) entry to 'make_boxed_int'
+          |   NN | {
+          |   NN |   boxed_int *result = (boxed_int *)wrapped_malloc (sizeof (boxed_int));
+          |      |                                    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+          |      |                                    |
+          |      |                                    (2) calling 'wrapped_malloc' from 'make_boxed_int'
+          |
+          +--> 'wrapped_malloc': events 3-4
+                       |
+                       |   NN | void *wrapped_malloc (size_t size)
+                       |      |       ^~~~~~~~~~~~~~
+                       |      |       |
+                       |      |       (3) entry to 'wrapped_malloc'
+                       |   NN | {
+                       |   NN |   return malloc (size);
+                       |      |          ~~~~~~~~~~~~~
+                       |      |          |
+                       |      |          (4) this call could return NULL (state of '<return-value>': 'start' -> 'unchecked', origin: NULL)
+                       |
+          <------------+
+          |
+  'make_boxed_int': events 5-6
+          |
+          |   NN |   boxed_int *result = (boxed_int *)wrapped_malloc (sizeof (boxed_int));
+          |      |                                    ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+          |      |                                    |
+          |      |                                    (5) returning to 'make_boxed_int' from 'wrapped_malloc'
+          |   NN |   result->i = i;
+          |      |   ~~~~~~~~~~~~~                     
+          |      |             |
+          |      |             (6) 'result' could be NULL ('result' is in state 'unchecked')
+          |
+  { dg-end-multiline-output "" } */
diff --git a/gcc/testsuite/gcc.dg/analyzer/malloc-ipa-8.c b/gcc/testsuite/gcc.dg/analyzer/malloc-ipa-8.c
deleted file mode 100644
index 80c490c..0000000
--- a/gcc/testsuite/gcc.dg/analyzer/malloc-ipa-8.c
+++ /dev/null
@@ -1,70 +0,0 @@
-/* Example of a multilevel wrapper around malloc/free, with a double-free.  */
-/* TODO: split into two test cases?
-   (one for the unchecked malloc, the other for the double-free).  */
-
-/* { dg-options "--analyzer -fdiagnostics-path-summary-format=none -fdump-analyzer-summaries -fanalyzer-checker=malloc -fanalyzer-verbose-state-changes" } */
-
-#include <stdlib.h>
-
-void *wrapped_malloc (size_t size) /* { dg-warning "summary: add: '<return-value>': 'start' -> 'unchecked'" } */
-/* { dg-message "\\(4\\) entry to 'wrapped_malloc'" "" { target *-*-* } .-1 } */
-{
-  return malloc (size); /* { dg-message "this call could return NULL" } */
-}
-
-void wrapped_free (void *ptr) /* { dg-warning "summary: add: 'ptr': 'start' -> 'free'" } */
-/* { dg-warning "summary: transition: 'ptr': 'nonnull' -> 'free'" "" { target *-*-* } .-1 } */
-/* { dg-warning "summary: transition: 'ptr': 'free' -> 'stop'" "" { target *-*-* } .-2 } */
-/* { dg-message "\\(10\\) entry to 'wrapped_free'" "" { target *-*-* } .-3 } */
-/* { dg-message "\\(17\\) entry to 'wrapped_free'" "" { target *-*-* } .-4 } */
-{
-  free (ptr); /* { dg-warning "double-free of 'ptr' \\\[CWE-415\\\]" } */
-  /* { dg-message "\\(11\\) first 'free' here" "" { target *-*-* } .-1 } */
-  /* { dg-message "\\(12\\) first 'free' here" "" { target *-*-* } .-2 } */
-  /* FIXME: unchecked -> free is correct, but start -> free should be pruned
-     from the path.
-     FIXME: do we need a way of turning off the friendlier messages?  */
-  /* { dg-message "\\(18\\) second 'free' here" "" { target *-*-* } .-6 } */
-}
-
-typedef struct boxed_int
-{
-  int i;
-} boxed_int;
-
-boxed_int *
-make_boxed_int (int i) /* { dg-warning "summary: add: '<return-value>': 'start' -> 'nonnull'" } */
-/* { dg-message "\\(3\\) entry to 'make_boxed_int'" "" { target *-*-* } .-1 } */
-{
-  boxed_int *result = (boxed_int *)wrapped_malloc (sizeof (boxed_int));
-  result->i = i; /* { dg-warning "use of possibly-NULL 'result'" } */
-  /* { dg-message "\\(.*\\) 'result' could be NULL" "" { target *-*-* } .-1 } */
-  return result;
-}
-
-void
-free_boxed_int (boxed_int *bi) /* { dg-warning "summary: add: 'bi': 'start' -> 'free'" } */
-/* { dg-warning "summary: add: 'bi': 'start' -> 'stop'" "" { target *-*-* } .-1 } */
-/* { dg-message "\\(7\\) entry to 'free_boxed_int'" "" { target *-*-* } .-2 } */
-/* { dg-message "\\(15\\) entry to 'free_boxed_int'" "" { target *-*-* } .-3 } */
-{
-  wrapped_free (bi); /* { dg-message "\\(8\\) state of 'ptr': 'start' -> 'nonnull'" } */
-  /* { dg-message "\\(9\\) first 'free' here" "" { target *-*-* } .-1 } */
-  /* FIXME: these are wrong; they refer to ptr, not bi.
-     (was "state of 'ptr': 'start' -> 'free'")
-     Also, they should be just start->free, or be skipped.  */
-  /* { dg-message "\\(16\\) calling 'wrapped_free' from 'free_boxed_int'" "" { target *-*-* } .-5 } */
-}
-
-void test (int i) /* { dg-message "\\(1\\) entry to 'test'" } */
-{
-  boxed_int *obj = make_boxed_int (i); /* { dg-message "\\(2\\) calling 'make_boxed_int' from 'test'" } */
-  /* { dg-message "\\(5\\) returning to 'test' from 'make_boxed_int'" "" { target *-*-* } .-1 } */
-
-  free_boxed_int (obj); /* { dg-message "\\(6\\) calling 'free_boxed_int' from 'test'" } */
-  /* { dg-message "\\(13\\) returning to 'test' from 'free_boxed_int'" "" { target *-*-* } .-1 } */
-
-  free_boxed_int (obj); /* { dg-message "\\(14\\) calling 'free_boxed_int' from 'test'" } */
-}
-
-/* TODO: various strange entries in the path.  */
diff --git a/gcc/testsuite/gcc.dg/analyzer/malloc-paths-7.c b/gcc/testsuite/gcc.dg/analyzer/malloc-paths-7.c
index 7f5e322..82f54c1 100644
--- a/gcc/testsuite/gcc.dg/analyzer/malloc-paths-7.c
+++ b/gcc/testsuite/gcc.dg/analyzer/malloc-paths-7.c
@@ -13,7 +13,7 @@ void test (void)
     {
       free (q);
       return; /* { dg-warning "leak of 'p'" } */ 
-      /* { dg-message "\\(2\\) here" "" { target *-*-* } .-1 } */
+      /* { dg-message "\\(2\\) 'p' leaks here" "" { target *-*-* } .-1 } */
     }
   bar ();
   free (q);
diff --git a/gcc/testsuite/gcc.dg/analyzer/malloc-paths-8.c b/gcc/testsuite/gcc.dg/analyzer/malloc-paths-8.c
index 612858d..d033969 100644
--- a/gcc/testsuite/gcc.dg/analyzer/malloc-paths-8.c
+++ b/gcc/testsuite/gcc.dg/analyzer/malloc-paths-8.c
@@ -32,3 +32,21 @@ void test_2 (size_t sz)
   if (sz >= LIMIT)
     free (ptr);
 }
+
+void test_3 (size_t sz)
+{
+  void *ptr;
+  if (sz <= LIMIT)
+    ptr = alloca (sz); /* { dg-message "memory is allocated on the stack here" } */
+  else
+    ptr = malloc (sz);
+
+  do_stuff (ptr);
+
+  /* Bug: the "sz <= LIMIT" above should have been "sz < LIMIT",
+     so there's a free-of-alloca when sz == LIMIT.  */
+  if (sz >= LIMIT)
+    free (ptr); /* { dg-warning "free of memory allocated on the stack by 'alloca'" } */
+}
+/* { dg-bogus "leak of 'ptr'" } */
+/* This can't happen, as "sz > 1024" && "sz <= 1023" is impossible.  */
diff --git a/gcc/testsuite/gcc.dg/analyzer/switch.c b/gcc/testsuite/gcc.dg/analyzer/switch.c
index 06d1398..a55ba2b 100644
--- a/gcc/testsuite/gcc.dg/analyzer/switch.c
+++ b/gcc/testsuite/gcc.dg/analyzer/switch.c
@@ -7,11 +7,7 @@ void test (int i)
       break;
 
     case 3 ... 5:
-      __analyzer_eval (i >= 3); /* { dg-warning "TRUE" "" { xfail *-*-* } } */
-      /* { dg-warning "UNKNOWN" "" { target *-*-* } .-1 } */
-      /* TODO(xfail^^^): The above comes in as "i_6(D) > 2" and hence
-	 doesn't match the constraint i_6 >= 3 we already have
-	 (actually 3 <= i_6).  */
+      __analyzer_eval (i >= 3); /* { dg-warning "TRUE" } */
       __analyzer_eval (i <= 5); /* { dg-warning "TRUE" } */
       break;
 
-- 
1.8.5.3

