cbmc: remove dependency on java_bytecode

Author: kroening

src/cbmc/CMakeLists.txt

@@ -16,7 +16,6 @@ target_link_libraries(cbmc-lib
     goto-instrument-lib
     goto-programs
     goto-symex
-    java_bytecode
     json
     langapi
     linking

src/cbmc/Makefile

@@ -17,7 +17,6 @@ SRC = all_properties.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) \

src/cbmc/cbmc_parse_options.cpp

@@ -36,9 +36,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/mm_io.h>
 #include <goto-programs/read_goto_binary.h>
 #include <goto-programs/remove_function_pointers.h>
-#include <goto-programs/remove_instanceof.h>
 #include <goto-programs/remove_returns.h>
-#include <goto-programs/remove_exceptions.h>
 #include <goto-programs/remove_vector.h>
 #include <goto-programs/remove_complex.h>
 #include <goto-programs/remove_asm.h>
@@ -729,8 +727,6 @@ bool cbmc_parse_optionst::process_goto_program(
       get_message_handler(),
       goto_model,
       cmdline.isset("pointer-check"));
-    // remove catch and throw (introduces instanceof)
-    remove_exceptions(goto_model);
 
     mm_io(goto_model);
 

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -25,8 +25,6 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/set_properties.h>
 #include <goto-programs/remove_function_pointers.h>
 #include <goto-programs/remove_virtual_functions.h>
-#include <goto-programs/remove_exceptions.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>
@@ -45,6 +43,9 @@ Author: Daniel Kroening, [email protected]
 #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>
 

src/goto-diff/goto_diff_parse_options.cpp

@@ -29,9 +29,7 @@ Author: Peter Schrammel
 #include <goto-programs/mm_io.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_exceptions.h>
 #include <goto-programs/remove_vector.h>
 #include <goto-programs/remove_complex.h>
 #include <goto-programs/remove_asm.h>
@@ -54,6 +52,8 @@ Author: Peter Schrammel
 #include <pointer-analysis/add_failed_symbols.h>
 
 #include <java_bytecode/java_bytecode_language.h>
+#include <java_bytecode/remove_instanceof.h>
+#include <java_bytecode/remove_exceptions.h>
 
 #include <langapi/mode.h>
 

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -26,8 +26,6 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/remove_calls_no_body.h>
 #include <goto-programs/remove_function_pointers.h>
 #include <goto-programs/remove_virtual_functions.h>
-#include <goto-programs/remove_exceptions.h>
-#include <goto-programs/remove_instanceof.h>
 #include <goto-programs/remove_skip.h>
 #include <goto-programs/goto_inline.h>
 #include <goto-programs/show_properties.h>
@@ -51,6 +49,9 @@ Author: Daniel Kroening, [email protected]
 #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>

src/goto-programs/Makefile

@@ -43,9 +43,7 @@ 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 \

src/java_bytecode/Makefile

@@ -31,6 +31,8 @@ SRC = bytecode_info.cpp \
       java_types.cpp \
       java_utils.cpp \
       mz_zip_archive.cpp \
+      remove_exceptions.cpp \
+      remove_instanceof.cpp \
       select_pointer_type.cpp \
       # Empty last line
 

src/java_bytecode/ci_lazy_methods.cpp

@@ -5,16 +5,17 @@
  Author: Diffblue Ltd.
 
 \*******************************************************************/
+
 #include "ci_lazy_methods.h"
+#include "java_entry_point.h"
+#include "java_class_loader.h"
+#include "java_utils.h"
+#include "java_string_library_preprocess.h"
+#include "remove_exceptions.h"
 
-#include <java_bytecode/java_entry_point.h>
-#include <java_bytecode/java_class_loader.h>
-#include <java_bytecode/java_utils.h>
 #include <util/suffix.h>
-#include <java_bytecode/java_string_library_preprocess.h>
 
 #include <goto-programs/resolve_inherited_component.h>
-#include <goto-programs/remove_exceptions.h>
 
 /// Constructor for lazy-method loading
 /// \param symbol_table: the symbol table to use

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -20,6 +20,7 @@ Author: Daniel Kroening, [email protected]
 #include "java_string_library_preprocess.h"
 #include "java_types.h"
 #include "java_utils.h"
+#include "remove_exceptions.h"
 
 #include <util/arith_tools.h>
 #include <util/c_types.h>
@@ -34,7 +35,6 @@ Author: Daniel Kroening, [email protected]
 #include <linking/zero_initializer.h>
 
 #include <goto-programs/cfg.h>
-#include <goto-programs/remove_exceptions.h>
 #include <goto-programs/class_hierarchy.h>
 #include <goto-programs/resolve_inherited_component.h>
 #include <analyses/cfg_dominators.h>