From c34be32177ca7728fc3d80f15ba66846236b8d32 Mon Sep 17 00:00:00 2001
From: Owen Jones <owen.jones@diffblue.com>
Date: Thu, 13 Apr 2017 12:19:51 +0100
Subject: [PATCH] Fix java argument input declarations

Previously, we would output code like this:
  INPUT("arg0i", NONDET(int));
  helloworld.fun:(I)I(NONDET(int));
We now output code like this instead:
  tmp_object_factory$1 = NONDET(int);
  INPUT("arg0i", tmp_object_factory$1);
  helloworld.fun:(I)I(tmp_object_factory$1);
This means that the correct value of the argument to helloworld() is
picked up. It also simplifies the code, as we now use the machinery
built to deal with pointers for all types, with just a minor tweak for
booleans.
---
 src/java_bytecode/java_object_factory.cpp | 59 ++++++++++-------------
 1 file changed, 25 insertions(+), 34 deletions(-)

diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp
index 34f5495bb85..4ab8055cf49 100644
--- a/src/java_bytecode/java_object_factory.cpp
+++ b/src/java_bytecode/java_object_factory.cpp
@@ -356,11 +356,13 @@ void java_object_factoryt::gen_nondet_init(
   }
   else
   {
-    side_effect_expr_nondett se=side_effect_expr_nondett(type);
+    exprt rhs=type.id()==ID_c_bool?
+      get_nondet_bool(type):
+      side_effect_expr_nondett(type);
+    code_assignt assign(expr, rhs);
+    assign.add_source_location()=loc;
 
-    code_assignt code(expr, se);
-    code.add_source_location()=loc;
-    init_code.copy_to_operands(code);
+    init_code.copy_to_operands(assign);
   }
 }
 
@@ -517,36 +519,25 @@ exprt object_factory(
   size_t max_nondet_array_length,
   const source_locationt &loc)
 {
-  if(type.id()==ID_pointer)
-  {
-    symbolt &aux_symbol=new_tmp_symbol(
-      symbol_table,
-      loc,
-      type);
-    aux_symbol.is_static_lifetime=true;
+  symbolt &aux_symbol=new_tmp_symbol(
+    symbol_table,
+    loc,
+    type);
+  aux_symbol.is_static_lifetime=true;
 
-    exprt object=aux_symbol.symbol_expr();
+  exprt object=aux_symbol.symbol_expr();
 
-    java_object_factoryt state(
-      init_code,
-      !allow_null,
-      max_nondet_array_length,
-      symbol_table);
-    state.gen_nondet_init(
-      object,
-      false,
-      "",
-      loc,
-      false);
-
-    return object;
-  }
-  else if(type.id()==ID_c_bool)
-  {
-    // We force this to 0 and 1 and won't consider
-    // other values.
-    return get_nondet_bool(type);
-  }
-  else
-    return side_effect_expr_nondett(type);
+  java_object_factoryt state(
+    init_code,
+    !allow_null,
+    max_nondet_array_length,
+    symbol_table);
+  state.gen_nondet_init(
+    object,
+    false,
+    "",
+    loc,
+    false);
+
+  return object;
 }