Merge pull request #362 from tautschnig/no-get-mutable

Replace get_mutable by goto_programt API function

Author: Daniel Kroening

src/goto-instrument/unwind.cpp

@@ -244,7 +244,7 @@ void goto_unwindt::unwind(
       goto_programt::targett t_goto=goto_program.insert_before(loop_exit);
       unwind_log.insert(t_goto, loop_exit->location_number);
 
-      t_goto->make_goto(get_mutable(goto_program, loop_exit));
+      t_goto->make_goto(goto_program.const_cast_target(loop_exit));
       t_goto->source_location=loop_exit->source_location;
       t_goto->function=loop_exit->function;
       t_goto->guard=true_exprt();
@@ -269,7 +269,8 @@ void goto_unwindt::unwind(
 
     // re-direct any branches that go to loop_head to loop_iter
 
-    for(goto_programt::targett t=get_mutable(goto_program, loop_head);
+    for(goto_programt::targett
+        t=goto_program.const_cast_target(loop_head);
         t!=loop_iter; t++)
     {
       if(!t->is_goto())

src/goto-instrument/unwind.h

@@ -117,13 +117,6 @@ class goto_unwindt
     const goto_programt::const_targett start,
     const goto_programt::const_targett end, // exclusive
     goto_programt &goto_program); // result
-
-  goto_programt::targett get_mutable(
-    goto_programt &goto_program,
-    const goto_programt::const_targett t) const
-  {
-    return goto_program.instructions.erase(t, t);
-  }
 };
 
 #endif // CPROVER_GOTO_INSTRUMENT_UNWIND_H

src/goto-programs/goto_program_template.h

@@ -248,6 +248,19 @@ class goto_program_templatet
   //! The list of instructions in the goto program
   instructionst instructions;
 
+  // Convert a const_targett to a targett - use with care and avoid
+  // whenever possible
+  targett const_cast_target(const_targett t)
+  {
+    return instructions.erase(t, t);
+  }
+
+  // Dummy for templates with possible const contexts
+  const_targett const_cast_target(const_targett t) const
+  {
+    return t;
+  }
+
   void get_successors(
     targett target,
     targetst &successors);