From 0f7b852d6bc5d7caefe3d75202f839c186c83b25 Mon Sep 17 00:00:00 2001
From: David Malcolm <dmalcolm@redhat.com>
Date: Tue, 21 May 2019 09:04:39 -0400
Subject: [PATCH 61/67] FIXME: 2019-05-21 work on region model

---
 gcc/analyzer/constraint-manager.cc                 | 259 ++-----------
 gcc/analyzer/constraint-manager.h                  |  17 -
 gcc/analyzer/hardcoded-state-machine-malloc.cc     | 192 +++++++++-
 gcc/analyzer/region-model.cc                       | 421 ++++++++++++++++-----
 gcc/analyzer/region-model.h                        |  49 +--
 gcc/common.opt                                     |  10 +-
 .../malloc-checker/arg_must_not_be_null/input.c    |  30 --
 .../malloc-checker/arg_must_not_be_null/script.py  |  23 --
 .../malloc-checker/arg_must_not_be_null/stderr.txt |   4 -
 .../malloc-checker/arg_must_not_be_null/stdout.txt |   0
 .../checkers/malloc-checker/double_free/input.c    |  29 --
 .../double_free/input.c.cpychecker-log.txt         |   1 -
 .../checkers/malloc-checker/double_free/script.py  |  23 --
 .../checkers/malloc-checker/double_free/stderr.txt |   7 -
 .../checkers/malloc-checker/double_free/stdout.txt |   0
 .../checkers/signal_handler/example/stderr.txt     |   5 -
 .../checkers/signal_handler/example/stdout.txt     |   0
 .../regression/rhs-is-vardecl/stdout.txt           |   0
 gcc/testsuite/gcc.dg/analyzer/attribute-nonnull.c  |  57 +++
 gcc/testsuite/gcc.dg/analyzer/data-model-1.c       |  10 +-
 gcc/testsuite/gcc.dg/analyzer/malloc-vs-local.c    |  83 ++++
 gcc/testsuite/gcc.dg/analyzer/pragma-1.c           |  26 ++
 22 files changed, 764 insertions(+), 482 deletions(-)
 delete mode 100644 gcc/testsuite/gcc.dg/TODO-analyzer/checkers/malloc-checker/arg_must_not_be_null/input.c
 delete mode 100644 gcc/testsuite/gcc.dg/TODO-analyzer/checkers/malloc-checker/arg_must_not_be_null/script.py
 delete mode 100644 gcc/testsuite/gcc.dg/TODO-analyzer/checkers/malloc-checker/arg_must_not_be_null/stderr.txt
 delete mode 100644 gcc/testsuite/gcc.dg/TODO-analyzer/checkers/malloc-checker/arg_must_not_be_null/stdout.txt
 delete mode 100644 gcc/testsuite/gcc.dg/TODO-analyzer/checkers/malloc-checker/double_free/input.c
 delete mode 100644 gcc/testsuite/gcc.dg/TODO-analyzer/checkers/malloc-checker/double_free/input.c.cpychecker-log.txt
 delete mode 100644 gcc/testsuite/gcc.dg/TODO-analyzer/checkers/malloc-checker/double_free/script.py
 delete mode 100644 gcc/testsuite/gcc.dg/TODO-analyzer/checkers/malloc-checker/double_free/stderr.txt
 delete mode 100644 gcc/testsuite/gcc.dg/TODO-analyzer/checkers/malloc-checker/double_free/stdout.txt
 delete mode 100644 gcc/testsuite/gcc.dg/TODO-analyzer/checkers/signal_handler/example/stderr.txt
 delete mode 100644 gcc/testsuite/gcc.dg/TODO-analyzer/checkers/signal_handler/example/stdout.txt
 delete mode 100644 gcc/testsuite/gcc.dg/TODO-analyzer/regression/rhs-is-vardecl/stdout.txt
 create mode 100644 gcc/testsuite/gcc.dg/analyzer/attribute-nonnull.c
 create mode 100644 gcc/testsuite/gcc.dg/analyzer/malloc-vs-local.c
 create mode 100644 gcc/testsuite/gcc.dg/analyzer/pragma-1.c

diff --git a/gcc/analyzer/constraint-manager.cc b/gcc/analyzer/constraint-manager.cc
index 531d1ff..c3204c2 100644
--- a/gcc/analyzer/constraint-manager.cc
+++ b/gcc/analyzer/constraint-manager.cc
@@ -319,7 +319,6 @@ equiv_class_id::get_obj (constraint_manager &cm) const
 /* FIXME.  */
 
 constraint_manager::constraint_manager (const constraint_manager &other)
