Address review comments

Author: Owen Jones

jbmc/src/java_bytecode/convert_java_nondet.cpp

@@ -59,12 +59,13 @@ static goto_programt::targett insert_nondet_init_code(
     const typet &type = side_effect.type();
     // If the lhs type doesn't have a subtype then I guess it's primitive and
     // we want to bail out now
-    if(!(type.id() == ID_pointer && type.has_subtype()))
+    if(type.id() != ID_pointer)
     {
       continue;
     }
 
-    // Although, if the type is a ptr-to-void then we also want to bail
+    // Although, if the type is a ptr-to-void or a function pointer then we also
+    // want to bail
     if(type.subtype().id() == ID_empty || type.subtype().id() == ID_code)
     {
       continue;
@@ -131,8 +132,6 @@ static goto_programt::targett insert_nondet_init_code(
     // Finally insert the dead instruction for aux_symbol after target
     goto_program.insert_after(target)->swap(
       aux_instructions.instructions.back());
-
-    goto_program.update();
   }
 
   return next_instr;
@@ -164,6 +163,9 @@ void convert_nondet(
       object_factory_parameters,
       mode);
   }
+
+  goto_program.update();
+
 }
 
 void convert_nondet(

jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp

@@ -95,7 +95,8 @@ void validate_nondet_method_removed(
 void validate_nondets_converted(
   std::list<goto_programt::instructiont> instructions)
 {
-  bool nondetExists = false, allocateExists = false;
+  bool nondet_exists = false;
+  bool allocate_exists = false;
   for(const auto &inst : instructions)
   {
     // Check that our NONDET(<type>) exists on a rhs somewhere.
@@ -110,18 +111,18 @@ void validate_nondets_converted(
       auto side_effect = to_side_effect_expr(target_expression);
       if(side_effect.get_statement() == ID_nondet)
       {
-        nondetExists = true;
+        nondet_exists = true;
       }
 
       if(side_effect.get_statement() == ID_allocate)
       {
-        allocateExists = true;
+        allocate_exists = true;
       }
     }
   }
 
-  REQUIRE(!nondetExists);
-  REQUIRE(allocateExists);
+  REQUIRE(!nondet_exists);
+  REQUIRE(allocate_exists);
 }
 
 void load_and_test_method(
@@ -174,12 +175,6 @@ void load_and_test_method(
 
     remove_returns(model_function, [](const irep_idt &) { return false; });
 
-    std::string output = "";
-    for(auto instruction : model_function.get_goto_function().body.instructions)
-    {
-      output += instruction.code.pretty(0, 0) + "\n\n\n";
-    }
-
     std::stringstream out;
     goto_function.body.output(namespacet(symbol_table), "", out);
     std::string res = out.str();
@@ -197,16 +192,6 @@ void load_and_test_method(
 
     remove_returns(model_function, [](const irep_idt &) { return false; });
 
-    std::string output = "";
-    for(auto instruction : model_function.get_goto_function().body.instructions)
-    {
-      output += instruction.code.pretty(0, 0) + "\n\n\n";
-    }
-
-    std::stringstream out;
-    goto_function.body.output(namespacet(symbol_table), "", out);
-    std::string res = out.str();
-
     validate_nondets_converted(goto_function.body.instructions);
   }
 }