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.

Author: Owen Jones

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;
 }