-: m_stack_depth (other.m_stack_depth)
 {
   // FIXME: auto_vec's copy_ctor...
   int i;
@@ -346,8 +345,6 @@ constraint_manager::~constraint_manager ()
 constraint_manager&
 constraint_manager::operator= (const constraint_manager &other)
 {
-  m_stack_depth = other.m_stack_depth;
-
   gcc_assert (m_equiv_classes.length () == 0);
   gcc_assert (m_constraints.length () == 0);
 
@@ -372,7 +369,6 @@ constraint_manager::hash () const
   equiv_class *ec;
   constraint *c;
 
-  hstate.add_int (m_stack_depth);
   FOR_EACH_VEC_ELT (m_equiv_classes, i, ec)
     hstate.merge_hash (ec->hash ());
   FOR_EACH_VEC_ELT (m_constraints, i, c)
@@ -385,8 +381,6 @@ constraint_manager::hash () const
 bool
 constraint_manager::operator== (const constraint_manager &other) const
 {
-  if (m_stack_depth != other.m_stack_depth)
-    return false;
   if (m_equiv_classes.length () != other.m_equiv_classes.length ())
     return false;
 
@@ -429,7 +423,7 @@ constraint_manager::print (pretty_printer *pp) const
 	pp_string (pp, " && ");
       pp_string (pp, c->to_str (*this).c_str ());
     }
-  pp_printf (pp, "}@%i", m_stack_depth);
+  pp_printf (pp, "}");
 }
 
 /* FIXME.  */
@@ -491,195 +485,6 @@ constraint_manager::dump () const
 
 /* FIXME.  */
 
-void
-constraint_manager::on_assignment (svalue_id lhs, svalue_id rhs)
-{
-  /* Clear LHS.  */
-  purge_one_svalue_id p (lhs);
-  purge (p);
-
-  add_constraint (lhs, EQ_EXPR, rhs);
-}
-
-#if 0
-
-/* FIXME.
-   Attempt to extend this path's state with the constraints required by
-   EDGE (where LAST_STMT, if non-NULL, was the stmt guarding the edge).
-   Return true if the edge can be followed, false if it can't be.  */
-
-bool
-constraint_manager::apply_constraints_for_edge (const superedge &edge,
-					const gimple *last_stmt)
-{
-  if (edge.m_kind == SUPEREDGE_CALL)
-    // FIXME: use as_a<>
-    return apply_constraints_for_call (*edge.dyn_cast_call_superedge ());
-
-  if (edge.m_kind == SUPEREDGE_RETURN)
-    // FIXME: use as_a<>
-    return apply_constraints_for_return (*edge.dyn_cast_return_superedge ());
-
-  if (last_stmt == NULL)
-    return true;
-
-  if (const gcond *cond_stmt = dyn_cast <const gcond *> (last_stmt))
-    return apply_constraints_for_gcond (edge, cond_stmt);
-
-  // FIXME: some linker issues with is_a_helper const
-  if (const gswitch *switch_stmt = dyn_cast <gswitch *> (const_cast <gimple *> (last_stmt)))
-    return apply_constraints_for_gswitch (edge, switch_stmt);
-
-  return true;
-}
-
-/* FIXME.  */
-
-bool
-constraint_manager::apply_constraints_for_call (const call_superedge& edge)
-{
-  /* Map args to parms at next stack_depth, incrementing stack depth.  */
-  int caller_stack_depth = m_stack_depth;
-  int callee_stack_depth = ++m_stack_depth;
-
-  tree callee = edge.get_callee_decl ();
-  gcall *call_stmt = edge.get_call_stmt ();
-
-  int i = 0;
-  for (tree parm = DECL_ARGUMENTS (callee); parm;
-       parm = DECL_CHAIN (parm), ++i)
-    {
-      tree parm_default_ssa = ssa_default_def (edge.m_dest->m_fun, parm);
-      if (parm_default_ssa)
-	add_constraint (path_var (parm_default_ssa, callee_stack_depth),
-			EQ_EXPR,
-			path_var (gimple_call_arg (call_stmt, i),
-				  caller_stack_depth));
-    }
-  return true;
-}
-
-/* FIXME.  */
-
-bool
-constraint_manager::apply_constraints_for_return (const return_superedge&)
-{
-  pop_stack_frame ();
-  return true;
-}
-
-/* A subclass of purge_criteria: purge anything above a given stack depth.  */
-
-class purge_above_stack_frame : public purge_criteria
-{
-public:
-  purge_above_stack_frame (int max_stack_depth)
-  : m_max_stack_depth (max_stack_depth) {}
-
-  bool should_purge_p (path_var pv) const FINAL OVERRIDE
-  {
-    return pv.m_stack_depth > m_max_stack_depth;
-  }
-
-private:
-  int m_max_stack_depth;
-};
-
-
-/* Decrement the stack depth, purging vars at the old stack depth (and beyond).
-   This is broken out as a subroutine so it can be unit-tested.  */
-
-void
-constraint_manager::pop_stack_frame ()
-{
-  int caller_stack_depth = --m_stack_depth;
-
-  purge_above_stack_frame p (caller_stack_depth);
-  purge (p);
-}
-
-/* FIXME.  */
-
-bool
-constraint_manager::apply_constraints_for_gcond (const superedge &edge,
-					 const gcond *cond_stmt)
-{
-  ::edge cfg_edge = edge.get_any_cfg_edge ();
-  gcc_assert (cfg_edge != NULL);
-  gcc_assert (cfg_edge->flags & (EDGE_TRUE_VALUE | EDGE_FALSE_VALUE));
-
-  enum tree_code op = gimple_cond_code (cond_stmt);
-  tree lhs = gimple_cond_lhs (cond_stmt);
-  tree rhs = gimple_cond_rhs (cond_stmt);
-  if (cfg_edge->flags & EDGE_FALSE_VALUE)
-    op = invert_tree_comparison (op, false /* honor_nans */);
-  return add_constraint (path_var (lhs, m_stack_depth),
-			 op,
-			 path_var (rhs, m_stack_depth));
-}
-
-/* FIXME.  */
-
-bool
-constraint_manager::apply_constraints_for_gswitch (const superedge &edge,
-					   const gswitch *switch_stmt)
-{
-  // FIXME: use an as_a for this cast:
-  const switch_cfg_superedge &switch_edge = (const switch_cfg_superedge &)edge;
-  path_var index (gimple_switch_index (switch_stmt), m_stack_depth);
-  tree case_label = switch_edge.get_case_label ();
-  gcc_assert (TREE_CODE (case_label) == CASE_LABEL_EXPR);
-  path_var lower_bound (CASE_LOW (case_label), m_stack_depth);
-  path_var upper_bound (CASE_HIGH (case_label), m_stack_depth);
-  if (lower_bound.m_tree)
-    {
-      if (upper_bound.m_tree)
-	{
-	  /* Range.  */
-	  if (!add_constraint (index, GE_EXPR, lower_bound))
-	    return false;
-	  return add_constraint (index, LE_EXPR, upper_bound);
-	}
-      else
-	/* Single-value.  */
-	return add_constraint (index, EQ_EXPR, lower_bound);
-    }
-  else
-    {
-      /* The default case.
-	 Add exclusions based on the other cases.  */
-      for (unsigned other_idx = 1;
-	   other_idx < gimple_switch_num_labels (switch_stmt);
-	   other_idx++)
-	{
-	  tree other_label = gimple_switch_label (switch_stmt,
-						  other_idx);
-	  path_var other_lower_bound (CASE_LOW (other_label), m_stack_depth);
-	  path_var other_upper_bound (CASE_HIGH (other_label), m_stack_depth);
-	  gcc_assert (other_lower_bound.m_tree);
-	  if (other_upper_bound.m_tree)
-	    {
-	      /* Exclude this range-valued case.
-		 For now, we just exclude the boundary values.
-		 TODO: exclude the values within the region.  */
-	      if (!add_constraint (index, NE_EXPR, other_lower_bound))
-		return false;
-	      if (!add_constraint (index, NE_EXPR, other_upper_bound))
-		return false;
-	    }
-	  else
-	    /* Exclude this single-valued case.  */
-	    if (!add_constraint (index, NE_EXPR, other_lower_bound))
-	      return false;
-	}
-      return true;
-    }
-}
-
-#endif
-
-/* FIXME.  */
-
 bool
 constraint_manager::add_constraint (svalue_id lhs,
 				    enum tree_code op,
@@ -2115,45 +1920,59 @@ test_assignment ()
 }
 #endif
 
-#if 0
 /* Check that operator== and hashing works as expected for the
    various types.  */
 
 static void
 test_equality ()
 {
-  svalue_id int_42 (build_int_cst (integer_type_node, 42), 0);
-  svalue_id int_0 (build_int_cst (integer_type_node, 0), 0);
+  tree int_42 = build_int_cst (integer_type_node, 42);
+  tree int_0 = build_int_cst (integer_type_node, 0);
 
-  svalue_id x (build_decl (UNKNOWN_LOCATION, PARM_DECL,
-			  get_identifier ("x"),
-			  integer_type_node), 0);
-  svalue_id y (build_decl (UNKNOWN_LOCATION, PARM_DECL,
-			  get_identifier ("y"),
-			  integer_type_node), 0);
-  svalue_id z (build_decl (UNKNOWN_LOCATION, PARM_DECL,
-			  get_identifier ("z"),
-			  integer_type_node), 0);
+  tree x = build_decl (UNKNOWN_LOCATION, VAR_DECL,
+		       get_identifier ("x"),
+		       integer_type_node);
+  tree y = build_decl (UNKNOWN_LOCATION, VAR_DECL,
+		       get_identifier ("y"),
+		       integer_type_node);
+  tree z = build_decl (UNKNOWN_LOCATION, VAR_DECL,
+		       get_identifier ("z"),
+		       integer_type_node);
 
   {
-    constraint_manager cm0;
-    constraint_manager cm1;
+    region_model model0;
+    region_model model1;
 
-    ASSERT_EQ (cm0.hash (), cm1.hash ());
-    ASSERT_EQ (cm0, cm1);
+    constraint_manager *cm0 = model0.get_constraints ();
+    constraint_manager *cm1 = model1.get_constraints ();
 
-    ADD_SAT_CONSTRAINT (cm1, x, EQ_EXPR, y);
-    ASSERT_NE (cm0.hash (), cm1.hash ());
-    ASSERT_NE (cm0, cm1);
+    ASSERT_EQ (cm0->hash (), cm1->hash ());
+    ASSERT_EQ (*cm0, *cm1);
+
+    ASSERT_EQ (model0.hash (), model1.hash ());
+    ASSERT_EQ (model0, model1);
 
-    constraint_manager cm2;
+    ADD_SAT_CONSTRAINT (model1, x, EQ_EXPR, y);
+    ASSERT_NE (cm0->hash (), cm1->hash ());
+    ASSERT_NE (*cm0, *cm1);
+
+    ASSERT_NE (model0.hash (), model1.hash ());
+    ASSERT_NE (model0, model1);
+
+    region_model model2;
+    constraint_manager *cm2 = model2.get_constraints ();
     /* Make the same change to cm2.  */
-    ADD_SAT_CONSTRAINT (cm2, x, EQ_EXPR, y);
-    ASSERT_EQ (cm1.hash (), cm2.hash ());
-    ASSERT_EQ (cm1, cm2);
+    ADD_SAT_CONSTRAINT (model2, x, EQ_EXPR, y);
+    ASSERT_EQ (cm1->hash (), cm2->hash ());
+    ASSERT_EQ (*cm1, *cm2);
+
+    ASSERT_EQ (model1.hash (), model2.hash ());
+    ASSERT_EQ (model1, model2);
   }
 }
 
+#if 0
+
 /* A subclass of purge_criteria for selftests: purge all svalue_id instances.  */
 
 class purge_all_svalue_ids : public purge_criteria
@@ -2267,7 +2086,9 @@ analyzer_constraint_manager_cc_tests ()
 #if 0
   test_assignment ();
   test_stack_frames ();
+#endif
   test_equality ();
+#if 0
   test_purging ();
 #endif
 }
