Remove 'erase' in replace_java_nondet.cpp

Erasing a range of instructions from a goto program can cause memory
bugs when `goto_program::update` is called. Specifically, if any of the
remaining nodes in the program have elements of `targets` which point
into the erased range, then the program may attempt an invalid read
during the `update` call.

To avoid this, I thought of two options:

- check through the goto-program for instructions with `target`s that
  point into the removed range, and remove those `target`s, or
- just replace the existing instructions with no-ops.

Although I think the first solution is better, I can't think of a good
way of doing it with acceptable complexity, so this patch implements the
second option.

Author: reuk

src/goto-programs/replace_java_nondet.cpp

@@ -215,9 +215,9 @@ Function: check_and_replace_target
 
 \*******************************************************************/
 
-static goto_programt::const_targett check_and_replace_target(
+static goto_programt::targett check_and_replace_target(
   goto_programt &goto_program,
-  const goto_programt::const_targett &target)
+  const goto_programt::targett &target)
 {
   // Check whether this is a nondet library method, and return if not
   const auto instr_info=get_nondet_instruction_info(target);
@@ -241,7 +241,7 @@ static goto_programt::const_targett check_and_replace_target(
     to_symbol_expr(next_instr_assign_lhs).get_identifier();
 
   auto &instructions=goto_program.instructions;
-  const auto end=instructions.cend();
+  const auto end=instructions.end();
 
   // Look for an instruction where this name is on the RHS of an assignment
   const auto matching_assignment=std::find_if(
@@ -263,10 +263,15 @@ static goto_programt::const_targett check_and_replace_target(
   const auto after_matching_assignment=std::next(matching_assignment);
   assert(after_matching_assignment!=end);
 
-  const auto after_erased=goto_program.instructions.erase(
-    target, after_matching_assignment);
+  std::for_each(
+    target,
+    after_matching_assignment,
+    [](goto_programt::instructiont &instr)
+    {
+      instr.make_skip();
+    });
 
-  const auto inserted=goto_program.insert_before(after_erased);
+  const auto inserted=goto_program.insert_before(after_matching_assignment);
   inserted->make_assignment();
   side_effect_expr_nondett inserted_expr(nondet_var.type());
   inserted_expr.set_nullable(
@@ -278,7 +283,7 @@ static goto_programt::const_targett check_and_replace_target(
 
   goto_program.update();
 
-  return after_erased;
+  return after_matching_assignment;
 }
 
 /*******************************************************************\
@@ -297,8 +302,8 @@ Function: replace_java_nondet
 
 static void replace_java_nondet(goto_programt &goto_program)
 {
-  for(auto instruction_iterator=goto_program.instructions.cbegin(),
-        end=goto_program.instructions.cend();
+  for(auto instruction_iterator=goto_program.instructions.begin(),
+        end=goto_program.instructions.end();
       instruction_iterator!=end;)
   {
     instruction_iterator=check_and_replace_target(