From deae734fcd9420ad4a341e3109ec77e2ed863e7a Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Sat, 21 Apr 2018 15:16:38 +0100
Subject: [PATCH 1/3] Move instanceof and exceptions removal back to
 goto-programs

---
 .../goto_analyzer_parse_options.cpp           | 45 ++++++++++---------
 src/goto-diff/goto_diff_parse_options.cpp     | 45 +++++++++----------
 src/goto-programs/Makefile                    |  2 +
 .../remove_exceptions.cpp                     |  0
 .../remove_exceptions.h                       |  0
 .../remove_instanceof.cpp                     |  0
 .../remove_instanceof.h                       |  0
 .../remove_virtual_functions.cpp              |  6 +++
 src/java_bytecode/Makefile                    |  2 -
 src/java_bytecode/ci_lazy_methods.cpp         |  4 +-
 .../java_bytecode_convert_method.cpp          | 23 +++++-----
 .../java_bytecode_internal_additions.cpp      |  2 +-
 src/java_bytecode/java_entry_point.cpp        | 23 ++++++++--
 src/jbmc/jbmc_parse_options.cpp               | 37 ++++++++-------
 14 files changed, 105 insertions(+), 84 deletions(-)
 rename src/{java_bytecode => goto-programs}/remove_exceptions.cpp (100%)
 rename src/{java_bytecode => goto-programs}/remove_exceptions.h (100%)
 rename src/{java_bytecode => goto-programs}/remove_instanceof.cpp (100%)
 rename src/{java_bytecode => goto-programs}/remove_instanceof.h (100%)

diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp
index 4df96cddc3e..8540991bc94 100644
--- a/src/goto-analyzer/goto_analyzer_parse_options.cpp
+++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp
@@ -16,38 +16,41 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <fstream>
 #include <memory>
 
+#include <analyses/constant_propagator.h>
+#include <analyses/dependence_graph.h>
+#include <analyses/goto_check.h>
+#include <analyses/interval_domain.h>
+#include <analyses/is_threaded.h>
+#include <analyses/local_may_alias.h>
+
 #include <ansi-c/ansi_c_language.h>
+
+#include <cbmc/version.h>
+
 #include <cpp/cpp_language.h>
-#include <java_bytecode/java_bytecode_language.h>
-#include <jsil/jsil_language.h>
 
+#include <goto-programs/goto_convert_functions.h>
+#include <goto-programs/goto_inline.h>
 #include <goto-programs/initialize_goto_model.h>
-#include <goto-programs/set_properties.h>
+#include <goto-programs/link_to_library.h>
+#include <goto-programs/read_goto_binary.h>
+#include <goto-programs/remove_exceptions.h>
 #include <goto-programs/remove_function_pointers.h>
 #include <goto-programs/remove_virtual_functions.h>
+#include <goto-programs/remove_instanceof.h>
 #include <goto-programs/remove_returns.h>
 #include <goto-programs/remove_vector.h>
 #include <goto-programs/remove_complex.h>
 #include <goto-programs/remove_asm.h>
-#include <goto-programs/goto_convert_functions.h>
+#include <goto-programs/set_properties.h>
 #include <goto-programs/show_properties.h>
 #include <goto-programs/show_symbol_table.h>
-#include <goto-programs/read_goto_binary.h>
-#include <goto-programs/goto_inline.h>
-#include <goto-programs/link_to_library.h>
-
-#include <analyses/is_threaded.h>
-#include <analyses/goto_check.h>
-#include <analyses/local_may_alias.h>
-#include <analyses/constant_propagator.h>
-#include <analyses/dependence_graph.h>
-#include <analyses/interval_domain.h>
 
-#include <java_bytecode/remove_exceptions.h>
-#include <java_bytecode/remove_instanceof.h>
-
-#include <langapi/mode.h>
 #include <langapi/language.h>
+#include <langapi/mode.h>
+
+#include <java_bytecode/java_bytecode_language.h>
+#include <jsil/jsil_language.h>
 
 #include <util/options.h>
 #include <util/config.h>
@@ -55,13 +58,11 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/unicode.h>
 #include <util/exit_codes.h>
 
