Address (some) review comments

Author: Owen Jones

jbmc/src/java_bytecode/convert_java_nondet.cpp

@@ -75,13 +75,14 @@ static std::pair<goto_programt::targett, bool> insert_nondet_init_code(
       continue;
     }
 
-    // Check whether the nondet object may be null
     if(!to_side_effect_expr_nondet(side_effect).get_nullable())
       object_factory_parameters.max_nonnull_tree_depth = 1;
+
     // Get the symbol to nondet-init
     const auto source_loc = target->source_location;
 
-    // Create aux symbol for nondet object
+    // Create symbol for storing nondet object. We will replace `op` with this
+    // symbol.
     symbolt &aux_symbol = get_fresh_aux_symbol(
       type,
       id2string(goto_programt::get_function_id(goto_program)),
@@ -103,20 +104,19 @@ static std::pair<goto_programt::targett, bool> insert_nondet_init_code(
       aux_block, symbol_table, aux_instructions, message_handler, mode);
     CHECK_RETURN(aux_instructions.instructions.size() == 2);
 
-    // Generate nondet init code
     code_blockt init_code;
 
+    const bool skip_classid = true;
     gen_nondet_init(
       aux_symbol_expr,
       init_code,
       symbol_table,
       source_loc,
-      true,
+      skip_classid,
       allocation_typet::DYNAMIC,
       object_factory_parameters,
       update_in_placet::NO_UPDATE_IN_PLACE);
 
-    // Convert this code into goto instructions
     goto_programt nondet_init_instructions;
     goto_convert(
       init_code, symbol_table, nondet_init_instructions, message_handler, mode);

jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp

@@ -121,7 +121,7 @@ void validate_nondets_converted(
     }
   }
 
-  REQUIRE(!nondet_exists);
+  REQUIRE_FALSE(nondet_exists);
   REQUIRE(allocate_exists);
 }
 
@@ -145,7 +145,7 @@ void load_and_test_method(
   remove_virtual_functions(model_function);
 
   // Then test both situations.
-  THEN("Replace nondet should work when remove returns has been called.")
+  THEN("Replace nondet should work after remove returns has been called.")
   {
     remove_returns(model_function, [](const irep_idt &) { return false; });
 
@@ -154,7 +154,7 @@ void load_and_test_method(
     validate_nondet_method_removed(goto_function.body.instructions);
   }
 
-  THEN("Replace nondet should work when remove returns hasn't been called.")
+  THEN("Replace nondet should work before remove returns has been called.")
   {
     replace_java_nondet(model_function);
 
@@ -166,24 +166,20 @@ void load_and_test_method(
   object_factory_parameterst params{};
 
   THEN(
-    "Replace and convert nondet should work when remove returns has been "
+    "Replace and convert nondet should work after remove returns has been "
     "called.")
   {
+    remove_returns(model_function, [](const irep_idt &) { return false; });
+
     replace_java_nondet(model_function);
 
     convert_nondet(model_function, null_message_handler, params, ID_java);
 
-    remove_returns(model_function, [](const irep_idt &) { return false; });
-
-    std::stringstream out;
-    goto_function.body.output(namespacet(symbol_table), "", out);
-    std::string res = out.str();
-
     validate_nondets_converted(goto_function.body.instructions);
   }
 
   THEN(
-    "Replace and convert nondet should work when remove returns hasn't been "
+    "Replace and convert nondet should work before remove returns has been "
     "called.")
   {
     replace_java_nondet(model_function);