diff --git a/src/pointer-analysis/Makefile b/src/pointer-analysis/Makefile
index 6df993586b8..95df6698b23 100644
--- a/src/pointer-analysis/Makefile
+++ b/src/pointer-analysis/Makefile
@@ -1,6 +1,6 @@
 SRC = value_set.cpp goto_program_dereference.cpp value_set_analysis.cpp \
       dereference.cpp pointer_offset_sum.cpp add_failed_symbols.cpp \
-      show_value_sets.cpp value_set_domain.cpp rewrite_index.cpp \
+      show_value_sets.cpp rewrite_index.cpp \
       value_set_analysis_fi.cpp value_set_fi.cpp value_set_domain_fi.cpp \
       value_set_analysis_fivr.cpp value_set_fivr.cpp value_set_domain_fivr.cpp \
       value_set_analysis_fivrns.cpp value_set_fivrns.cpp \
diff --git a/src/pointer-analysis/show_value_sets.h b/src/pointer-analysis/show_value_sets.h
index b98acbacd93..a33e6976562 100644
--- a/src/pointer-analysis/show_value_sets.h
+++ b/src/pointer-analysis/show_value_sets.h
@@ -10,10 +10,10 @@ Author: Daniel Kroening, kroening@kroening.com
 #define CPROVER_POINTER_ANALYSIS_SHOW_VALUE_SETS_H
 
 #include <util/ui_message.h>
+#include "value_set_analysis.h"
 
 class goto_functionst;
 class goto_programt;