-#include <cbmc/version.h>
-
-#include "taint_analysis.h"
-#include "unreachable_instructions.h"
 #include "static_show_domain.h"
 #include "static_simplifier.h"
 #include "static_verifier.h"
+#include "taint_analysis.h"
+#include "unreachable_instructions.h"
 
 goto_analyzer_parse_optionst::goto_analyzer_parse_optionst(
   int argc,
diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp
index c2b7bbb34ca..27601f421f8 100644
--- a/src/goto-diff/goto_diff_parse_options.cpp
+++ b/src/goto-diff/goto_diff_parse_options.cpp
@@ -16,53 +16,52 @@ Author: Peter Schrammel
 #include <iostream>
 #include <memory>
 
-#include <util/string2int.h>
-#include <util/config.h>
-#include <util/options.h>
-#include <util/make_unique.h>
-#include <util/exit_codes.h>
-
-#include <langapi/language.h>
+#include <cbmc/version.h>
 
 #include <goto-programs/goto_convert_functions.h>
+#include <goto-programs/goto_inline.h>
 #include <goto-programs/instrument_preconditions.h>
+#include <goto-programs/link_to_library.h>
+#include <goto-programs/loop_ids.h>
 #include <goto-programs/mm_io.h>
+#include <goto-programs/read_goto_binary.h>
+#include <goto-programs/remove_asm.h>
+#include <goto-programs/remove_complex.h>
+#include <goto-programs/remove_exceptions.h>
 #include <goto-programs/remove_function_pointers.h>
-#include <goto-programs/remove_virtual_functions.h>
+#include <goto-programs/remove_instanceof.h>
 #include <goto-programs/remove_returns.h>
+#include <goto-programs/remove_skip.h>
 #include <goto-programs/remove_vector.h>
-#include <goto-programs/remove_complex.h>
-#include <goto-programs/remove_asm.h>
+#include <goto-programs/remove_virtual_functions.h>
 #include <goto-programs/remove_unused_functions.h>
-#include <goto-programs/remove_skip.h>
-#include <goto-programs/goto_inline.h>
 #include <goto-programs/show_properties.h>
 #include <goto-programs/set_properties.h>
-#include <goto-programs/read_goto_binary.h>
 #include <goto-programs/string_abstraction.h>
 #include <goto-programs/string_instrumentation.h>
-#include <goto-programs/loop_ids.h>
-#include <goto-programs/link_to_library.h>
-
-#include <goto-symex/rewrite_union.h>
-#include <goto-symex/adjust_float_expressions.h>
 
 #include <goto-instrument/cover.h>
 
-#include <pointer-analysis/add_failed_symbols.h>
+#include <goto-symex/adjust_float_expressions.h>
+#include <goto-symex/rewrite_union.h>
 
 #include <java_bytecode/java_bytecode_language.h>
-#include <java_bytecode/remove_instanceof.h>
-#include <java_bytecode/remove_exceptions.h>
 
+#include <langapi/language.h>
 #include <langapi/mode.h>
 
-#include <cbmc/version.h>
+#include <pointer-analysis/add_failed_symbols.h>
+
+#include <util/config.h>
+#include <util/exit_codes.h>
+#include <util/make_unique.h>
+#include <util/options.h>
+#include <util/string2int.h>
 
+#include "change_impact.h"
 #include "goto_diff.h"
 #include "syntactic_diff.h"
 #include "unified_diff.h"
-#include "change_impact.h"
 
 goto_diff_parse_optionst::goto_diff_parse_optionst(int argc, const char **argv):
   parse_options_baset(GOTO_DIFF_OPTIONS, argc, argv),
diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile
index c16ba9f9ae0..40b86a50f29 100644
--- a/src/goto-programs/Makefile
+++ b/src/goto-programs/Makefile
@@ -43,7 +43,9 @@ SRC = basic_blocks.cpp \
       remove_calls_no_body.cpp \
       remove_complex.cpp \
       remove_const_function_pointers.cpp \
+      remove_exceptions.cpp \
       remove_function_pointers.cpp \
+      remove_instanceof.cpp \
       remove_returns.cpp \
       remove_skip.cpp \
       remove_unreachable.cpp \
diff --git a/src/java_bytecode/remove_exceptions.cpp b/src/goto-programs/remove_exceptions.cpp
similarity index 100%
rename from src/java_bytecode/remove_exceptions.cpp
rename to src/goto-programs/remove_exceptions.cpp
diff --git a/src/java_bytecode/remove_exceptions.h b/src/goto-programs/remove_exceptions.h
similarity index 100%
rename from src/java_bytecode/remove_exceptions.h
rename to src/goto-programs/remove_exceptions.h
diff --git a/src/java_bytecode/remove_instanceof.cpp b/src/goto-programs/remove_instanceof.cpp
similarity index 100%
rename from src/java_bytecode/remove_instanceof.cpp
rename to src/goto-programs/remove_instanceof.cpp
diff --git a/src/java_bytecode/remove_instanceof.h b/src/goto-programs/remove_instanceof.h
similarity index 100%
rename from src/java_bytecode/remove_instanceof.h
rename to src/goto-programs/remove_instanceof.h
diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp
index a242577e8cd..2d543601cc7 100644
--- a/src/goto-programs/remove_virtual_functions.cpp
+++ b/src/goto-programs/remove_virtual_functions.cpp
@@ -12,8 +12,14 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <algorithm>
 
+#include <langapi/language.h>
+#include <langapi/mode.h>
+
+#include <util/c_types.h>
+#include <util/prefix.h>
 #include <util/type_eq.h>
 
+#include "class_hierarchy.h"
 #include "class_identifier.h"
 #include "goto_model.h"
 #include "resolve_inherited_component.h"
diff --git a/src/java_bytecode/Makefile b/src/java_bytecode/Makefile
index 13aa8e6c2ca..3fa30f99a32 100644
--- a/src/java_bytecode/Makefile
+++ b/src/java_bytecode/Makefile
@@ -31,8 +31,6 @@ SRC = bytecode_info.cpp \
       java_types.cpp \
       java_utils.cpp \
       mz_zip_archive.cpp \
-      remove_exceptions.cpp \
-      remove_instanceof.cpp \
       remove_java_new.cpp \
       replace_java_nondet.cpp \
       select_pointer_type.cpp \
diff --git a/src/java_bytecode/ci_lazy_methods.cpp b/src/java_bytecode/ci_lazy_methods.cpp
index ccb892a296c..62c03ad2a85 100644
--- a/src/java_bytecode/ci_lazy_methods.cpp
+++ b/src/java_bytecode/ci_lazy_methods.cpp
@@ -11,11 +11,11 @@
 #include "java_class_loader.h"
 #include "java_utils.h"
 #include "java_string_library_preprocess.h"
-#include "remove_exceptions.h"
 
+#include <goto-programs/remove_exceptions.h>
+#include <goto-programs/resolve_inherited_component.h>
 #include <util/suffix.h>
 
-#include <goto-programs/resolve_inherited_component.h>
 
 /// Constructor for lazy-method loading
 /// \param symbol_table: the symbol table to use
diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp
index 9b221d4298c..fd0eb17e9a4 100644
--- a/src/java_bytecode/java_bytecode_convert_method.cpp
+++ b/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -13,14 +13,22 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <iostream>
 #endif
 
+#include "bytecode_info.h"
 #include "java_bytecode_convert_method.h"
 #include "java_bytecode_convert_method_class.h"
-#include "bytecode_info.h"
 #include "java_static_initializers.h"
 #include "java_string_library_preprocess.h"
 #include "java_types.h"
 #include "java_utils.h"
-#include "remove_exceptions.h"
+
+#include <analyses/cfg_dominators.h>
+
+#include <goto-programs/cfg.h>
+#include <goto-programs/class_hierarchy.h>
+#include <goto-programs/remove_exceptions.h>
+#include <goto-programs/resolve_inherited_component.h>
+
+#include <linking/zero_initializer.h>
 
 #include <util/arith_tools.h>
 #include <util/c_types.h>
@@ -32,18 +40,11 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/std_expr.h>
 #include <util/string2int.h>
 
-#include <linking/zero_initializer.h>
-
-#include <goto-programs/cfg.h>
-#include <goto-programs/class_hierarchy.h>
-#include <goto-programs/resolve_inherited_component.h>
-#include <analyses/cfg_dominators.h>
-
-#include <limits>
 #include <algorithm>
 #include <functional>
-#include <unordered_set>
+#include <limits>
 #include <regex>
+#include <unordered_set>
 
 /// Given a string of the format '?blah?', will return true when compared
 /// against a string that matches appart from any characters that are '?'
diff --git a/src/java_bytecode/java_bytecode_internal_additions.cpp b/src/java_bytecode/java_bytecode_internal_additions.cpp
index 106cd0fb642..9229aab3fec 100644
--- a/src/java_bytecode/java_bytecode_internal_additions.cpp
+++ b/src/java_bytecode/java_bytecode_internal_additions.cpp
@@ -9,7 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "java_bytecode_internal_additions.h"
 
 // For INFLIGHT_EXCEPTION_VARIABLE_NAME
-#include "remove_exceptions.h"
+#include <goto-programs/remove_exceptions.h>
 
 #include <util/std_types.h>
 #include <util/cprover_prefix.h>
diff --git a/src/java_bytecode/java_entry_point.cpp b/src/java_bytecode/java_entry_point.cpp
index 2556ee4d7e9..a8aaa7bdccd 100644
--- a/src/java_bytecode/java_entry_point.cpp
+++ b/src/java_bytecode/java_entry_point.cpp
@@ -8,15 +8,30 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "java_entry_point.h"
 
-#include <util/config.h>
-#include <util/string_constant.h>
-#include <util/suffix.h>
+#include <algorithm>
+#include <set>
+#include <unordered_set>
 
-#include <goto-programs/goto_functions.h>
+#include <goto-programs/remove_exceptions.h>
 
 #include <linking/static_lifetime_init.h>
 
+#include <util/arith_tools.h>
+#include <util/c_types.h>
+#include <util/config.h>
+#include <util/cprover_prefix.h>
+#include <util/message.h>
+#include <util/namespace.h>
+#include <util/pointer_offset_size.h>
+#include <util/prefix.h>
+#include <util/std_code.h>
+#include <util/std_expr.h>
+#include <util/std_types.h>
+#include <util/string_constant.h>
+#include <util/suffix.h>
+
 #include "java_object_factory.h"
+#include "java_types.h"
 #include "java_utils.h"
 
 static void create_initialize(symbol_table_baset &symbol_table)
diff --git a/src/jbmc/jbmc_parse_options.cpp b/src/jbmc/jbmc_parse_options.cpp
index 031d7aec587..8a30327613f 100644
--- a/src/jbmc/jbmc_parse_options.cpp
+++ b/src/jbmc/jbmc_parse_options.cpp
@@ -16,49 +16,48 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <iostream>
 #include <memory>
 
-#include <util/string2int.h>
-#include <util/config.h>
-#include <util/unicode.h>
-#include <util/invariant.h>
-
-#include <langapi/language.h>
-
 #include <ansi-c/ansi_c_language.h>
 
+#include <cbmc/version.h>
+
 #include <goto-programs/convert_nondet.h>
 #include <goto-programs/lazy_goto_model.h>
 #include <goto-programs/instrument_preconditions.h>
 #include <goto-programs/goto_convert_functions.h>
 #include <goto-programs/goto_inline.h>
 #include <goto-programs/loop_ids.h>
-#include <goto-programs/remove_virtual_functions.h>
-#include <goto-programs/remove_returns.h>
 #include <goto-programs/remove_asm.h>
-#include <goto-programs/remove_unused_functions.h>
+#include <goto-programs/remove_exceptions.h>
+#include <goto-programs/remove_instanceof.h>
+#include <goto-programs/remove_returns.h>
 #include <goto-programs/remove_skip.h>
+#include <goto-programs/remove_unused_functions.h>
+#include <goto-programs/remove_virtual_functions.h>
 #include <goto-programs/set_properties.h>
 #include <goto-programs/show_goto_functions.h>
 #include <goto-programs/show_symbol_table.h>
 #include <goto-programs/show_properties.h>
 
-#include <goto-symex/adjust_float_expressions.h>
-
 #include <goto-instrument/full_slicer.h>
 #include <goto-instrument/reachability_slicer.h>
 #include <goto-instrument/nondet_static.h>
 
-#include <pointer-analysis/add_failed_symbols.h>
-
-#include <langapi/mode.h>
+#include <goto-symex/adjust_float_expressions.h>
 
 #include <java_bytecode/java_bytecode_language.h>
 #include <java_bytecode/java_enum_static_init_unwind_handler.h>
-#include <java_bytecode/remove_exceptions.h>
-#include <java_bytecode/remove_instanceof.h>
-#include <java_bytecode/remove_java_new.h>
 #include <java_bytecode/replace_java_nondet.h>
+#include <java_bytecode/remove_java_new.h>
 
-#include <cbmc/version.h>
+#include <langapi/mode.h>
+#include <langapi/language.h>
+
+#include <pointer-analysis/add_failed_symbols.h>
+
+#include <util/string2int.h>
+#include <util/config.h>
+#include <util/unicode.h>
+#include <util/invariant.h>
 
 jbmc_parse_optionst::jbmc_parse_optionst(int argc, const char **argv):
   parse_options_baset(JBMC_OPTIONS, argc, argv),

From 9d09ebc78a89139b5fbd5143aa98e3a7338da7d0 Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Sat, 17 Mar 2018 13:15:57 +0000
Subject: [PATCH 2/3] Remove java_bytecode dependency from remove_instanceof

---
 src/ansi-c/ansi_c_language.h                 |  6 ++++++
 src/cpp/cpp_language.h                       |  6 ++++++
 src/goto-programs/remove_instanceof.cpp      | 14 ++++++++++----
 src/java_bytecode/java_bytecode_language.cpp |  5 +++++
 src/java_bytecode/java_bytecode_language.h   |  2 ++
 src/jsil/jsil_language.h                     |  6 ++++++
 src/langapi/language.h                       |  3 +++
 7 files changed, 38 insertions(+), 4 deletions(-)

diff --git a/src/ansi-c/ansi_c_language.h b/src/ansi-c/ansi_c_language.h
index b23bdad6469..628c5bab08c 100644
--- a/src/ansi-c/ansi_c_language.h
+++ b/src/ansi-c/ansi_c_language.h
@@ -63,6 +63,12 @@ class ansi_c_languaget:public languaget
     exprt &expr,
     const namespacet &ns) override;
 
