diff --git a/regression/cbmc-java/instance-method-user-interface-field/A.class b/regression/cbmc-java/instance-method-user-interface-field/A.class
new file mode 100644
index 00000000000..86d25a78c28
Binary files /dev/null and b/regression/cbmc-java/instance-method-user-interface-field/A.class differ
diff --git a/regression/cbmc-java/instance-method-user-interface-field/B.class b/regression/cbmc-java/instance-method-user-interface-field/B.class
new file mode 100644
index 00000000000..09103c22aac
Binary files /dev/null and b/regression/cbmc-java/instance-method-user-interface-field/B.class differ
diff --git a/regression/cbmc-java/instance-method-user-interface-field/I.class b/regression/cbmc-java/instance-method-user-interface-field/I.class
new file mode 100644
index 00000000000..ad5d429af3b
Binary files /dev/null and b/regression/cbmc-java/instance-method-user-interface-field/I.class differ
diff --git a/regression/cbmc-java/instance-method-user-interface-field/TestClass.class b/regression/cbmc-java/instance-method-user-interface-field/TestClass.class
new file mode 100644
index 00000000000..6a6298d05b8
Binary files /dev/null and b/regression/cbmc-java/instance-method-user-interface-field/TestClass.class differ
diff --git a/regression/cbmc-java/instance-method-user-interface-field/TestClass.java b/regression/cbmc-java/instance-method-user-interface-field/TestClass.java
new file mode 100644
index 00000000000..0065a473c57
--- /dev/null
+++ b/regression/cbmc-java/instance-method-user-interface-field/TestClass.java
@@ -0,0 +1,44 @@
+interface I
+{
+    int getANumber();
+}
+
+class A implements I {
+    public int a;
+
+    public int getANumber() { return a; }
+}
+
+class B implements I {
+    public int b;
+    public int getANumber() { return b; }
+}
+
+class TestClass
+{
+    public I someObject;
+
+    public boolean foo() {
+        if(someObject!=null)
+        {
+            int result = someObject.getANumber();
+            if(result == 42) {
+                return true;
+            } else {
+                return false;
+            }
+        }
+        else
+        {
+            return false;
+        }
+    }
+
+    public static void main(String[] args)
+    {
+        // ensure that A, B are referenced explicitly
+        // in order to get them converted into GOTO
+        A a = new A();
+        B b = new B();
+    }
+}
diff --git a/regression/cbmc-java/instance-method-user-interface-field/test.desc b/regression/cbmc-java/instance-method-user-interface-field/test.desc
new file mode 100644
index 00000000000..da1f8c687ee
--- /dev/null
+++ b/regression/cbmc-java/instance-method-user-interface-field/test.desc
@@ -0,0 +1,5 @@
+CORE
+TestClass.class
+--cover location --function TestClass.foo --show-goto-functions
+\.someObject = \(struct I \*\)\w+
+@class_identifier = "java::A";
diff --git a/regression/cbmc-java/instance-method-user-interface-two-fields-different/A.class b/regression/cbmc-java/instance-method-user-interface-two-fields-different/A.class
new file mode 100644
index 00000000000..86d25a78c28
Binary files /dev/null and b/regression/cbmc-java/instance-method-user-interface-two-fields-different/A.class differ
diff --git a/regression/cbmc-java/instance-method-user-interface-two-fields-different/B.class b/regression/cbmc-java/instance-method-user-interface-two-fields-different/B.class
new file mode 100644
index 00000000000..09103c22aac
Binary files /dev/null and b/regression/cbmc-java/instance-method-user-interface-two-fields-different/B.class differ
diff --git a/regression/cbmc-java/instance-method-user-interface-two-fields-different/C.class b/regression/cbmc-java/instance-method-user-interface-two-fields-different/C.class
new file mode 100644
index 00000000000..ee05ffe5f45
Binary files /dev/null and b/regression/cbmc-java/instance-method-user-interface-two-fields-different/C.class differ
diff --git a/regression/cbmc-java/instance-method-user-interface-two-fields-different/D.class b/regression/cbmc-java/instance-method-user-interface-two-fields-different/D.class
new file mode 100644
index 00000000000..916313b41a4
Binary files /dev/null and b/regression/cbmc-java/instance-method-user-interface-two-fields-different/D.class differ
diff --git a/regression/cbmc-java/instance-method-user-interface-two-fields-different/I.class b/regression/cbmc-java/instance-method-user-interface-two-fields-different/I.class
new file mode 100644
index 00000000000..ad5d429af3b
Binary files /dev/null and b/regression/cbmc-java/instance-method-user-interface-two-fields-different/I.class differ
diff --git a/regression/cbmc-java/instance-method-user-interface-two-fields-different/J.class b/regression/cbmc-java/instance-method-user-interface-two-fields-different/J.class
new file mode 100644
index 00000000000..c3180580ad6
Binary files /dev/null and b/regression/cbmc-java/instance-method-user-interface-two-fields-different/J.class differ
diff --git a/regression/cbmc-java/instance-method-user-interface-two-fields-different/TestClass.class b/regression/cbmc-java/instance-method-user-interface-two-fields-different/TestClass.class
new file mode 100644
index 00000000000..bce9ce9e330
Binary files /dev/null and b/regression/cbmc-java/instance-method-user-interface-two-fields-different/TestClass.class differ
diff --git a/regression/cbmc-java/instance-method-user-interface-two-fields-different/TestClass.java b/regression/cbmc-java/instance-method-user-interface-two-fields-different/TestClass.java
new file mode 100644
index 00000000000..7f2f00d6f52
--- /dev/null
+++ b/regression/cbmc-java/instance-method-user-interface-two-fields-different/TestClass.java
@@ -0,0 +1,61 @@
+interface I
+{
+    int getANumber();
+}
+
+class A implements I {
+    public int a;
+
+    public int getANumber() { return a; }
+}
+
+class B implements I {
+    public int b;
+    public int getANumber() { return b; }
+}
+
+interface J
+{
+    int getANumber();
+}
+
+class C implements J {
+    public int c;
+    public int getANumber() { return c; }
+}
+
+class D implements J {
+    public int d;
+    public int getANumber() { return d; }
+}
+
+class TestClass
+{
+    public I someObject1;
+    public J someObject2;
+
+    public boolean foo() {
+        if(someObject1 != null && someObject2 != null)
+        {
+            if(someObject1.getANumber() == someObject2.getANumber()) {
+                return true;
+            } else {
+                return false;
+            }
+        }
+        else
+        {
+            return false;
+        }
+    }
+
+    public static void main(String[] args)
+    {
+        // ensure that A, B, C, D are referenced explicitly
+        // in order to get them converted into GOTO
+        A a = new A();
+        B b = new B();
+        C c = new C();
+        D d = new D();
+    }
+}
diff --git a/regression/cbmc-java/instance-method-user-interface-two-fields-different/test.desc b/regression/cbmc-java/instance-method-user-interface-two-fields-different/test.desc
new file mode 100644
index 00000000000..2ea5b2f5224
--- /dev/null
+++ b/regression/cbmc-java/instance-method-user-interface-two-fields-different/test.desc
@@ -0,0 +1,7 @@
+CORE
+TestClass.class
+--cover location --function TestClass.foo --show-goto-functions
+@class_identifier = "java::A";
+@class_identifier = "java::C";
+.someObject1 = \(struct I \*\)
+.someObject2 = \(struct J \*\)
diff --git a/regression/cbmc-java/static-method-user-interface-param/A.class b/regression/cbmc-java/static-method-user-interface-param/A.class
new file mode 100644
index 00000000000..86d25a78c28
Binary files /dev/null and b/regression/cbmc-java/static-method-user-interface-param/A.class differ
diff --git a/regression/cbmc-java/static-method-user-interface-param/B.class b/regression/cbmc-java/static-method-user-interface-param/B.class
new file mode 100644
index 00000000000..09103c22aac
Binary files /dev/null and b/regression/cbmc-java/static-method-user-interface-param/B.class differ
diff --git a/regression/cbmc-java/static-method-user-interface-param/I.class b/regression/cbmc-java/static-method-user-interface-param/I.class
new file mode 100644
index 00000000000..ad5d429af3b
Binary files /dev/null and b/regression/cbmc-java/static-method-user-interface-param/I.class differ
diff --git a/regression/cbmc-java/static-method-user-interface-param/TestClass.class b/regression/cbmc-java/static-method-user-interface-param/TestClass.class
new file mode 100644
index 00000000000..40b782a3bd1
Binary files /dev/null and b/regression/cbmc-java/static-method-user-interface-param/TestClass.class differ
diff --git a/regression/cbmc-java/static-method-user-interface-param/TestClass.java b/regression/cbmc-java/static-method-user-interface-param/TestClass.java
new file mode 100644
index 00000000000..ba04482cb04
--- /dev/null
+++ b/regression/cbmc-java/static-method-user-interface-param/TestClass.java
@@ -0,0 +1,42 @@
+interface I
+{
+    int getANumber();
+}
+
+class A implements I {
+    public int a;
+
+    public int getANumber() { return a; }
+}
+
+class B implements I {
+    public int b;
+    public int getANumber() { return b; }
+}
+
+class TestClass
+{
+    public static boolean foo(I someObject) {
+        if(someObject!=null)
+        {
+            int result = someObject.getANumber();
+            if(result == 42) {
+                return true;
+            } else {
+                return false;
+            }
+        }
+        else
+        {
+            return false;
+        }
+    }
+
+    public static void main(String[] args)
+    {
+        // ensure that A, B are referenced explicitly
+        // in order to get them converted into GOTO
+        A a = new A();
+        B b = new B();
+    }
+}
diff --git a/regression/cbmc-java/static-method-user-interface-param/test.desc b/regression/cbmc-java/static-method-user-interface-param/test.desc
new file mode 100644
index 00000000000..ff70e7d9ed2
--- /dev/null
+++ b/regression/cbmc-java/static-method-user-interface-param/test.desc
@@ -0,0 +1,6 @@
+CORE
+TestClass.class
+--cover location --function TestClass.foo --show-goto-functions
+@class_identifier = "java::A";
+ = \(struct I \*\)
+tmp_object_factory\$\d+ = null;
diff --git a/regression/cbmc-java/static-method-user-interface-two-params-different/A.class b/regression/cbmc-java/static-method-user-interface-two-params-different/A.class
new file mode 100644
index 00000000000..57be332d717
Binary files /dev/null and b/regression/cbmc-java/static-method-user-interface-two-params-different/A.class differ
diff --git a/regression/cbmc-java/static-method-user-interface-two-params-different/B.class b/regression/cbmc-java/static-method-user-interface-two-params-different/B.class
new file mode 100644
index 00000000000..a4af6b76682
Binary files /dev/null and b/regression/cbmc-java/static-method-user-interface-two-params-different/B.class differ
diff --git a/regression/cbmc-java/static-method-user-interface-two-params-different/C.class b/regression/cbmc-java/static-method-user-interface-two-params-different/C.class
new file mode 100644
index 00000000000..412c7c05a6c
Binary files /dev/null and b/regression/cbmc-java/static-method-user-interface-two-params-different/C.class differ
diff --git a/regression/cbmc-java/static-method-user-interface-two-params-different/D.class b/regression/cbmc-java/static-method-user-interface-two-params-different/D.class
new file mode 100644
index 00000000000..e15180a7178
Binary files /dev/null and b/regression/cbmc-java/static-method-user-interface-two-params-different/D.class differ
diff --git a/regression/cbmc-java/static-method-user-interface-two-params-different/I.class b/regression/cbmc-java/static-method-user-interface-two-params-different/I.class
new file mode 100644
index 00000000000..ad5d429af3b
Binary files /dev/null and b/regression/cbmc-java/static-method-user-interface-two-params-different/I.class differ
diff --git a/regression/cbmc-java/static-method-user-interface-two-params-different/J.class b/regression/cbmc-java/static-method-user-interface-two-params-different/J.class
new file mode 100644
index 00000000000..c3180580ad6
Binary files /dev/null and b/regression/cbmc-java/static-method-user-interface-two-params-different/J.class differ
diff --git a/regression/cbmc-java/static-method-user-interface-two-params-different/TestClass.class b/regression/cbmc-java/static-method-user-interface-two-params-different/TestClass.class
new file mode 100644
index 00000000000..fb9f3540d98
Binary files /dev/null and b/regression/cbmc-java/static-method-user-interface-two-params-different/TestClass.class differ
diff --git a/regression/cbmc-java/static-method-user-interface-two-params-different/TestClass.java b/regression/cbmc-java/static-method-user-interface-two-params-different/TestClass.java
new file mode 100644
index 00000000000..5228b22ae58
--- /dev/null
+++ b/regression/cbmc-java/static-method-user-interface-two-params-different/TestClass.java
@@ -0,0 +1,57 @@
+interface I
+{
+    int getANumber();
+}
+
+class A implements I {
+    public int a;
+    public int getANumber() { return a; }
+}
+
+class B implements I {
+    public int b;
+    public int getANumber() { return b; }
+}
+
+interface J
+{
+    int getANumber();
+}
+
+class C implements J {
+    public int c;
+    public int getANumber() { return c; }
+}
+
+class D implements J {
+    public int d;
+    public int getANumber() { return d; }
+}
+
+class TestClass
+{
+    public static boolean foo(I someObject1, J someObject2) {
+        if(someObject1 != null && someObject2 != null)
+        {
+            if(someObject1.getANumber() == someObject2.getANumber()) {
+                return true;
+            } else {
+                return false;
+            }
+        }
+        else
+        {
+            return false;
+        }
+    }
+
+    public static void main(String[] args)
+    {
+        // ensure that A, B, C, D are referenced explicitly
+        // in order to get them converted into GOTO
+        A a = new A();
+        B b = new B();
+        C c = new C();
+        D d = new D();
+    }
+}
diff --git a/regression/cbmc-java/static-method-user-interface-two-params-different/test.desc b/regression/cbmc-java/static-method-user-interface-two-params-different/test.desc
new file mode 100644
index 00000000000..2db59134dd0
--- /dev/null
+++ b/regression/cbmc-java/static-method-user-interface-two-params-different/test.desc
@@ -0,0 +1,8 @@
+CORE
+TestClass.class
+--cover location --function TestClass.foo --show-goto-functions
+@class_identifier = "java::A";
+ = \(struct I \*\)
+@class_identifier = "java::C";
+ = \(struct J \*\)
+tmp_object_factory\$\d+ = null;
diff --git a/regression/cbmc-java/static-method-user-interface-two-params-same/A.class b/regression/cbmc-java/static-method-user-interface-two-params-same/A.class
new file mode 100644
index 00000000000..86d25a78c28
Binary files /dev/null and b/regression/cbmc-java/static-method-user-interface-two-params-same/A.class differ
diff --git a/regression/cbmc-java/static-method-user-interface-two-params-same/B.class b/regression/cbmc-java/static-method-user-interface-two-params-same/B.class
new file mode 100644
index 00000000000..09103c22aac
Binary files /dev/null and b/regression/cbmc-java/static-method-user-interface-two-params-same/B.class differ
diff --git a/regression/cbmc-java/static-method-user-interface-two-params-same/I.class b/regression/cbmc-java/static-method-user-interface-two-params-same/I.class
new file mode 100644
index 00000000000..ad5d429af3b
Binary files /dev/null and b/regression/cbmc-java/static-method-user-interface-two-params-same/I.class differ
diff --git a/regression/cbmc-java/static-method-user-interface-two-params-same/TestClass.class b/regression/cbmc-java/static-method-user-interface-two-params-same/TestClass.class
new file mode 100644
index 00000000000..10ca4729e9d
Binary files /dev/null and b/regression/cbmc-java/static-method-user-interface-two-params-same/TestClass.class differ
diff --git a/regression/cbmc-java/static-method-user-interface-two-params-same/TestClass.java b/regression/cbmc-java/static-method-user-interface-two-params-same/TestClass.java
new file mode 100644
index 00000000000..145dce70525
--- /dev/null
+++ b/regression/cbmc-java/static-method-user-interface-two-params-same/TestClass.java
@@ -0,0 +1,41 @@
+interface I
+{
+    int getANumber();
+}
+
+class A implements I {
+    public int a;
+
+    public int getANumber() { return a; }
+}
+
+class B implements I {
+    public int b;
+    public int getANumber() { return b; }
+}
+
+class TestClass
+{
+    public static boolean foo(I someObject1, I someObject2) {
+        if(someObject1 != null && someObject2 != null)
+        {
+            if(someObject1.getANumber() == someObject2.getANumber()) {
+                return true;
+            } else {
+                return false;
+            }
+        }
+        else
+        {
+            return false;
+        }
+    }
+
+    public static void main(String[] args)
+    {
+        // ensure that A, B are referenced explicitly
+        // in order to get them converted into GOTO
+        A a = new A();
+        B b = new B();
+    }
+}
diff --git a/regression/cbmc-java/static-method-user-interface-two-params-same/test.desc b/regression/cbmc-java/static-method-user-interface-two-params-same/test.desc
new file mode 100644
index 00000000000..ff70e7d9ed2
--- /dev/null
+++ b/regression/cbmc-java/static-method-user-interface-two-params-same/test.desc
@@ -0,0 +1,6 @@
+CORE
+TestClass.class
+--cover location --function TestClass.foo --show-goto-functions
+@class_identifier = "java::A";
+ = \(struct I \*\)
+tmp_object_factory\$\d+ = null;
diff --git a/regression/strings-smoke-tests/jsonArrays/test.desc b/regression/strings-smoke-tests/jsonArrays/test.desc
index e59f08d44b4..71edef45763 100644
--- a/regression/strings-smoke-tests/jsonArrays/test.desc
+++ b/regression/strings-smoke-tests/jsonArrays/test.desc
@@ -3,7 +3,7 @@ test.class
 --refine-strings --function test.check --json-ui --trace --string-max-length 100 --cover location
 ^EXIT=0$
 ^SIGNAL=0$
