Use remove_java_new

Author: peterschrammel

src/jbmc/jbmc_parse_options.cpp

@@ -53,8 +53,9 @@ Author: Daniel Kroening, [email protected]
 
 #include <java_bytecode/java_bytecode_language.h>
 #include <java_bytecode/java_enum_static_init_unwind_handler.h>
-#include <java_bytecode/remove_instanceof.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 <cbmc/version.h>
@@ -763,6 +764,9 @@ void jbmc_parse_optionst::process_goto_function(
     // add generic checks
     goto_check(ns, options, ID_java, function.get_goto_function());
 
+    // Replace Java new side effects
+    remove_java_new(goto_function, symbol_table, get_message_handler());
+
     // checks don't know about adjusted float expressions
     adjust_float_expressions(goto_function, ns);
 

unit/pointer-analysis/custom_value_set_analysis.cpp

@@ -14,6 +14,7 @@ Author: Chris Smowton, [email protected]
 #include <goto-programs/goto_inline.h>
 #include <java_bytecode/java_bytecode_language.h>
 #include <java_bytecode/java_types.h>
+#include <java_bytecode/remove_java_new.h>
 #include <pointer-analysis/value_set_analysis.h>
 
 /// An example customised value_sett. It makes a series of small changes
@@ -183,6 +184,9 @@ SCENARIO("test_value_set_analysis",
     goto_modelt goto_model=
       initialize_goto_model(command_line, null_output);
 
+    null_message_handlert message_handler;
+    remove_java_new(goto_model, message_handler);
+
     namespacet ns(goto_model.symbol_table);
 
     // Fully inline the test program, to avoid VSA conflating