+  symbol_typet root_base_class_type() override
+  {
+    // does not exist
+    UNREACHABLE;
+  }
+
   std::unique_ptr<languaget> new_language() override
   { return util_make_unique<ansi_c_languaget>(); }
 
diff --git a/src/cpp/cpp_language.h b/src/cpp/cpp_language.h
index 3f474005f15..a3db8124f44 100644
--- a/src/cpp/cpp_language.h
+++ b/src/cpp/cpp_language.h
@@ -75,6 +75,12 @@ class cpp_languaget:public languaget
     exprt &expr,
     const namespacet &ns) override;
 
+  symbol_typet root_base_class_type() override
+  {
+    // TODO: need a synthetic wrapper with a member that holds the type_info
+    UNIMPLEMENTED;
+  }
+
   std::unique_ptr<languaget> new_language() override
   { return util_make_unique<cpp_languaget>(); }
 
diff --git a/src/goto-programs/remove_instanceof.cpp b/src/goto-programs/remove_instanceof.cpp
index cb93fcbbb98..02e998eeb9b 100644
--- a/src/goto-programs/remove_instanceof.cpp
+++ b/src/goto-programs/remove_instanceof.cpp
@@ -14,8 +14,10 @@ Author: Chris Smowton, chris.smowton@diffblue.com
 #include <goto-programs/class_hierarchy.h>
 #include <goto-programs/class_identifier.h>
 