-\"data\".*\"tmp_object_factory\$6.*\"
+\"data\".*\"tmp_object_factory\$\d+.*\"
 --
 This checks that tmp_object_factory$6 gets affected to the data field
 of some strings, which was not the case in previous versions of cbmc,
diff --git a/src/java_bytecode/Makefile b/src/java_bytecode/Makefile
index 5125f2f6664..ba28e401492 100644
--- a/src/java_bytecode/Makefile
+++ b/src/java_bytecode/Makefile
@@ -2,6 +2,7 @@ SRC = bytecode_info.cpp \
       character_refine_preprocess.cpp \
       ci_lazy_methods.cpp \
       expr2java.cpp \
+      get_concrete_class_alphabetically.cpp \
       jar_file.cpp \
       java_bytecode_convert_class.cpp \
       java_bytecode_convert_method.cpp \
@@ -24,6 +25,7 @@ SRC = bytecode_info.cpp \
       java_string_library_preprocess.cpp \
       java_types.cpp \
       java_utils.cpp \
+      select_pointer_type.cpp \
       # Empty last line
 
 INCLUDES= -I ..
diff --git a/src/java_bytecode/get_concrete_class_alphabetically.cpp b/src/java_bytecode/get_concrete_class_alphabetically.cpp
new file mode 100644
index 00000000000..01bf6519e21
--- /dev/null
+++ b/src/java_bytecode/get_concrete_class_alphabetically.cpp
@@ -0,0 +1,123 @@
+/*******************************************************************\
+
+Module: Java Bytecode Language Conversion
+
+Author: DiffBlue Limited. All rights reserved.
+
+\*******************************************************************/
+
+/// \file
+/// Select a subclass of the provided type, picking the alphabetically first
+
+#include "get_concrete_class_alphabetically.h"
+
+#include <algorithm>
+
+#include <util/invariant.h>
+#include <util/namespace.h>
+#include <util/std_types.h>
+#include <util/symbol_table.h>
+
+#include <goto-programs/class_hierarchy.h>
+
+/// Get type the pointer is pointing to, replacing it with a concrete
+/// implementation when it is abstract.
+/// \param `pointer_type`: The type of the pointer
+/// \return The subtype of the pointer. If this is an abstract class then we
+///   will randomly select a concrete child class.
+pointer_typet get_concrete_class_alphabeticallyt::operator()(
+  const pointer_typet &pointer_type)
+{
+  const typet &subtype=ns.follow(pointer_type.subtype());
+  INVARIANT(subtype.id()==ID_struct,
+    "Can only find derived classes of class types");
+
+  const class_typet &class_type=to_class_type(subtype);
+  INVARIANT(class_type.is_class(),
+    "Can only find derived classes of class types");
+
+  const class_typet &selected_subtype=select_concrete_type(class_type);
+
+  // If we've not selected a subtype (i.e. there aren't any) we should
+  // return the original unmodified type
+  if(selected_subtype==class_type)
+  {
+    return pointer_type;
+  }
+
+  // Recreate the pointer_type as it was before
+  if(pointer_type.subtype().id()==ID_symbol)
+  {
+    INVARIANT(
+      ns.get_symbol_table().has_symbol(selected_subtype.get(ID_name)),
+      "Selected a type that wasn't in the symbol table");
+
+    symbol_typet symbol_subtype(selected_subtype.get(ID_name));
+
+    return pointer_typet(symbol_subtype);
+  }
+  else
+  {
+    return pointer_typet(selected_subtype);
+  }
+}
+
+/// Select the alphabetically first concrete sub-class of an abstract class or
+/// interface This can be then used when analyzing the function.
+/// \param `abstract_type`: an class type that is abstract (i.e. either an
+///   interface or a abstract class).
+/// \return A class_typet that the GOTO code should instantiate to fill this
+///   type. This will be a concrete type unless no concrete types are found that
+///   inherit from the abstract_type. `
+class_typet get_concrete_class_alphabeticallyt::select_concrete_type(
+  const class_typet &abstract_type)
+{
+  const symbol_tablet &symbol_table=ns.get_symbol_table();
+  // abstract class - we should find a derived class ideally to test with
+  class_hierarchyt class_hierachy;
+  class_hierachy(symbol_table);
+  class_hierarchyt::idst child_ids=
+    class_hierachy.get_children_trans(abstract_type.get_string(ID_name));
+
+  // filter out abstract classes
+  class_hierarchyt::idst concrete_childen;
+  std::copy_if(
+    child_ids.begin(),
+    child_ids.end(),
+    std::back_inserter(concrete_childen),
+    [&] (const irep_idt &child_class_id)
+    {
+      const symbolt &type_symbol=symbol_table.lookup(child_class_id);
+      const class_typet &child_type=to_class_type(type_symbol.type);
+      return child_type.is_class() && !child_type.is_abstract();
+    });
+
+
+  if(!concrete_childen.empty())
+  {
+    // Alphabetize the list
+    std::sort(
+      concrete_childen.begin(),
+      concrete_childen.end(),
+      [](const irep_idt &a, const irep_idt &b)
+      {
+        return a.compare(b)<0;
+      });
+
+    const symbolt &type_symbol=
+      symbol_table.lookup(concrete_childen.front());
+    INVARIANT(
+      type_symbol.type.id()==ID_struct,
+      "Should always substitute a class type");
+
+    const class_typet &child_type=to_class_type(type_symbol.type);
+    INVARIANT(child_type.is_class(), "Should always substitute a class type");
+    return child_type;
+  }
+  else
+  {
+    // else no children in the symbol table - here the best we can do is
+    // mock the interface/abstract object
+    return abstract_type;
+  }
+}
diff --git a/src/java_bytecode/get_concrete_class_alphabetically.h b/src/java_bytecode/get_concrete_class_alphabetically.h
new file mode 100644
index 00000000000..08f2c00ec50
--- /dev/null
+++ b/src/java_bytecode/get_concrete_class_alphabetically.h
@@ -0,0 +1,32 @@
+/*******************************************************************\
+
+Module: Java Bytecode Language Conversion
+
+Author: DiffBlue Limited. All rights reserved.
+
+\*******************************************************************/
+
+/// \file
+/// Select a subclass of the provided type, picking the alphabetically first
+
+#ifndef CPROVER_JAVA_BYTECODE_GET_CONCRETE_CLASS_ALPHABETICALLY_H
+#define CPROVER_JAVA_BYTECODE_GET_CONCRETE_CLASS_ALPHABETICALLY_H
+
+#include <util/std_types.h>
+
+class namespacet;
+
+class get_concrete_class_alphabeticallyt
+{
+public:
+  explicit get_concrete_class_alphabeticallyt(const namespacet &ns):ns(ns)
+  {}
+
+  pointer_typet operator()(const pointer_typet &pointer_type);
+
+private:
+  const namespacet &ns;
+  class_typet select_concrete_type(const class_typet &abstract_type);
+};
+
+#endif // CPROVER_JAVA_BYTECODE_GET_CONCRETE_CLASS_ALPHABETICALLY_H
diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp
index 61f287ced07..8726cc5f931 100644
--- a/src/java_bytecode/java_object_factory.cpp
+++ b/src/java_bytecode/java_object_factory.cpp
@@ -6,6 +6,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
+#include "java_object_factory.h"
 
 #include <unordered_set>
 #include <sstream>
