From 692f92d3eb6f786d0c93eb1bab2066b5ae54da06 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <kroening@cs.ox.ac.uk>
Date: Sat, 21 Apr 2018 13:58:08 +0100
Subject: [PATCH] remove dependency on java_bytecode

---
 src/goto-cc/Makefile                                  | 1 -
 src/goto-cc/goto_cc_languages.cpp                     | 2 --
 src/goto-instrument/Makefile                          | 1 -
 src/goto-instrument/goto_instrument_languages.cpp     | 2 --
 src/goto-instrument/goto_instrument_parse_options.cpp | 8 --------
 5 files changed, 14 deletions(-)

diff --git a/src/goto-cc/Makefile b/src/goto-cc/Makefile
index 374ed507b44..6874910fbcc 100644
--- a/src/goto-cc/Makefile
+++ b/src/goto-cc/Makefile
@@ -24,7 +24,6 @@ OBJ += ../big-int/big-int$(LIBEXT) \
       ../linking/linking$(LIBEXT) \
       ../ansi-c/ansi-c$(LIBEXT) \
       ../cpp/cpp$(LIBEXT) \
-      ../java_bytecode/java_bytecode$(LIBEXT) \
       ../xmllang/xmllang$(LIBEXT) \
       ../assembler/assembler$(LIBEXT) \
       ../langapi/langapi$(LIBEXT) \
diff --git a/src/goto-cc/goto_cc_languages.cpp b/src/goto-cc/goto_cc_languages.cpp
index 12ea70c04e7..c3246b5b8f1 100644
--- a/src/goto-cc/goto_cc_languages.cpp
+++ b/src/goto-cc/goto_cc_languages.cpp
@@ -15,7 +15,6 @@ Author: CM Wintersteiger
 
 #include <ansi-c/ansi_c_language.h>
 #include <cpp/cpp_language.h>
-#include <java_bytecode/java_bytecode_language.h>
 #include <jsil/jsil_language.h>
 
 #ifdef HAVE_SPECC
@@ -26,7 +25,6 @@ void goto_cc_modet::register_languages()
 {
   register_language(new_ansi_c_language);
   register_language(new_cpp_language);
-  register_language(new_java_bytecode_language);
   register_language(new_jsil_language);
 
   #ifdef HAVE_SPECC
diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile
index 9fe42bddd18..bb4ff425daf 100644
--- a/src/goto-instrument/Makefile
+++ b/src/goto-instrument/Makefile
@@ -75,7 +75,6 @@ SRC = accelerate/accelerate.cpp \
 
 OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../cpp/cpp$(LIBEXT) \
-      ../java_bytecode/java_bytecode$(LIBEXT) \
       ../linking/linking$(LIBEXT) \
       ../big-int/big-int$(LIBEXT) \
       ../goto-programs/goto-programs$(LIBEXT) \
diff --git a/src/goto-instrument/goto_instrument_languages.cpp b/src/goto-instrument/goto_instrument_languages.cpp
index cf0731573ac..a52628601e6 100644
--- a/src/goto-instrument/goto_instrument_languages.cpp
+++ b/src/goto-instrument/goto_instrument_languages.cpp
@@ -15,11 +15,9 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <ansi-c/ansi_c_language.h>
 #include <cpp/cpp_language.h>
-#include <java_bytecode/java_bytecode_language.h>
 
 void goto_instrument_parse_optionst::register_languages()
 {
   register_language(new_ansi_c_language);
   register_language(new_cpp_language);
-  register_language(new_java_bytecode_language);
 }
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index 61c5f1265ca..4a95d96e9f2 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -49,9 +49,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <pointer-analysis/add_failed_symbols.h>
 #include <pointer-analysis/show_value_sets.h>
 
-#include <java_bytecode/remove_exceptions.h>
-#include <java_bytecode/remove_instanceof.h>
-
 #include <analyses/natural_loops.h>
 #include <analyses/global_may_alias.h>
 #include <analyses/local_bitvector_analysis.h>
@@ -841,11 +838,6 @@ void goto_instrument_parse_optionst::do_indirect_call_and_rtti_removal(
     cmdline.isset("pointer-check"));
   status() << "Virtual function removal" << eom;
   remove_virtual_functions(goto_model);
-  status() << "Catch and throw removal" << eom;
-  // This introduces instanceof, so order is important:
-  remove_exceptions(goto_model);
-  status() << "Java instanceof removal" << eom;
-  remove_instanceof(goto_model);
 }
 
 /// Remove function pointers that can be resolved by analysing const variables