+#include <langapi/mode.h>
+#include <langapi/language.h>
+
 #include <util/fresh_symbol.h>
-#include <java_bytecode/java_types.h>
 
 #include <sstream>
 
@@ -100,9 +102,13 @@ std::size_t remove_instanceoft::lower_instanceof(
   // We actually insert the assignment instruction after the existing one.
   // This will briefly be ill-formed (use before def of instanceof_tmp) but the
   // two will subsequently switch places. This makes sure that the inserted
-  // assignement doesn't end up before any labels pointing at this instruction.
-  symbol_typet jlo=to_symbol_type(java_lang_object_type().subtype());
-  exprt object_clsid=get_class_identifier_field(check_ptr, jlo, ns);
+  // assignment doesn't end up before any labels pointing at this instruction.
+  const irep_idt &mode = get_mode_from_identifier(
+    ns, to_symbol_type(target_type).get_identifier());
+  const auto language = get_language_from_mode(mode);
+  CHECK_RETURN(language);
+  exprt object_clsid =
+    get_class_identifier_field(check_ptr, language->root_base_class_type(), ns);
 
   symbolt &newsym = get_fresh_aux_symbol(
     object_clsid.type(),
diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp
index cfcb797cc40..3e7aeb5f90c 100644
--- a/src/java_bytecode/java_bytecode_language.cpp
+++ b/src/java_bytecode/java_bytecode_language.cpp
@@ -1091,6 +1091,11 @@ bool java_bytecode_languaget::to_expr(
   return true; // fail for now
 }
 
+symbol_typet java_bytecode_languaget::root_base_class_type()
+{
+  return to_symbol_type(java_lang_object_type().subtype());
+}
+
 java_bytecode_languaget::~java_bytecode_languaget()
 {
 }
diff --git a/src/java_bytecode/java_bytecode_language.h b/src/java_bytecode/java_bytecode_language.h
index 47d5fb69d82..268c5256fe2 100644
--- a/src/java_bytecode/java_bytecode_language.h
+++ b/src/java_bytecode/java_bytecode_language.h
@@ -127,6 +127,8 @@ class java_bytecode_languaget:public languaget
     exprt &expr,
     const namespacet &ns) override;
 
+  symbol_typet root_base_class_type() override;
+
   std::unique_ptr<languaget> new_language() override
   { return util_make_unique<java_bytecode_languaget>(); }
 
diff --git a/src/jsil/jsil_language.h b/src/jsil/jsil_language.h
index 8b902b86ded..b1419f5a9f7 100644
--- a/src/jsil/jsil_language.h
+++ b/src/jsil/jsil_language.h
@@ -60,6 +60,12 @@ class jsil_languaget:public languaget
     exprt &expr,
     const namespacet &ns) override;
 