@@ -26,7 +27,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <goto-programs/goto_functions.h>
 
-#include "java_object_factory.h"
+
+#include <java_bytecode/select_pointer_type.h>
 #include "java_types.h"
 #include "java_utils.h"
 
@@ -59,11 +61,6 @@ class java_object_factoryt
     const exprt &expr,
     const pointer_typet &ptr_type);
 
-  void gen_pointer_target_init(
-    const exprt &expr,
-    const typet &target_type,
-    bool create_dynamic_objects,
-    update_in_placet update_in_place);
 
   code_assignt get_null_assignment(
     const exprt &expr,
@@ -74,7 +71,7 @@ class java_object_factoryt
     const exprt &expr,
     const typet &target_type,
     bool create_dynamic_objects,
-    update_in_placet);
+    update_in_placet update_in_place);
 
   void allocate_nondet_length_array(
     code_blockt &assignments,
@@ -137,6 +134,11 @@ class java_object_factoryt
     bool create_dynamic_objects,
     const struct_typet &struct_type,
     const update_in_placet &update_in_place);
+
+  symbol_exprt gen_nondet_subtype_pointer_init(
+    code_blockt &assignments,
+    bool create_dynamic_objects,
+    const pointer_typet &substitute_pointer_type);
 };
 
 /// Generates code for allocating a dynamic object. This is used in
