Add remove_java_new pass to jdiff and janalyzer tools

Add the `remove_java_new` pass after `convert_java_nondet` to both
`jdiff` and `janalyzer`. This ensures that any new statements introduced
by `convert_java_nondet` are properly processed.

Fixes: #3094

Author: tautschnig

jbmc/src/janalyzer/janalyzer_parse_options.cpp

@@ -35,10 +35,13 @@ Author: Daniel Kroening, [email protected]
 #include <goto-analyzer/static_verifier.h>
 #include <goto-analyzer/taint_analysis.h>
 #include <goto-analyzer/unreachable_instructions.h>
+#include <java_bytecode/convert_java_nondet.h>
 #include <java_bytecode/java_bytecode_language.h>
+#include <java_bytecode/java_object_factory_parameters.h>
 #include <java_bytecode/lazy_goto_model.h>
 #include <java_bytecode/remove_exceptions.h>
 #include <java_bytecode/remove_instanceof.h>
+#include <java_bytecode/remove_java_new.h>
 #include <langapi/language.h>
 #include <langapi/mode.h>
 #include <linking/static_lifetime_init.h>
@@ -695,6 +698,19 @@ void janalyzer_parse_optionst::process_goto_function(
 
   remove_returns(function, function_is_stub);
 
+  // convert Java nondet expressions
+  java_object_factory_parameterst object_factory_parameters;
+  object_factory_parameters.set(options);
+  convert_nondet(
+    function, ui_message_handler, object_factory_parameters, ID_java);
+
+  // remove Java new expressions (must be after convert_nondet)
+  remove_java_new(
+    function.get_function_id(),
+    function.get_goto_function(),
+    symbol_table,
+    ui_message_handler);
+
   transform_assertions_assumptions(options, function.get_goto_function().body);
 }
 

jbmc/src/jdiff/jdiff_parse_options.cpp

@@ -33,9 +33,12 @@ Author: Peter Schrammel
 #include <goto-diff/change_impact.h>
 #include <goto-diff/unified_diff.h>
 #include <goto-instrument/cover.h>
+#include <java_bytecode/convert_java_nondet.h>
 #include <java_bytecode/java_bytecode_language.h>
+#include <java_bytecode/java_object_factory_parameters.h>
 #include <java_bytecode/remove_exceptions.h>
 #include <java_bytecode/remove_instanceof.h>
+#include <java_bytecode/remove_java_new.h>
 
 #include "java_syntactic_diff.h"
 
@@ -198,6 +201,14 @@ bool jdiff_parse_optionst::process_goto_program(
   // remove returns
   remove_returns(goto_model);
 
+  // convert Java nondet expressions
+  java_object_factory_parameterst object_factory_parameters;
+  object_factory_parameters.set(options);
+  convert_nondet(goto_model, ui_message_handler, object_factory_parameters);
+
+  // remove Java new expressions (must be after convert_nondet)
+  remove_java_new(goto_model, ui_message_handler);
+
   transform_assertions_assumptions(options, goto_model);
 
   // checks don't know about adjusted float expressions