From 0e5540963f1a866359c27879b5e4efa47640bfc6 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Sun, 30 Nov 2025 14:09:31 +0000
Subject: [PATCH] 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
---
 jbmc/src/janalyzer/janalyzer_parse_options.cpp | 16 ++++++++++++++++
 jbmc/src/jdiff/jdiff_parse_options.cpp         | 11 +++++++++++
 2 files changed, 27 insertions(+)

diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp
index 79b712d55d1..d6feafdc14e 100644
--- a/jbmc/src/janalyzer/janalyzer_parse_options.cpp
+++ b/jbmc/src/janalyzer/janalyzer_parse_options.cpp
@@ -35,10 +35,13 @@ Author: Daniel Kroening, kroening@kroening.com
 #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);
 }
 
diff --git a/jbmc/src/jdiff/jdiff_parse_options.cpp b/jbmc/src/jdiff/jdiff_parse_options.cpp
index 7575d35ef2c..095d9d056fe 100644
--- a/jbmc/src/jdiff/jdiff_parse_options.cpp
+++ b/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