diff --git a/gcc/analyzer/constraint-manager.h b/gcc/analyzer/constraint-manager.h
index 3c75075..2e4dcea 100644
--- a/gcc/analyzer/constraint-manager.h
+++ b/gcc/analyzer/constraint-manager.h
@@ -200,28 +200,12 @@ public:
     return ec_id.get_obj (*this);
   }
 
-  void on_assignment (svalue_id lhs, svalue_id rhs);
-
-  bool apply_constraints_for_edge (const superedge &edge,
-				   const gimple *last_stmt);
-
   bool add_constraint (svalue_id lhs, enum tree_code op, svalue_id 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);
-
-  bool apply_constraints_for_return (const return_superedge& edge);
-
-  void pop_stack_frame ();
-
-  bool apply_constraints_for_gcond (const superedge &edge,
-				    const gcond *cond_stmt);
-  bool apply_constraints_for_gswitch (const superedge &edge,
-				      const gswitch *switch_stmt);
   bool get_equiv_class (svalue_id sid, equiv_class_id *out) const;
   equiv_class_id get_or_add_equiv_class (svalue_id sid);
   tristate eval_condition (equiv_class_id lhs,
@@ -243,7 +227,6 @@ public:
 
   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,
diff --git a/gcc/analyzer/hardcoded-state-machine-malloc.cc b/gcc/analyzer/hardcoded-state-machine-malloc.cc
index cb612b9..9704bae 100644
--- a/gcc/analyzer/hardcoded-state-machine-malloc.cc
+++ b/gcc/analyzer/hardcoded-state-machine-malloc.cc
@@ -128,11 +128,37 @@ private:
   //event_id_t m_second_free_event;
 };
 
-class possible_null_deref : public malloc_diagnostic
+/* Abstract subclass for describing possible bad uses of NULL.
+   Responsible for describing the call that could return NULL.  */
+
+class possible_null : public malloc_diagnostic
+{
+public:
+  possible_null (const malloc_state_machine &sm, tree arg)
+  : malloc_diagnostic (sm, arg)
+  {}
+
+  label_text describe_critical_state_change (tree expr,
+					     state_machine::state_t old_state,
+					     state_machine::state_t new_state,
+					     event_id_t event_id)
+    FINAL OVERRIDE
+  {
+    if (old_state == m_sm.m_start && new_state == m_sm.m_unchecked)
+      return label_text::borrow ("this call could return NULL");
+    return label_text ();
+  }
+};
+
+/* Concrete subclass for describing dereference of a possible NULL
+   value.  */
+
+class possible_null_deref : public possible_null
 {
 public:
   possible_null_deref (const malloc_state_machine &sm, tree arg)
-  : malloc_diagnostic (sm, arg) {}
+  : possible_null (sm, arg)
+  {}
 
   const char *get_kind () const FINAL OVERRIDE { return "possible_null_deref"; }
 
@@ -145,15 +171,67 @@ public:
 		"use of possibly-NULL %qE", m_arg);
   }
 
-  label_text describe_critical_state_change (tree expr,
-					     state_machine::state_t old_state,
-					     state_machine::state_t new_state,
-					     event_id_t event_id)
-    FINAL OVERRIDE
+  /* FIXME.  */
+  label_text describe_final_event
+    (/*diagnostic_context *ctxt, */
+     tree expr,
+     state_machine::state_t state ATTRIBUTE_UNUSED)
   {
-    if (old_state == m_sm.m_start && new_state == m_sm.m_unchecked)
-      return label_text::borrow ("this call could return NULL");
-    return label_text ();
+    return formatted_print ("%qE could be NULL", expr);
+  }
+
+};
+
+/* Subroutine for use by possible_null_arg::emit and null_arg::emit.
+   Issue a note informing that the pertinent argument must be non-NULL.  */
+
+static void
+inform_nonnull_attribute (tree fndecl, int arg_idx)
+{
+  inform (DECL_SOURCE_LOCATION (fndecl),
+	  "argument %u of %qD must be non-null",
+	  arg_idx + 1, fndecl);
+  /* FIXME: ideally, use the location of the parm
+     and underline the attribute also (but we probably don't have the
+     location_t...)  */
+
+  /* C and C++ FEs have get_fndecl_argument_location.  */
+}
+
+/* Concrete subclass for describing passing a possibly-NULL value to a
+   function marked with __attribute__((nonnull)).  */
+
+class possible_null_arg : public possible_null
+{
+public:
+  possible_null_arg (const malloc_state_machine &sm, tree arg,
+		     tree fndecl, int arg_idx)
+  : possible_null (sm, arg),
+    m_fndecl (fndecl), m_arg_idx (arg_idx)
+  {}
+
+  const char *get_kind () const FINAL OVERRIDE { return "possible_null_arg"; }
+
+  bool subclass_equal_p (const pending_diagnostic &base_other) const
+  {
+    const possible_null_arg &sub_other
+      = (const possible_null_arg &)base_other;
+    return (m_arg == sub_other.m_arg
+	    && m_fndecl == sub_other.m_fndecl
+	    && m_arg_idx == sub_other.m_arg_idx);
+  }
+
+
+  void emit (rich_location *rich_loc) FINAL OVERRIDE
+  {
+    /* CWE-690: Unchecked Return Value to NULL Pointer Dereference.  */
+    auto_diagnostic_group d;
+    metadata m;
+    m.add_cwe (690);
+    warning_at (rich_loc, m, OPT_Wanalyzer_possible_null_argument,
+		"use of possibly-NULL %qE where non-null expected",
+		m_arg);
+    inform_nonnull_attribute (m_fndecl, m_arg_idx);
   }
 
   /* FIXME.  */
@@ -162,11 +240,20 @@ public:
      tree expr,
      state_machine::state_t state ATTRIBUTE_UNUSED)
   {
-    return formatted_print ("%qE could be NULL", expr);
+    return formatted_print ("argument %u (%qE) could be NULL"
+			    " where non-null expected",
+			    m_arg_idx + 1, expr);
   }
 
+  // TODO
+
+private:
+  tree m_fndecl;
+  int m_arg_idx;
 };
 
+/* Concrete subclass for describing a dereference of a NULL value.  */
+
 class null_deref : public malloc_diagnostic
 {
 public:
@@ -185,6 +272,56 @@ public:
   }
 };
 