+  virtual symbol_typet root_base_class_type() override
+  {
+    // unused
+    UNREACHABLE;
+  }
+
   virtual std::unique_ptr<languaget> new_language() override
   { return util_make_unique<jsil_languaget>(); }
 
diff --git a/src/langapi/language.h b/src/langapi/language.h
index 9e35daa17c9..6a7c5cecec5 100644
--- a/src/langapi/language.h
+++ b/src/langapi/language.h
@@ -156,6 +156,9 @@ class languaget:public messaget
     exprt &expr,
     const namespacet &ns)=0;
 
+  /// returns the class type that contains RTTI
+  virtual symbol_typet root_base_class_type() = 0;
+
   virtual std::unique_ptr<languaget> new_language()=0;
 
   void set_should_generate_opaque_method_stubs(bool should_generate_stubs);

From b3ba2cc13e7b0610cead0d09c314c790a905176f Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Sat, 17 Mar 2018 13:17:10 +0000
Subject: [PATCH 3/3] Remove Java dependency from remove_virtual_functions

---
 src/goto-programs/remove_virtual_functions.cpp | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp
index 2d543601cc7..64d091e12c6 100644
--- a/src/goto-programs/remove_virtual_functions.cpp
+++ b/src/goto-programs/remove_virtual_functions.cpp
@@ -321,6 +321,10 @@ void remove_virtual_functionst::get_child_functions_rec(
   if(findit==class_hierarchy.class_map.end())
     return;
 
+  const auto language = get_language_from_identifier(ns, this_id);
+  CHECK_RETURN(language);
+  const irep_idt root_base_class_type_name =
+    language->root_base_class_type().get_identifier();
   for(const auto &child : findit->second.children)
   {
     // Skip if we have already visited this and we found a function call that
@@ -330,7 +334,7 @@ void remove_virtual_functionst::get_child_functions_rec(
       it != entry_map.end() &&
       !has_prefix(
         id2string(it->second.symbol_expr.get_identifier()),
-        "java::java.lang.Object"))
+        id2string(root_base_class_type_name)))
     {
       continue;
     }