@@ -356,8 +358,10 @@ void java_object_factoryt::gen_pointer_target_init(
     if(target.id()==ID_address_of)
       init_expr=target.op0();
     else
+    {
       init_expr=
         dereference_exprt(target, target.type().subtype());
+    }
     gen_nondet_init(
       assignments,
       init_expr,
@@ -394,11 +398,33 @@ void java_object_factoryt::gen_nondet_pointer_init(
   const pointer_typet &pointer_type,
   const update_in_placet &update_in_place)
 {
+  select_pointer_typet pointer_type_selector(ns);
+  const pointer_typet &replacement_pointer_type=
+    pointer_type_selector(pointer_type);
+
+  // If we are changing the pointer, we generate code for creating a pointer
+  // to the substituted type instead
+  if(replacement_pointer_type!=pointer_type)
+  {
+    const symbol_exprt real_pointer_symbol=gen_nondet_subtype_pointer_init(
+      assignments,
+      create_dynamic_objects,
+      replacement_pointer_type);
+
+    // Having created a pointer to object of type replacement_pointer_type
+    // we now assign it back to the original pointer with a cast
+    // from pointer_type to replacement_pointer_type
+    assignments.add(
+      code_assignt(expr, typecast_exprt(real_pointer_symbol, pointer_type)));
+    return;
+  }
+
   const typet &subtype=ns.follow(pointer_type.subtype());
   if(subtype.id()==ID_struct)
   {
     const struct_typet &struct_type=to_struct_type(subtype);
     const irep_idt &struct_tag=struct_type.get_tag();
+
     // If this is a recursive type of some kind, set null.
     if(!recursion_set.insert(struct_tag).second)
     {
@@ -498,6 +524,41 @@ void java_object_factoryt::gen_nondet_pointer_init(
   }
 }
 
+/// Generate GOTO code to initalize the selected concrete type
+/// A { ... } tmp_object;
+/// A.x = NONDET ...
+/// // non-det init of all the fields of A
+/// A * p = &tmp_object
+/// expr = (I *)p
+/// \param assignments: the code to append to
+/// \param create_dynamic_objects: if true, use malloc to allocate objects;
+///   otherwise generate fresh static symbols.
+/// \param replacement_pointer: The type of the pointer we actually want to
+///   to create.
+/// \return The symbol expression that corresponds to the pointer to object
+///   created of the required type.
+symbol_exprt java_object_factoryt::gen_nondet_subtype_pointer_init(
+  code_blockt &assignments,
+  bool create_dynamic_objects,
+  const pointer_typet &replacement_pointer)
+{
+  symbolt new_symbol=new_tmp_symbol(symbol_table, loc, replacement_pointer);
+
+  // Generate a new object into this new symbol
+  gen_nondet_init(
+    assignments,
+    new_symbol.symbol_expr(),
+    false,
+    "",
+    false,
+    create_dynamic_objects,
+    false,
+    typet(),
+    update_in_placet::NO_UPDATE_IN_PLACE);
+
+  return new_symbol.symbol_expr();
+}
+
 /// Initialises an object tree rooted at `expr`, allocating child objects as
 /// necessary and nondet-initialising their members, or if MUST_UPDATE_IN_PLACE
 /// is set, re-initialising already-allocated objects.
@@ -660,7 +721,7 @@ void java_object_factoryt::gen_nondet_init(
   }
 }
 
-/// Allocates a fresh array. Single-use herem at the moment, but useful to keep
+/// Allocates a fresh array. Single-use at the moment, but useful to keep
 /// as a separate function for downstream branches.
 /// \par parameters: `lhs`, symbol to assign the new array structure
 /// `max_length_expr`, maximum length of the new array (minimum is fixed at zero
@@ -873,10 +934,6 @@ exprt object_factory(
 
   std::vector<const symbolt *> symbols_created;
   symbols_created.push_back(main_symbol_ptr);
-
-  symbolt &aux_symbol=new_tmp_symbol(symbol_table, loc, type);
-  aux_symbol.is_static_lifetime=true;
-
   java_object_factoryt state(
     symbols_created,
     loc,
diff --git a/src/java_bytecode/select_pointer_type.cpp b/src/java_bytecode/select_pointer_type.cpp
new file mode 100644
index 00000000000..88092503a37
--- /dev/null
+++ b/src/java_bytecode/select_pointer_type.cpp
@@ -0,0 +1,66 @@
+/*******************************************************************\
+
+ Module: Java Bytecode Language Conversion
+
+ Author: DiffBlue Limited. All rights reserved.
+
+\*******************************************************************/
+
+/// \file
+/// Handle selection of correct pointer type (for example changing abstract
+/// classes to concrete versions).
+
+#include "select_pointer_type.h"
+
+#include <java_bytecode/get_concrete_class_alphabetically.h>
+
+#include <util/invariant.h>
+#include <util/namespace.h>
+#include <util/std_types.h>
+
+
+/// Select what type should be used for a given pointer type. If the class
+/// pointed to is abstract then we consider using a subclass of it.
+/// \param pointer_type: The pointer type replace
+/// \return A pointer type where the subtype may have been modified
+pointer_typet select_pointer_typet::operator()(
+  const pointer_typet &pointer_type) const
+{
+  // Currently only replace abstract classes
+  // Potentially in the future we might want to consider anything with
+  // derived classes
+  if(!is_abstract_type(pointer_type))
+  {
+    return pointer_type;
+  }
+
+  // TODO(tkiley): Look to see whether there is a suitable model class to use
+
+  get_concrete_class_alphabeticallyt get_concrete_class_alphabetically(ns);
+  const pointer_typet &resolved_type=
+    get_concrete_class_alphabetically(pointer_type);
+
+  return resolved_type;
+}
+
+/// Find out whether a pointer is pointing to an abstract type (either an
+/// abstract class or an interface).
+/// \param pointer_type: The type of the pointer
+/// \return True if the type pointed to is either an abstract class or an
+///   interface.
+bool select_pointer_typet::is_abstract_type(
+  const pointer_typet &pointer_type) const
+{
+  const typet &pointing_to_type=ns.follow(pointer_type.subtype());
+  if(pointing_to_type.id()==ID_struct)
+  {
+    const class_typet &class_type=to_class_type(pointing_to_type);
+    return class_type.is_class() && class_type.is_abstract();
+  }
+  else
+  {
+    // we are dealing with some other type that a reference to a polymorphic
+    // class so therefore we are definitely not abstract
+    return false;
+  }
+}
diff --git a/src/java_bytecode/select_pointer_type.h b/src/java_bytecode/select_pointer_type.h
new file mode 100644
index 00000000000..fac85cad543
--- /dev/null
+++ b/src/java_bytecode/select_pointer_type.h
@@ -0,0 +1,32 @@
+/*******************************************************************\
+
+ Module: Java Bytecode Language Conversion
+
+ Author: DiffBlue Limited. All rights reserved.
+
+\*******************************************************************/
+#ifndef CPROVER_JAVA_BYTECODE_SELECT_POINTER_TYPE_H
+#define CPROVER_JAVA_BYTECODE_SELECT_POINTER_TYPE_H
+
+/// \file
+/// Handle selection of correct pointer type (for example changing abstract
+/// classes to concrete versions).
+
+#include <util/std_types.h>
+
+class namespacet;
+
+class select_pointer_typet
+{
+public:
+  explicit select_pointer_typet(const namespacet &ns):ns(ns)
+  {}
+
+  pointer_typet operator()(const pointer_typet &pointer_type) const;
+private:
+  bool is_abstract_type(const pointer_typet &pointer_type) const;
+
+  const namespacet &ns;
+};
+
+#endif // CPROVER_JAVA_BYTECODE_SELECT_POINTER_TYPE_H
diff --git a/src/util/symbol_table.cpp b/src/util/symbol_table.cpp
index 2dd167600cf..43c0301dd7e 100644
--- a/src/util/symbol_table.cpp
+++ b/src/util/symbol_table.cpp
@@ -13,9 +13,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 /// Add a new symbol to the symbol table
 /// \param symbol: The symbol to be added to the symbol table
-/// \return Returns a boolean indicating whether the process failed, which
-///   should only happen if there is a symbol with the same name already in the
-///   symbol table
+/// \return Returns true if the process failed, which should only happen if
+///   there is a symbol with the same name already in the symbol table.
 bool symbol_tablet::add(const symbolt &symbol)
 {
   if(!symbols.insert(std::pair<irep_idt, symbolt>(symbol.name, symbol)).second)