+/* Concrete subclass for describing passing a NULL value to a
+   function marked with __attribute__((nonnull)).  */
+
+class null_arg : public malloc_diagnostic
+{
+public:
+  null_arg (const malloc_state_machine &sm, tree arg,
+	    tree fndecl, int arg_idx)
+  : malloc_diagnostic (sm, arg),
+    m_fndecl (fndecl), m_arg_idx (arg_idx)
+  {}
+
+  const char *get_kind () const FINAL OVERRIDE { return "null_arg"; }
+
+  bool subclass_equal_p (const pending_diagnostic &base_other) const
+  {
+    const null_arg &sub_other
+      = (const null_arg &)base_other;
+    return (m_arg == sub_other.m_arg
+	    && m_fndecl == sub_other.m_fndecl
+	    && m_arg_idx == sub_other.m_arg_idx);
+  }
+
+  void emit (rich_location *rich_loc) FINAL OVERRIDE
+  {
+    /* CWE-690: Unchecked Return Value to NULL Pointer Dereference.  */
+    auto_diagnostic_group d;
+    metadata m;
+    m.add_cwe (690);
+    warning_at (rich_loc, m, OPT_Wanalyzer_null_argument,
+		"use of NULL %qE where non-null expected", m_arg);
+    inform_nonnull_attribute (m_fndecl, m_arg_idx);
+  }
+
+  /* FIXME.  */
+  label_text describe_final_event
+    (/*diagnostic_context *ctxt, */
+     tree expr,
+     state_machine::state_t state ATTRIBUTE_UNUSED)
+  {
+    return formatted_print ("argument %u (%qE) NULL"
+			    " where non-null expected",
+			    m_arg_idx + 1, expr);
+  }
+
+private:
+  tree m_fndecl;
+  int m_arg_idx;
+};
+
 class use_after_free : public malloc_diagnostic
 {
 public:
@@ -411,6 +548,39 @@ malloc_state_machine::on_stmt (sm_context *sm_ctxt,
 	  sm_ctxt->on_transition (node, stmt, arg, m_non_heap, m_stop);
 	  return true;
 	}
+
+      /* TODO: handle "__attribute__((nonnull))".   */
+      if (tree callee_fndecl = gimple_call_fndecl (stmt))
+	{
+	  tree fntype = TREE_TYPE (callee_fndecl);
+	  bitmap nonnull_args = get_nonnull_args (fntype);
+	  if (nonnull_args)
+	    {
+	      for (unsigned i = 0; i < gimple_call_num_args (stmt); i++)
+		{
+		  tree arg = gimple_call_arg (stmt, i);
+		  if (TREE_CODE (TREE_TYPE (arg)) != POINTER_TYPE)
+		    continue;
+		  /* If we have a nonnull-args, and either all pointers, or just
+		     the specified pointers.  */
+		  if (bitmap_empty_p (nonnull_args)
+		      || bitmap_bit_p (nonnull_args, i))
+		    {
+		      sm_ctxt->warn_for_state
+			(node, stmt, arg, m_unchecked,
+			 new possible_null_arg (*this, arg, callee_fndecl, i));
+		      sm_ctxt->on_transition (node, stmt, arg, m_unchecked,
+					      m_nonnull);
+
+		      sm_ctxt->warn_for_state
+			(node, stmt, arg, m_null,
+			 new null_arg (*this, arg, callee_fndecl, i));
+		      sm_ctxt->on_transition (node, stmt, arg, m_null, m_stop);
+		    }
+		}
+	      BITMAP_FREE (nonnull_args);
+	    }
+	}
     }
 
   /* FIXME: It's not clear if we need this, due to the SSA representation:
diff --git a/gcc/analyzer/region-model.cc b/gcc/analyzer/region-model.cc
index 9849f73..a4da8f8 100644
--- a/gcc/analyzer/region-model.cc
+++ b/gcc/analyzer/region-model.cc
@@ -148,7 +148,55 @@ region_id::dump_node_name_to_pp (pretty_printer *pp) const
 bool
 svalue::operator== (const svalue &other) const
 {
-  return false; // FIXME
+  enum svalue_kind this_kind = get_kind ();
+  enum svalue_kind other_kind = other.get_kind ();
+  if (this_kind != other_kind)
+    return false;
+
+  if (m_type != other.m_type)
+    return false;
+
+  switch (this_kind)
+    {
+    default:
+      gcc_unreachable ();
+    case SK_REGION:
+      {
+	const region_svalue &this_sub
+	  = (const region_svalue &)*this;
+	const region_svalue &other_sub
+	  = (const region_svalue &)other;
+	return this_sub.compare_fields (other_sub);
+      }
+      break;
+    case SK_CONSTANT:
+      {
+	const constant_svalue &this_sub
+	  = (const constant_svalue &)*this;
+	const constant_svalue &other_sub
+	  = (const constant_svalue &)other;
+	return this_sub.compare_fields (other_sub);
+      }
+      break;
+    case SK_POISONED:
+      {
+	const poisoned_svalue &this_sub
+	  = (const poisoned_svalue &)*this;
+	const poisoned_svalue &other_sub
+	  = (const poisoned_svalue &)other;
+	return this_sub.compare_fields (other_sub);
+      }
+      break;
+    case SK_UNKNOWN:
+      {
+	const unknown_svalue &this_sub
+	  = (const unknown_svalue &)*this;
+	const unknown_svalue &other_sub
+	  = (const unknown_svalue &)other;
+	return this_sub.compare_fields (other_sub);
+      }
+      break;
+    }
 }
 
 void
@@ -200,6 +248,12 @@ svalue::to_str () const
 
 /* class region_svalue : public svalue.  */
 