-class value_set_analysist;
 
 void show_value_sets(
   ui_message_handlert::uit ui,
diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp
index 629a25509d6..719cadd386f 100644
--- a/src/pointer-analysis/value_set.cpp
+++ b/src/pointer-analysis/value_set.cpp
@@ -1064,6 +1064,53 @@ void value_sett::get_reference_set(
 
 /*******************************************************************\
 
+Function: strip_casts
+
+  Inputs: `e`: expression to strip
+          `ns`: global namespace
+          `target_type_raw`: if in the course of stripping casts we
+            end up at an expression with this type, stop stripping.
+
+ Outputs: Side-effect on `e`: remove typecasts and address-of-first-
+          struct-member expressions until either we find an underlying
+          expression of type `target_type_raw`, or we run out of
+          strippable expressions.
+
+ Purpose: Cleanly cast `e` to a given type if possible, avoiding the
+          possibility of ever-expanding towers of typecasts (either
+          explict or via taking address of first member).
+
+\*******************************************************************/
+
+static void strip_casts(
+  exprt &e,
+  const namespacet &ns,
+  const typet &target_type_raw)
+{
+  const auto &target_type=ns.follow(target_type_raw);
+  while(true)
+  {
+    if(e.id()==ID_typecast)
+      e=e.op0();
+    else if(e.id()==ID_member)
+    {
+      auto &mem=to_member_expr(e);
+      const auto &struct_type=to_struct_type(ns.follow(e.op0().type()));
+      if(mem.get_component_name()==struct_type.components()[0].get_name())
+        e=e.op0();
+      else
+        return;
+    }
+    else
+      return;
+
+    if(ns.follow(e.type())==target_type)
+      return;
+  }
+}
+
+/*******************************************************************\
+
 Function: value_sett::get_reference_set_rec
 
   Inputs:
@@ -1208,7 +1255,13 @@ void value_sett::get_reference_set_rec(
         {
           // adjust type?
           if(ns.follow(struct_op.type())!=final_object_type)
+          {
+            // Avoid an infinite loop of casting by stripping typecasts
+            // and address-of-first-members first.
+            strip_casts(member_expr.op0(), ns, struct_op.type());
+            if(ns.follow(member_expr.op0().type())!=ns.follow(struct_op.type()))
             member_expr.op0().make_typecast(struct_op.type());
+          }
 
           insert(dest, member_expr, o);
         }
@@ -1492,7 +1545,6 @@ void value_sett::assign_rec(
   if(lhs.id()==ID_symbol)
   {
     const irep_idt &identifier=to_symbol_expr(lhs).get_identifier();
-
     entryt &e=get_entry(entryt(identifier, suffix), lhs.type(), ns);
 
     if(add_to_sets)
diff --git a/src/pointer-analysis/value_set.h b/src/pointer-analysis/value_set.h
index 486b55e998b..94ed55febb7 100644
--- a/src/pointer-analysis/value_set.h
+++ b/src/pointer-analysis/value_set.h
@@ -32,6 +32,7 @@ class value_sett
     const namespacet &);
 
   unsigned location_number;
+  irep_idt function;
   static object_numberingt object_numbering;
 
   typedef irep_idt idt;
@@ -101,7 +102,7 @@ class value_sett
     object_mapt object_map;
     idt identifier;
     std::string suffix;
-
+    typet declared_on_type;
     entryt()
     {
     }
@@ -111,6 +112,16 @@ class value_sett
       suffix(_suffix)
     {
     }
+
+    entryt(
+      const idt &_identifier,
+      const std::string &_suffix,
+      const typet &_declared_on_type):
+      identifier(_identifier),
+      suffix(_suffix),
+      declared_on_type(_declared_on_type)
+    {
+    }
   };
 
   typedef std::set<exprt> expr_sett;
@@ -166,11 +177,11 @@ class value_sett
     const exprt &expr,
     const namespacet &ns);
 
-  void apply_code(
+  virtual void apply_code(
     const codet &code,
     const namespacet &ns);
 
-  void assign(
+  virtual void assign(
     const exprt &lhs,
     const exprt &rhs,
     const namespacet &ns,
@@ -197,20 +208,20 @@ class value_sett
     const namespacet &ns) const;
 
 protected:
-  void get_value_set_rec(
+  virtual void get_value_set_rec(
     const exprt &expr,
     object_mapt &dest,
     const std::string &suffix,
     const typet &original_type,
     const namespacet &ns) const;
 
-  void get_value_set(
+  virtual void get_value_set(
     const exprt &expr,
     object_mapt &dest,
     const namespacet &ns,
     bool is_simplified) const;
 
-  void get_reference_set(
+  virtual void get_reference_set(
     const exprt &expr,
     object_mapt &dest,
     const namespacet &ns) const
@@ -218,16 +229,16 @@ class value_sett
     get_reference_set_rec(expr, dest, ns);
   }
 
-  void get_reference_set_rec(
+  virtual void get_reference_set_rec(
     const exprt &expr,
     object_mapt &dest,
     const namespacet &ns) const;
 
-  void dereference_rec(
+  virtual void dereference_rec(
     const exprt &src,
     exprt &dest) const;
 
-  void assign_rec(
+  virtual void assign_rec(
     const exprt &lhs,
     const object_mapt &values_rhs,
     const std::string &suffix,
diff --git a/src/pointer-analysis/value_set_analysis.cpp b/src/pointer-analysis/value_set_analysis.cpp
index 4e98c10aee4..6dd8fff785e 100644
--- a/src/pointer-analysis/value_set_analysis.cpp
+++ b/src/pointer-analysis/value_set_analysis.cpp
@@ -8,8 +8,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/prefix.h>
 #include <util/cprover_prefix.h>
-#include <util/xml_expr.h>
-#include <util/xml.h>
 
 #include <langapi/language_util.h>
 
@@ -17,105 +15,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 /*******************************************************************\
 
-Function: value_set_analysist::initialize
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-void value_set_analysist::initialize(
-  const goto_programt &goto_program)
-{
-  baset::initialize(goto_program);
-}
-
-/*******************************************************************\
-
-Function: value_set_analysist::initialize
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-void value_set_analysist::initialize(
-  const goto_functionst &goto_functions)
-{
-  baset::initialize(goto_functions);
-}
-
-/*******************************************************************\
-
-Function: value_set_analysist::convert
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-void value_set_analysist::convert(
-  const goto_programt &goto_program,
-  const irep_idt &identifier,
-  xmlt &dest) const
-{
-  source_locationt previous_location;
-
-  forall_goto_program_instructions(i_it, goto_program)
-  {
-    const source_locationt &location=i_it->source_location;
-
-    if(location==previous_location)
-      continue;
-
-    if(location.is_nil() || location.get_file()==irep_idt())
-      continue;
-
-    // find value set
-    const value_sett &value_set=(*this)[i_it].value_set;
-
-    xmlt &i=dest.new_element("instruction");
-    i.new_element()=::xml(location);
-
-    for(value_sett::valuest::const_iterator
-        v_it=value_set.values.begin();
-        v_it!=value_set.values.end();
-        v_it++)
-    {
-      xmlt &var=i.new_element("variable");
-      var.new_element("identifier").data=
-        id2string(v_it->first);
-
-      #if 0
-      const value_sett::expr_sett &expr_set=
-        v_it->second.expr_set();
-
-      for(value_sett::expr_sett::const_iterator
-          e_it=expr_set.begin();
-          e_it!=expr_set.end();
-          e_it++)
-      {
-        std::string value_str=
-          from_expr(ns, identifier, *e_it);
-
-        var.new_element("value").data=
-          xmlt::escape(value_str);
-      }
-      #endif
-    }
-  }
-}
-/*******************************************************************\
-
 Function: convert
 
   Inputs:
diff --git a/src/pointer-analysis/value_set_analysis.h b/src/pointer-analysis/value_set_analysis.h
index 3437b34af2c..67179de3985 100644
--- a/src/pointer-analysis/value_set_analysis.h
+++ b/src/pointer-analysis/value_set_analysis.h
@@ -11,32 +11,90 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #define USE_DEPRECATED_STATIC_ANALYSIS_H
 #include <analyses/static_analysis.h>
+#include <util/xml_expr.h>
+#include <util/xml.h>
 
 #include "value_set_domain.h"
 #include "value_sets.h"
+#include "value_set.h"
 
 class xmlt;
 
-class value_set_analysist:
+template<class Value_Sett>
+class value_set_analysis_baset:
   public value_setst,
-  public static_analysist<value_set_domaint>
+  public static_analysist<value_set_domaint<Value_Sett> >
 {
 public:
-  explicit value_set_analysist(const namespacet &_ns):
-    static_analysist<value_set_domaint>(_ns)
+  typedef value_set_domaint<Value_Sett> domaint;
+  typedef static_analysist<domaint> baset;
+  typedef typename baset::locationt locationt;
+
+  explicit value_set_analysis_baset(const namespacet &_ns):baset(_ns)
   {
   }
 
-  typedef static_analysist<value_set_domaint> baset;
-
   // overloading
-  virtual void initialize(const goto_programt &goto_program);
-  virtual void initialize(const goto_functionst &goto_functions);
+  void initialize(const goto_programt &goto_program)
+  {
+    baset::initialize(goto_program);
+  }
+  void initialize(const goto_functionst &goto_functions)
+  {
+    baset::initialize(goto_functions);
+  }
 
   void convert(
     const goto_programt &goto_program,
     const irep_idt &identifier,
-    xmlt &dest) const;
+    xmlt &dest) const
+  {
+    source_locationt previous_location;
+
+    forall_goto_program_instructions(i_it, goto_program)
+    {
+      const source_locationt &location=i_it->source_location;
+
+      if(location==previous_location)
+        continue;
+
+      if(location.is_nil() || location.get_file()==irep_idt())
+        continue;
+
+      // find value set
+      const value_sett &value_set=(*this)[i_it].value_set;
+
+      xmlt &i=dest.new_element("instruction");
+      i.new_element()=::xml(location);
+
+      for(value_sett::valuest::const_iterator
+            v_it=value_set.values.begin();
+          v_it!=value_set.values.end();
+          v_it++)
+      {
+        xmlt &var=i.new_element("variable");
+        var.new_element("identifier").data=
+          id2string(v_it->first);
+
+#if 0
+        const value_sett::expr_sett &expr_set=
+          v_it->second.expr_set();
+
+        for(value_sett::expr_sett::const_iterator
+              e_it=expr_set.begin();
+            e_it!=expr_set.end();
+            e_it++)
+        {
+          std::string value_str=
+            from_expr(ns, identifier, *e_it);
+
+          var.new_element("value").data=
+            xmlt::escape(value_str);
+        }
+#endif
+      }
+    }
+  }
 
 public:
   // interface value_sets
@@ -45,10 +103,12 @@ class value_set_analysist:
     const exprt &expr,
     value_setst::valuest &dest)
   {
-    (*this)[l].value_set.get_value_set(expr, dest, ns);
+    (*this)[l].value_set.get_value_set(expr, dest, baset::ns);
   }
 };
 
+typedef value_set_analysis_baset<value_sett> value_set_analysist;
+
 void convert(
   const goto_functionst &goto_functions,
   const value_set_analysist &value_set_analysis,
diff --git a/src/pointer-analysis/value_set_domain.cpp b/src/pointer-analysis/value_set_domain.cpp
deleted file mode 100644
index 74656d23fe6..00000000000
--- a/src/pointer-analysis/value_set_domain.cpp
+++ /dev/null
@@ -1,65 +0,0 @@
-/*******************************************************************\
-
-Module: Value Set
-
-Author: Daniel Kroening, kroening@kroening.com
-
-\*******************************************************************/
-
-#include <util/std_code.h>
-
-#include "value_set_domain.h"
-
-/*******************************************************************\
-
-Function: value_set_domaint::transform
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-void value_set_domaint::transform(
-  const namespacet &ns,
-  locationt from_l,
-  locationt to_l)
-{
-  switch(from_l->type)
-  {
-  case GOTO:
-    // ignore for now
-    break;
-
-  case END_FUNCTION:
-    value_set.do_end_function(static_analysis_baset::get_return_lhs(to_l), ns);
-    break;
-
-  case RETURN:
-  case OTHER:
-  case ASSIGN:
-  case DECL:
-    value_set.apply_code(from_l->code, ns);
-    break;
-
-  case ASSUME:
-    value_set.guard(from_l->guard, ns);
-    break;
-
-  case FUNCTION_CALL:
-    {
-      const code_function_callt &code=
-        to_code_function_call(from_l->code);
-
-      value_set.do_function_call(to_l->function, code.arguments(), ns);
-    }
-    break;
-
-  default:
-    {
-      // do nothing
-    }
-  }
-}
diff --git a/src/pointer-analysis/value_set_domain.h b/src/pointer-analysis/value_set_domain.h
index df028b0d4e1..c1aeacf7811 100644
--- a/src/pointer-analysis/value_set_domain.h
+++ b/src/pointer-analysis/value_set_domain.h
@@ -14,10 +14,11 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "value_set.h"
 
+template<class Value_Sett>
 class value_set_domaint:public domain_baset
 {
 public:
-  value_sett value_set;
+  Value_Sett value_set;
 
   // overloading
 
@@ -39,13 +40,9 @@ class value_set_domaint:public domain_baset
   {
     value_set.clear();
     value_set.location_number=l->location_number;
+    value_set.function=l->function;
   }
 
-  virtual void transform(
-    const namespacet &ns,
-    locationt from_l,
-    locationt to_l);
-
   virtual void get_reference_set(
     const namespacet &ns,
     const exprt &expr,
@@ -53,6 +50,51 @@ class value_set_domaint:public domain_baset
   {
     value_set.get_reference_set(expr, dest, ns);
   }
+
+  virtual void transform(
+    const namespacet &ns,
+    locationt from_l,
+    locationt to_l)
+  {
+    switch(from_l->type)
+    {
+    case GOTO:
+      // ignore for now
+      break;
+
+    case END_FUNCTION:
+      value_set.do_end_function(
+        static_analysis_baset::get_return_lhs(to_l),
+        ns);
+      break;
+
+    case RETURN:
+    case OTHER:
+    case ASSIGN:
+    case DECL:
+    case DEAD:
+      value_set.apply_code(from_l->code, ns);
+      break;
+
+    case ASSUME:
+      value_set.guard(from_l->guard, ns);
+      break;
+
+    case FUNCTION_CALL:
+      {
+        const code_function_callt &code=
+          to_code_function_call(from_l->code);
+
+        value_set.do_function_call(to_l->function, code.arguments(), ns);
+      }
+    break;
+
+    default:
+      {
+        // do nothing
+      }
+    }
+  }
 };
 
 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_DOMAIN_H