Only update goto program if it was changed

Author: Owen Jones

jbmc/src/java_bytecode/convert_java_nondet.cpp

@@ -29,9 +29,11 @@ Author: Reuben Thomas, [email protected]
 /// \param target: One of the steps in that goto program.
 /// \param symbol_table: The global symbol table.
 /// \param message_handler: Handles logging.
-/// \param max_nondet_array_length: Maximum size of new nondet arrays.
-/// \return The next instruction to process with this function.
-static goto_programt::targett insert_nondet_init_code(
+/// \param object_factory_parameters: Parameters for the generation of nondet
+///   objects.
+/// \return The next instruction to process with this function and a boolean
+///   indicating whether any changes were made to the goto program.
+static std::pair<goto_programt::targett, bool> insert_nondet_init_code(
   goto_programt &goto_program,
   const goto_programt::targett &target,
   symbol_table_baset &symbol_table,
@@ -40,6 +42,7 @@ static goto_programt::targett insert_nondet_init_code(
   const irep_idt &mode)
 {
   const auto next_instr = std::next(target);
+  bool changed = false;
 
   // We only expect to find nondets in the rhs of an assignments or in return
   // statements
@@ -132,9 +135,11 @@ 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());
+
+    changed = true;
   }
 
-  return next_instr;
+  return std::make_pair(next_instr, changed);
 }
 
 /// For each instruction in the goto program, checks if it is an assignment from
@@ -151,20 +156,27 @@ void convert_nondet(
   const object_factory_parameterst &object_factory_parameters,
   const irep_idt &mode)
 {
-  for(auto instruction_iterator=goto_program.instructions.begin(),
-        end=goto_program.instructions.end();
-      instruction_iterator!=end;)
+  bool changed = false;
+  auto instruction_iterator = goto_program.instructions.begin();
+  auto end = goto_program.instructions.end();
+
+  while(instruction_iterator != end)
   {
-    instruction_iterator = insert_nondet_init_code(
+    auto ret = insert_nondet_init_code(
       goto_program,
       instruction_iterator,
       symbol_table,
       message_handler,
       object_factory_parameters,
       mode);
+    instruction_iterator = ret.first;
+    changed |= ret.second;
   }
 
-  goto_program.update();
+  if(changed)
+  {
+    goto_program.update();
+  }
 }
 
 void convert_nondet(