+bool
+region_svalue::compare_fields (const region_svalue &other) const
+{
+  return m_rid == other.m_rid;
+}
+
 hashval_t
 region_svalue::hash () const
 {
@@ -243,6 +297,13 @@ region_svalue::dump_dot_to_pp (const region_model &model,
 
 /* class constant_svalue : public svalue.  */
 
+bool
+constant_svalue::compare_fields (const constant_svalue &other) const
+{
+  // FIXME: should we do tree equality here?
+  return m_cst_expr == other.m_cst_expr;
+}
+
 /* FIXME.  */
 
 hashval_t
@@ -269,6 +330,15 @@ POP_IGNORE_WFORMAT
 
 /* FIXME.  */
 
+bool
+unknown_svalue::compare_fields (const unknown_svalue &other) const
+{
+  /* I *think* we want to return true here, in that when comparing
+     two region models, we want two peer unknown_svalue instances
+     to be the "same".  */
+  return true;
+}
+
 hashval_t
 unknown_svalue::hash () const
 {
@@ -303,6 +373,12 @@ poison_kind_to_str (enum poison_kind kind)
 
 /* class poisoned_svalue : public svalue.  */
 
+bool
+poisoned_svalue::compare_fields (const poisoned_svalue &other) const
+{
+  return m_kind == other.m_kind;
+}
+
 /* FIXME.  */
 
 hashval_t
@@ -352,7 +428,71 @@ region_kind_to_str (enum region_kind kind)
 bool
 region::operator== (const region &other) const
 {
-  return false; // FIXME
+  if (m_parent_rid != other.m_parent_rid)
+    return false;
+  if (m_sval_id != other.m_sval_id)
+    return false;
+  if (m_type != other.m_type)
+    return false;
+
+  enum region_kind this_kind = get_kind ();
+  enum region_kind other_kind = other.get_kind ();
+  if (this_kind != other_kind)
+    return false;
+
+  switch (this_kind)
+    {
+    default:
+      gcc_unreachable ();
+    case RK_MAP:
+      {
+	const map_region &this_sub
+	  = (const map_region &)*this;
+	const map_region &other_sub
+	  = (const map_region &)other;
+	return this_sub.compare_fields (other_sub);
+      }
+    case RK_FRAME:
+      {
+	const frame_region &this_sub
+	  = (const frame_region &)*this;
+	const frame_region &other_sub
+	  = (const frame_region &)other;
+	return this_sub.compare_fields (other_sub);
+      }
+    case RK_STACK:
+      {
+	const stack_region &this_sub
+	  = (const stack_region &)*this;
+	const stack_region &other_sub
+	  = (const stack_region &)other;
+	return this_sub.compare_fields (other_sub);
+      }
+    case RK_ROOT:
+      {
+	const root_region &this_sub
+	  = (const root_region &)*this;
+	const root_region &other_sub
+	  = (const root_region &)other;
+	return this_sub.compare_fields (other_sub);
+      }
+    case RK_SYMBOLIC:
+      {
+	const symbolic_region &this_sub
+	  = (const symbolic_region &)*this;
+	const symbolic_region &other_sub
+	  = (const symbolic_region &)other;
+	return this_sub.compare_fields (other_sub);
+      }
+    case RK_HEAP:
+      {
+	const heap_region &this_sub
+	  = (const heap_region &)*this;
+	const heap_region &other_sub
+	  = (const heap_region &)other;
+	return this_sub.compare_fields (other_sub);
+      }
+    }
 }
 
 /* class region.  */
@@ -602,6 +742,29 @@ map_region::map_region (const map_region &other)
 
 /* FIXME.  */
 
+bool
+map_region::compare_fields (const map_region &other) const
+{
+  if (m_map.elements () != other.m_map.elements ())
+    return false;
+
+  for (map_t::iterator iter = m_map.begin ();
+       iter != m_map.end ();
+       ++iter)
+    {
+      tree key = (*iter).first;
+      region_id e = (*iter).second;
+      region_id *other_slot = const_cast <map_t &> (other.m_map).get (key);
+      if (other_slot == NULL)
+	return false;
+      if (e != *other_slot)
+	return false;
+    }
+  return true;
+}
+
+/* FIXME.  */
+
 region *
 map_region::clone () const
 {
@@ -718,6 +881,18 @@ map_region::add_to_hash (inchash::hash &hstate) const
 
 /* FIXME.  */
 
+bool
+frame_region::compare_fields (const frame_region &other) const
+{
+  if (!map_region::compare_fields (other))
+    return false;
+  if (m_fun != other.m_fun)
+    return false;
+  return true;
+}
+
+/* FIXME.  */
+
 region *
 frame_region::clone () const
 {
@@ -760,6 +935,23 @@ stack_region::stack_region (const stack_region &other)
 
 /* FIXME.  */
 
+bool
+stack_region::compare_fields (const stack_region &other) const
+{
+  if (m_frame_rids.length () != other.m_frame_rids.length ())
+    return false;
+
+  int i;
+  region_id *frame_rid;
+  FOR_EACH_VEC_ELT (m_frame_rids, i, frame_rid)
+    if (m_frame_rids[i] != other.m_frame_rids[i])
+      return false;
+
+  return true;
+}
+
+/* FIXME.  */
+
 region *
 stack_region::clone () const
 {
@@ -840,6 +1032,15 @@ heap_region::heap_region (const heap_region &other)
 {
 }
 
+/* FIXME.  */
+
+bool
+heap_region::compare_fields (const heap_region &other) const
+{
+  /* Empty.  */
+  return true;
+}
+
 region *
 heap_region::clone () const
 {
@@ -869,6 +1070,20 @@ root_region::root_region (const root_region &other)
 
 /* FIXME.  */
 
+bool
+root_region::compare_fields (const root_region &other) const
+{
+  if (m_stack_rid != other.m_stack_rid)
+    return false;
+  if (m_globals_rid != other.m_globals_rid)
+    return false;
+  if (m_heap_rid != other.m_heap_rid)
+    return false;
+  return true;
+}
+
+/* FIXME.  */
+
 region *
 root_region::clone () const
 {
@@ -1062,56 +1277,19 @@ symbolic_region::symbolic_region (const symbolic_region &other)
 
 /* FIXME.  */
 
-region *
-symbolic_region::clone () const
-{
-  return new symbolic_region (*this);
-}
-
-////////////////////////////////////////////////////////////////////////////
-
-/* struct svalue_constraint.  */
-
-/* FIXME.  */
-
-void
-svalue_constraint::print (const region_model &model, pretty_printer *pp) const
+bool
+symbolic_region::compare_fields (const symbolic_region &other) const
 {
-  model.print_svalue (m_lhs, pp);
-  switch (m_op)
-    {
-    default:
-      gcc_unreachable ();
-    case EQ_EXPR:
-      pp_string (pp, " == ");
-      break;
-    case GE_EXPR:
-      pp_string (pp, " >= ");
-      break;
-    case LE_EXPR:
-      pp_string (pp, " <= ");
-      break;
-    case NE_EXPR:
-      pp_string (pp, " != ");
-      break;
-    case GT_EXPR:
-      pp_string (pp, " > ");
-      break;
-    case LT_EXPR:
-      pp_string (pp, " < ");
-      break;
-    }
-  model.print_svalue (m_rhs, pp);
+  /* Empty.  */
+  return true;
 }
 
 /* FIXME.  */
 
-bool
-svalue_constraint::operator== (const svalue_constraint &other) const
+region *
+symbolic_region::clone () const
 {
-  return (m_lhs == other.m_lhs
-	  && m_op == other.m_op
-	  && m_rhs == other.m_rhs);
+  return new symbolic_region (*this);
 }
 
 ////////////////////////////////////////////////////////////////////////////
@@ -1160,7 +1338,7 @@ region_model::operator== (const region_model &other) const
   if (m_svalues.length () != other.m_svalues.length ())
     return false;
 
-  if (!(m_constraints == other.m_constraints))
+  if (*m_constraints != *other.m_constraints)
     return false;
 
   unsigned i;
@@ -1358,7 +1536,8 @@ void
 region_model::validate () const
 {
   // TODO: skip this in a release build
-  // TODO
+  m_constraints->validate ();
+  // TODO: anything else?
 }
 
 /* FIXME.  */
@@ -2416,6 +2595,110 @@ test_unique_constants ()
   ASSERT_NE (model.get_rvalue (int_0), model.get_rvalue (int_42));
 }
 
+/* Check that operator== and hashing works as expected for the
+   various svalue subclasses.  */
+
+static void
+test_svalue_equality ()
+{
+  tree int_42 = build_int_cst (integer_type_node, 42);
+  tree int_0 = build_int_cst (integer_type_node, 0);
+
+  /* Create pairs instances of the various subclasses of svalue,
+     testing for hash and equality between (this, this) and
+     (this, other of same subclass). */
+  svalue *ptr_to_r0
+    = new region_svalue (ptr_type_node, region_id::from_int (0));
+  svalue *ptr_to_r1
+    = new region_svalue (ptr_type_node, region_id::from_int (1));
+
+  ASSERT_EQ (ptr_to_r0->hash (), ptr_to_r0->hash ());
+  ASSERT_EQ (*ptr_to_r0, *ptr_to_r0);
+
+  ASSERT_NE (ptr_to_r0->hash (), ptr_to_r1->hash ());
+  ASSERT_NE (*ptr_to_r0, *ptr_to_r1);
+
+  svalue *cst_int_42 = new constant_svalue (int_42);
+  svalue *cst_int_0 = new constant_svalue (int_0);
+
+  ASSERT_EQ (cst_int_42->hash (), cst_int_42->hash ());
+  ASSERT_EQ (*cst_int_42, *cst_int_42);
+
+  ASSERT_NE (cst_int_42->hash (), cst_int_0->hash ());
+  ASSERT_NE (*cst_int_42, *cst_int_0);
+
+  svalue *uninit = new poisoned_svalue (POISON_KIND_UNINIT);
+  svalue *freed = new poisoned_svalue (POISON_KIND_FREED);
+
+  ASSERT_EQ (uninit->hash (), uninit->hash ());
+  ASSERT_EQ (*uninit, *uninit);
+
+  ASSERT_NE (uninit->hash (), freed->hash ());
+  ASSERT_NE (*uninit, *freed);
+
+  svalue *unknown_0 = new unknown_svalue (ptr_type_node);
+  svalue *unknown_1 = new unknown_svalue (ptr_type_node);
+  ASSERT_EQ (unknown_0->hash (), unknown_0->hash ());
+  ASSERT_EQ (*unknown_0, *unknown_0);
+  ASSERT_EQ (*unknown_1, *unknown_1);
+
+  /* Comparisons between different kinds of svalue.  */
+  ASSERT_NE (*ptr_to_r0, *cst_int_42);
+  ASSERT_NE (*ptr_to_r0, *uninit);
+  ASSERT_NE (*ptr_to_r0, *unknown_0);
+  ASSERT_NE (*cst_int_42, *ptr_to_r0);
+  ASSERT_NE (*cst_int_42, *uninit);
+  ASSERT_NE (*cst_int_42, *unknown_0);
+  ASSERT_NE (*uninit, *ptr_to_r0);
+  ASSERT_NE (*uninit, *cst_int_42);
+  ASSERT_NE (*uninit, *unknown_0);
+  ASSERT_NE (*unknown_0, *ptr_to_r0);
+  ASSERT_NE (*unknown_0, *cst_int_42);
+  ASSERT_NE (*unknown_0, *uninit);
+
+  delete ptr_to_r0;
+  delete ptr_to_r1;
+  delete cst_int_42;
+  delete cst_int_0;
+  delete uninit;
+  delete freed;
+  delete unknown_0;
+  delete unknown_1;
+}
+
+/* Check that operator== and hashing works as expected for the
+   various region subclasses.  */
+
+static void
+test_region_equality ()
+{
+  tree int_42 = build_int_cst (integer_type_node, 42);
+  tree int_0 = build_int_cst (integer_type_node, 0);
+
+  tree x = build_decl (UNKNOWN_LOCATION, VAR_DECL,
+		       get_identifier ("x"),
+		       integer_type_node);
+  tree y = build_decl (UNKNOWN_LOCATION, VAR_DECL,
+		       get_identifier ("y"),
+		       integer_type_node);
+  tree z = build_decl (UNKNOWN_LOCATION, VAR_DECL,
+		       get_identifier ("z"),
+		       integer_type_node);
+  // TODO
+
+  region *r0 = new map_region (region_id::from_int (3), integer_type_node);
+  region *r1 = new map_region (region_id::from_int (4), integer_type_node);
+
+  ASSERT_EQ (*r0, *r0);
+  ASSERT_EQ (r0->hash (), r0->hash ());
+  ASSERT_NE (*r0, *r1);
+  ASSERT_NE (r0->hash (), r1->hash ());
+
+  // TODO: test coverage for the map within a map_region
+
+  delete r0;
+  delete r1;
+}
 
 #if 0
 
@@ -2472,44 +2755,9 @@ test_stack_frames ()
   }
 }
 
-/* Check that operator== and hashing works as expected for the
-   various types.  */
-
-static void
-test_equality ()
-{
-  tree int_42 (build_int_cst (integer_type_node, 42), 0);
-  tree int_0 (build_int_cst (integer_type_node, 0), 0);
-
-  tree x (build_decl (UNKNOWN_LOCATION, VAR_DECL,
-			  get_identifier ("x"),
-			  integer_type_node);
-  tree y (build_decl (UNKNOWN_LOCATION, VAR_DECL,
-			  get_identifier ("y"),
-			  integer_type_node);
-  tree z (build_decl (UNKNOWN_LOCATION, VAR_DECL,
-			  get_identifier ("z"),
-			  integer_type_node);
-
-  {
-    region_model model0;
-    region_model model1;
-
-    ASSERT_EQ (model0.hash (), model1.hash ());
-    ASSERT_EQ (model0, model1);
-
-    ADD_SAT_CONSTRAINT (model1, x, EQ_EXPR, y);
-    ASSERT_NE (model0.hash (), model1.hash ());
-    ASSERT_NE (model0, model1);
-
-    region_model model2;
-    /* Make the same change to model2.  */
-    ADD_SAT_CONSTRAINT (model2, x, EQ_EXPR, y);
-    ASSERT_EQ (model1.hash (), model2.hash ());
-    ASSERT_EQ (model1, model2);
-  }
-}
+#endif
 
+#if 0
 /* A subclass of purge_criteria for selftests: purge all path_var instances.  */
 
 class purge_all_path_vars : public purge_criteria
@@ -2618,10 +2866,11 @@ analyzer_region_model_cc_tests ()
 {
   test_dump ();
   test_unique_constants ();
+  test_svalue_equality ();
+  test_region_equality ();
 #if 0
   test_assignment ();
   test_stack_frames ();
-  test_equality ();
   test_purging ();
 #endif
 }
diff --git a/gcc/analyzer/region-model.h b/gcc/analyzer/region-model.h
index 491bccf..4a954ba 100644
--- a/gcc/analyzer/region-model.h
+++ b/gcc/analyzer/region-model.h
@@ -131,6 +131,7 @@ public:
   virtual ~svalue () {}
 
   bool operator== (const svalue &other) const;
+  bool operator!= (const svalue &other) const { return !(*this == other); }
 
   virtual svalue *clone () const = 0;
 
@@ -175,6 +176,8 @@ class region_svalue : public svalue
 public:
   region_svalue (tree type, region_id rid) : svalue (type), m_rid (rid) {}
 
+  bool compare_fields (const region_svalue &other) const;
+
   svalue *clone () const FINAL OVERRIDE
   { return new region_svalue (get_type (), m_rid); }
 
@@ -209,6 +212,8 @@ public:
   : svalue (TREE_TYPE (cst_expr)), m_cst_expr (cst_expr)
   {}
 
+  bool compare_fields (const constant_svalue &other) const;
+
   svalue *clone () const FINAL OVERRIDE
   { return new constant_svalue (m_cst_expr); }
 
@@ -240,6 +245,8 @@ public:
   : svalue (type)
   {}
 
+  bool compare_fields (const unknown_svalue &other) const;
+
   svalue *clone () const FINAL OVERRIDE
   { return new unknown_svalue (get_type ()); }
 
@@ -274,6 +281,8 @@ class poisoned_svalue : public svalue
 public:
   poisoned_svalue (enum poison_kind kind) : svalue (NULL), m_kind (kind) {}
 
+  bool compare_fields (const poisoned_svalue &other) const;
+
   svalue *clone () const FINAL OVERRIDE
   { return new poisoned_svalue (m_kind); }
 
@@ -327,6 +336,7 @@ public:
   virtual ~region () {}
 
   bool operator== (const region &other) const;
+  bool operator!= (const region &other) const { return !(*this == other); }
 
   virtual region *clone () const = 0;
 
@@ -392,6 +402,8 @@ public:
   {}
   map_region (const map_region &other);
 
+  bool compare_fields (const map_region &other) const;
+
   region *clone () const OVERRIDE;
 
   enum region_kind get_kind () const OVERRIDE { return RK_MAP; }
@@ -439,6 +451,8 @@ public:
   {
   }
 
+  bool compare_fields (const frame_region &other) const;
+
   region *clone () const FINAL OVERRIDE;
 
   enum region_kind get_kind () const FINAL OVERRIDE { return RK_FRAME; }
@@ -467,6 +481,8 @@ public:
 
   stack_region (const stack_region &other);
 
+  bool compare_fields (const stack_region &other) const;
+
   region *clone () const FINAL OVERRIDE;
 
   enum region_kind get_kind () const FINAL OVERRIDE { return RK_STACK; }
@@ -501,6 +517,8 @@ public:
   {}
   heap_region (const heap_region &other);
 
+  bool compare_fields (const heap_region &other) const;
+
   region *clone () const OVERRIDE;
 
   enum region_kind get_kind () const OVERRIDE { return RK_HEAP; }
@@ -516,6 +534,8 @@ public:
   root_region ();
   root_region (const root_region &other);
 
+  bool compare_fields (const root_region &other) const;
+
   region *clone () const FINAL OVERRIDE;
 
   enum region_kind get_kind () const FINAL OVERRIDE { return RK_ROOT; }
@@ -557,6 +577,8 @@ public:
   {}
   symbolic_region (const symbolic_region &other);
 
+  bool compare_fields (const symbolic_region &other) const;
+
   region *clone () const OVERRIDE;
 
   enum region_kind get_kind () const OVERRIDE { return RK_SYMBOLIC; }
@@ -564,25 +586,6 @@ public:
 
 ////////////////////////////////////////////////////////////////////////////
 
-/* FIXME: a very simple implementation of constraints.  */
-
-struct svalue_constraint
-{
-  svalue_constraint (svalue_id lhs, enum tree_code op, svalue_id rhs)
-  : m_lhs (lhs), m_op (op), m_rhs (rhs)
-  {}
-
-  bool operator== (const svalue_constraint &other) const;
-
-  void print (const region_model &model, pretty_printer *pp) const;
-
-  svalue_id m_lhs;
-  enum tree_code m_op;
-  svalue_id m_rhs;
-};
-
-////////////////////////////////////////////////////////////////////////////
-
 /* A region_model encapsulates a representation of the state of memory, with
    a tree of regions, along with their associated values.
    The representation is graph-like because values can be pointers to
@@ -595,6 +598,10 @@ class region_model
   region_model (const region_model &other);
 
   bool operator== (const region_model &other) const;
+  bool operator!= (const region_model &other) const
+  {
+    return !(*this == other);
+  }
 
   hashval_t hash () const;
 
@@ -686,11 +693,7 @@ class region_model
   auto_delete_vec<region> m_regions;
   region_id m_root_rid;
  private:
-#if 1
   constraint_manager *m_constraints; // FIXME: embed, rather than dynalloc?
-#else
-  auto_vec<svalue_constraint> m_constraints; // TODO hash, copy-ctor, etc
-#endif
 };
 
 namespace inchash
diff --git a/gcc/common.opt b/gcc/common.opt
index 432e631..19f54d7 100644
--- a/gcc/common.opt
+++ b/gcc/common.opt
@@ -565,7 +565,7 @@ Wanalyzer-malloc-leak
 Common Init(1) Warning
 FIXME
 
-Wanalyzer-null-dereference
+Wanalyzer-possible-null-argument
 Common Init(1) Warning
 FIXME
 
@@ -573,6 +573,14 @@ Wanalyzer-possible-null-dereference
 Common Init(1) Warning
 FIXME
 
+Wanalyzer-null-argument
+Common Init(1) Warning
+FIXME
+
+Wanalyzer-null-dereference
+Common Init(1) Warning
+FIXME
+
 Wanalyzer-tainted-array-index
 Common Init(1) Warning
 FIXME
diff --git a/gcc/testsuite/gcc.dg/TODO-analyzer/checkers/malloc-checker/arg_must_not_be_null/input.c b/gcc/testsuite/gcc.dg/TODO-analyzer/checkers/malloc-checker/arg_must_not_be_null/input.c
deleted file mode 100644
index 141e55c..0000000
--- a/gcc/testsuite/gcc.dg/TODO-analyzer/checkers/malloc-checker/arg_must_not_be_null/input.c
+++ /dev/null
@@ -1,30 +0,0 @@
-/*
-   Copyright 2013 David Malcolm <dmalcolm@redhat.com>
-   Copyright 2013 Red Hat, Inc.
-
-   This 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 of the License, or
-   (at your option) any later version.
-
-   This program 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 this program.  If not, see
-   <http://www.gnu.org/licenses/>.
-*/
-
-#include <stdlib.h>
-
-extern void foo(void *ptrA, void *ptrB, void *ptrC)
-  __attribute__((nonnull (1, 3)));
-
-void test(void *p, void *q, void *r)
-{
-  p = NULL;
-
-  foo(p, q, r);
-}
diff --git a/gcc/testsuite/gcc.dg/TODO-analyzer/checkers/malloc-checker/arg_must_not_be_null/script.py b/gcc/testsuite/gcc.dg/TODO-analyzer/checkers/malloc-checker/arg_must_not_be_null/script.py
deleted file mode 100644
index d6390c5..0000000
--- a/gcc/testsuite/gcc.dg/TODO-analyzer/checkers/malloc-checker/arg_must_not_be_null/script.py
+++ /dev/null
@@ -1,23 +0,0 @@
-# -*- coding: utf-8 -*-
-#   Copyright 2012 David Malcolm <dmalcolm@redhat.com>
-#   Copyright 2012 Red Hat, Inc.
-#
-#   This 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 of the License, or
-#   (at your option) any later version.
-#
-#   This program 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 this program.  If not, see
-#   <http://www.gnu.org/licenses/>.
-
-from sm import main
-from sm.parser import parse_file
-
-checker = parse_file('sm/checkers/malloc_checker.sm')
-main([checker])
diff --git a/gcc/testsuite/gcc.dg/TODO-analyzer/checkers/malloc-checker/arg_must_not_be_null/stderr.txt b/gcc/testsuite/gcc.dg/TODO-analyzer/checkers/malloc-checker/arg_must_not_be_null/stderr.txt
deleted file mode 100644
index cc5466f..0000000
--- a/gcc/testsuite/gcc.dg/TODO-analyzer/checkers/malloc-checker/arg_must_not_be_null/stderr.txt
+++ /dev/null
@@ -1,4 +0,0 @@
-tests/sm/checkers/malloc-checker/arg_must_not_be_null/input.c: In function 'test':
-tests/sm/checkers/malloc-checker/arg_must_not_be_null/input.c:29:nn: error: NULL pointer p passed as argument 1 to foo [CWE-690]
-tests/sm/checkers/malloc-checker/arg_must_not_be_null/input.c:27:nn: note: p assigned to 0
-tests/sm/checkers/malloc-checker/arg_must_not_be_null/input.c:29:nn: note: NULL pointer p passed as argument 1 to foo
diff --git a/gcc/testsuite/gcc.dg/TODO-analyzer/checkers/malloc-checker/arg_must_not_be_null/stdout.txt b/gcc/testsuite/gcc.dg/TODO-analyzer/checkers/malloc-checker/arg_must_not_be_null/stdout.txt
deleted file mode 100644
index e69de29..0000000
diff --git a/gcc/testsuite/gcc.dg/TODO-analyzer/checkers/malloc-checker/double_free/input.c b/gcc/testsuite/gcc.dg/TODO-analyzer/checkers/malloc-checker/double_free/input.c
deleted file mode 100644
index 56385c3..0000000
--- a/gcc/testsuite/gcc.dg/TODO-analyzer/checkers/malloc-checker/double_free/input.c
+++ /dev/null
@@ -1,29 +0,0 @@
-/*
-   Copyright 2012 David Malcolm <dmalcolm@redhat.com>
-   Copyright 2012 Red Hat, Inc.
-
-   This 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 of the License, or
-   (at your option) any later version.
-
-   This program 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 this program.  If not, see
-   <http://www.gnu.org/licenses/>.
-*/
-
-#include <stdlib.h>
-#include <string.h>
-
-void test(void *ptr)
-{
-  free(ptr);
-
-  /* BUG: double-free: */
-  free(ptr);
-}
diff --git a/gcc/testsuite/gcc.dg/TODO-analyzer/checkers/malloc-checker/double_free/input.c.cpychecker-log.txt b/gcc/testsuite/gcc.dg/TODO-analyzer/checkers/malloc-checker/double_free/input.c.cpychecker-log.txt
deleted file mode 100644
index 7499d84..0000000
--- a/gcc/testsuite/gcc.dg/TODO-analyzer/checkers/malloc-checker/double_free/input.c.cpychecker-log.txt
+++ /dev/null
@@ -1 +0,0 @@
-gcc.Function('test')
diff --git a/gcc/testsuite/gcc.dg/TODO-analyzer/checkers/malloc-checker/double_free/script.py b/gcc/testsuite/gcc.dg/TODO-analyzer/checkers/malloc-checker/double_free/script.py
deleted file mode 100644
index d6390c5..0000000
--- a/gcc/testsuite/gcc.dg/TODO-analyzer/checkers/malloc-checker/double_free/script.py
+++ /dev/null
@@ -1,23 +0,0 @@
-# -*- coding: utf-8 -*-
-#   Copyright 2012 David Malcolm <dmalcolm@redhat.com>
-#   Copyright 2012 Red Hat, Inc.
-#
-#   This 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 of the License, or
-#   (at your option) any later version.
-#
-#   This program 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 this program.  If not, see
-#   <http://www.gnu.org/licenses/>.
-
-from sm import main
-from sm.parser import parse_file
-
-checker = parse_file('sm/checkers/malloc_checker.sm')
-main([checker])
diff --git a/gcc/testsuite/gcc.dg/TODO-analyzer/checkers/malloc-checker/double_free/stderr.txt b/gcc/testsuite/gcc.dg/TODO-analyzer/checkers/malloc-checker/double_free/stderr.txt
deleted file mode 100644
index 6bdd7a2..0000000
--- a/gcc/testsuite/gcc.dg/TODO-analyzer/checkers/malloc-checker/double_free/stderr.txt
+++ /dev/null
@@ -1,7 +0,0 @@
-tests/sm/checkers/malloc-checker/double_free/input.c: In function 'test':
-tests/sm/checkers/malloc-checker/double_free/input.c:28:nn: error: double-free of ptr [CWE-415]
-tests/sm/checkers/malloc-checker/double_free/input.c:25:nn: note: ptr passed to free()
-tests/sm/checkers/malloc-checker/double_free/input.c:28:nn: note: double-free of ptr
-tests/sm/checkers/malloc-checker/double_free/input.c:28:nn: error: use-after-free of ptr [CWE-416]
-tests/sm/checkers/malloc-checker/double_free/input.c:25:nn: note: ptr passed to free()
-tests/sm/checkers/malloc-checker/double_free/input.c:28:nn: note: use-after-free of ptr
diff --git a/gcc/testsuite/gcc.dg/TODO-analyzer/checkers/malloc-checker/double_free/stdout.txt b/gcc/testsuite/gcc.dg/TODO-analyzer/checkers/malloc-checker/double_free/stdout.txt
deleted file mode 100644
index e69de29..0000000
diff --git a/gcc/testsuite/gcc.dg/TODO-analyzer/checkers/signal_handler/example/stderr.txt b/gcc/testsuite/gcc.dg/TODO-analyzer/checkers/signal_handler/example/stderr.txt
deleted file mode 100644
index 55b4ce0..0000000
--- a/gcc/testsuite/gcc.dg/TODO-analyzer/checkers/signal_handler/example/stderr.txt
+++ /dev/null
@@ -1,5 +0,0 @@
-tests/sm/checkers/points_to_stack/return_of_ptr_to_local/input.c: In function 'test':
-tests/sm/checkers/points_to_stack/return_of_ptr_to_local/input.c:41:nn: error: return of "result" returns address within stack of local variable "buffer" [CWE-562]
-tests/sm/checkers/points_to_stack/return_of_ptr_to_local/input.c:38:nn: note: assignment of result to &buffer
-tests/sm/checkers/points_to_stack/return_of_ptr_to_local/input.c:41:nn: note: state of result ("State('ptr.points_to_stack', 'var_pointed_to'=gcc.VarDecl('buffer'))") propagated to result
-tests/sm/checkers/points_to_stack/return_of_ptr_to_local/input.c:41:nn: note: return of "result" returns address within stack of local variable "buffer"
diff --git a/gcc/testsuite/gcc.dg/TODO-analyzer/checkers/signal_handler/example/stdout.txt b/gcc/testsuite/gcc.dg/TODO-analyzer/checkers/signal_handler/example/stdout.txt
deleted file mode 100644
index e69de29..0000000
diff --git a/gcc/testsuite/gcc.dg/TODO-analyzer/regression/rhs-is-vardecl/stdout.txt b/gcc/testsuite/gcc.dg/TODO-analyzer/regression/rhs-is-vardecl/stdout.txt
deleted file mode 100644
index e69de29..0000000
diff --git a/gcc/testsuite/gcc.dg/analyzer/attribute-nonnull.c b/gcc/testsuite/gcc.dg/analyzer/attribute-nonnull.c
new file mode 100644
index 0000000..ab44d07
--- /dev/null
+++ b/gcc/testsuite/gcc.dg/analyzer/attribute-nonnull.c
@@ -0,0 +1,57 @@
+#include <stdlib.h>
+
+extern void foo(void *ptrA, void *ptrB, void *ptrC) /* { dg-message "argument 1 of 'foo' must be non-null" } */
+  __attribute__((nonnull (1, 3)));
+
+extern void bar(void *ptrA, void *ptrB, void *ptrC) /* { dg-message "argument 1 of 'bar' must be non-null" } */
+  __attribute__((nonnull));
+
+// TODO: complain about NULL and possible NULL args
+// FIXME: ought to complain about NULL args
+
+void test_1 (void *p, void *q, void *r)
+{
+  foo(p, q, r);
+  foo(NULL, q, r);
+  foo(p, NULL, r);
+  foo(p, q, NULL);
+}
+
+void test_1a (void *q, void *r)
+{
+  void *p = NULL;
+  foo(p, q, r); /* { dg-warning "use of NULL 'p' where non-null expected" } */
+  /* { dg-message "argument 1 \\('p'\\) NULL where non-null expected" "" { target *-*-* } .-1 } */
+}
+
+void test_2 (void *p, void *q, void *r)
+{
+  bar(p, q, r);
+  bar(NULL, q, r);
+  bar(p, NULL, r);
+  bar(p, q, NULL);
+}
+
+void test_3 (void *q, void *r)
+{
+  void *p = malloc(1024); /* { dg-message "this call could return NULL" } */
+
+  foo(p, q, r); /* { dg-warning "use of possibly-NULL 'p' where non-null expected" } */
+  /* { dg-message "argument 1 \\('p'\\) could be NULL where non-null expected" "" { target *-*-* } .-1 } */
+
+  foo(p, q, r);
+
+  free(p);
+}
+
+void test_4 (void *q, void *r)
+{
+  void *p = malloc(1024); /* { dg-message "this call could return NULL" } */
+
+  bar(p, q, r); /* { dg-warning "use of possibly-NULL 'p' where non-null expected" } */
+  /* { dg-message "argument 1 \\('p'\\) could be NULL where non-null expected" "" { target *-*-* } .-1 } */
+
+  bar(p, q, r);
+
+  free(p);
+}
diff --git a/gcc/testsuite/gcc.dg/analyzer/data-model-1.c b/gcc/testsuite/gcc.dg/analyzer/data-model-1.c
index 8da8a48..14543a9 100644
--- a/gcc/testsuite/gcc.dg/analyzer/data-model-1.c
+++ b/gcc/testsuite/gcc.dg/analyzer/data-model-1.c
@@ -493,7 +493,7 @@ void test_25 (struct foo *f)
 
   /* Overwriting a whole struct where we know things about the
      source value should update our knowledge about fields within
-     the dest value.  */     
+     the dest value.  */
   g = *f;
   __analyzer_eval (g.i == 43); /* { dg-warning "TRUE" "" { xfail *-*-* } } */
   /* { dg-warning "FALSE" "" { target *-*-* } .-1 } */
@@ -511,14 +511,14 @@ void test_26 (struct coord *p, struct coord *q)
 
   /* Overwriting a whole struct where we know some things about the
      source value should update our knowledge about fields within
-     the dest value.  */     
+     the dest value.  */
   *p = *q;
   __analyzer_eval (p->x); /* { dg-warning "UNKNOWN" "" { xfail *-*-* } } */
   /* { dg-warning "TRUE" "" { target *-*-* } .-1 } */
   // TODO(xfail): should have been overwritten
   __analyzer_eval (p->y == 17); /* { dg-warning "TRUE" "" { xfail *-*-* } } */
   /* { dg-warning "UNKNOWN" "" { target *-*-* } .-1 } */
-  // TODO(xfail): should have been overwritten with q->y 
+  // TODO(xfail): should have been overwritten with q->y
 
   __analyzer_eval (q->x); /* { dg-warning "UNKNOWN" } */
   __analyzer_eval (q->y == 17); /* { dg-warning "TRUE" } */
@@ -771,6 +771,8 @@ union u
    - globals
    - memcpy, memmove, bcopy, memccpy, meppcpy, strcpy, etc from <string.h>
    - loops
+     - known bound
+     - unknown bound
    - goto
    - third-party libraries
    - recursive functions
@@ -782,5 +784,7 @@ union u
    - int <-> float conversions
    - other casts
    - try it on a bunch of real-world code
+   - setjmp/longjmp
+   - function pointers
    - C++
    etc.  */
diff --git a/gcc/testsuite/gcc.dg/analyzer/malloc-vs-local.c b/gcc/testsuite/gcc.dg/analyzer/malloc-vs-local.c
new file mode 100644
index 0000000..d4d8557
--- /dev/null
+++ b/gcc/testsuite/gcc.dg/analyzer/malloc-vs-local.c
@@ -0,0 +1,83 @@
+#include <stdlib.h>
+
+extern int foo (int);
+
+static int do_stuff (int *p, int n)
+{
+  int sum = 0;
+  int i;
+  for (i = 0; i < n; i++)
+    p[i] = i;
+  for (i = 0; i < n; i++)
+    sum += foo (p[i]);
+  return sum;
+}
+
+/* Various examples of functions that use either a malloc buffer
+   or a local buffer, do something, then conditionally free the
+   buffer, tracking whether "free" is necessary in various
+   ways.  */
+
+#if 0
+int test_repeated_predicate (int n)
+{
+  int buf[10];
+  int *ptr;
+  int result;
+
+  if (n > 10)
+    ptr = (int *)malloc (sizeof (int) * n);
+  else
+    ptr = buf;
+
+  result = do_stuff (ptr, n);
+
+  if (n > 10)
+    free (ptr);
+
+  return result;
+}
+
+int test_explicit_flag (int n)
+{
+  int buf[10];
+  int *ptr;
+  int result;
+  int need_to_free = 0;
+
+  if (n > 10)
+    {
+      ptr = (int *)malloc (sizeof (int) * n);
+      need_to_free = 1;
+    }
+  else
+    ptr = buf;
+
+  result = do_stuff (ptr, n);
+
+  if (need_to_free)
+    free (ptr);
+
+  return result;
+}
+
+// TODO: currently this leads to an ICE:
+int test_pointer_comparison (int n)
+{
+  int buf[10];
+  int *ptr;
+  int result;
+
+  if (n > 10)
+    ptr = (int *)malloc (sizeof (int) * n);
+  else
+    ptr = buf;
+
+  result = do_stuff (ptr, n);
+
+  if (ptr != buf)
+    free (ptr);
+
+  return result;
+}
+#endif
diff --git a/gcc/testsuite/gcc.dg/analyzer/pragma-1.c b/gcc/testsuite/gcc.dg/analyzer/pragma-1.c
new file mode 100644
index 0000000..56abb84
--- /dev/null
+++ b/gcc/testsuite/gcc.dg/analyzer/pragma-1.c
@@ -0,0 +1,26 @@
+/* Verify that we can disable analyzer warnings via pragmas.  */
+
+#include <stdlib.h>
+
+void test_1 (void *ptr)
+{
+  free (ptr);
+  free (ptr); /* { dg-warning "double-free" } */
+}
+
+void test_2 (void *ptr)
+{
+  _Pragma("GCC diagnostic push")
+  _Pragma("GCC diagnostic ignored \"-Wanalyzer-double-free\"")
+
+  free (ptr);
+  free (ptr);  /* { dg-bogus "double-free" } */
+
+  _Pragma("GCC diagnostic pop")
+}
+
+void test_3 (void *ptr)
+{
+  free (ptr);
+  free (ptr);  /* { dg-warning "double-free" } */
+}
-- 
1.8.5.3

