remove_skip includes goto_{program,functions}.update(), avoid redundant calls

Author: tautschnig

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -983,7 +983,6 @@ bool jbmc_parse_optionst::process_goto_functions(
 
     // remove any skips introduced since coverage instrumentation
     remove_skip(goto_model);
-    goto_model.goto_functions.update();
   }
 
   catch(const char *e)

src/goto-analyzer/static_simplifier.cpp

@@ -158,16 +158,13 @@ bool static_simplifier(
     m.status() << "Removing unreachable instructions" << messaget::eom;
 
     // Removes goto false
-    remove_skip(goto_model.goto_functions);
-    goto_model.goto_functions.update();
+    remove_skip(goto_model);
 
     // Convert unreachable to skips
     remove_unreachable(goto_model.goto_functions);
-    goto_model.goto_functions.update();
 
     // Remove all of the new skips
-    remove_skip(goto_model.goto_functions);
-    goto_model.goto_functions.update();
+    remove_skip(goto_model);
   }
 
   // restore return types before writing the binary

src/goto-diff/change_impact.cpp

@@ -132,7 +132,6 @@ void full_slicert::operator()(
 
   // remove the skips
   remove_skip(goto_functions);
-  goto_functions.update();
 }
 
 

src/goto-diff/goto_diff_parse_options.cpp

@@ -445,7 +445,6 @@ bool goto_diff_parse_optionst::process_goto_program(
 
     // remove any skips introduced since coverage instrumentation
     remove_skip(goto_model);
-    goto_model.goto_functions.update();
   }
 
   catch(const char *e)

src/goto-instrument/accelerate/scratch_program.cpp

@@ -29,7 +29,6 @@ bool scratch_programt::check_sat(bool do_slice)
   add_instruction(END_FUNCTION);
 
   remove_skip(*this);
-  update();
 
 #ifdef DEBUG
   std::cout << "Checking following program for satness:\n";

src/goto-instrument/full_slicer.cpp

@@ -364,7 +364,6 @@ void full_slicert::operator()(
 
   // remove the skips
   remove_skip(goto_functions);
-  goto_functions.update();
 }
 
 void full_slicer(

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -707,7 +707,6 @@ int goto_instrument_parse_optionst::doit()
       accelerate_functions(
         goto_model, get_message_handler(), cmdline.isset("z3"));
       remove_skip(goto_model);
-      goto_model.goto_functions.update();
     }
 
     if(cmdline.isset("horn-encoding"))

src/goto-instrument/model_argc_argv.cpp

@@ -182,8 +182,6 @@ bool model_argc_argv(
 
   // update counters etc.
   remove_skip(start);
-  start.compute_loop_numbers();
-  goto_model.goto_functions.update();
 
   return false;
 }

src/goto-instrument/reachability_slicer.cpp

@@ -206,7 +206,6 @@ void reachability_slicert::slice(goto_functionst &goto_functions)
 
   // remove the skips
   remove_skip(goto_functions);
-  goto_functions.update();
 }
 
 /// Perform reachability slicing on goto_model, with respect to the

src/goto-programs/remove_function_pointers.cpp

@@ -451,10 +451,7 @@ bool remove_function_pointerst::remove_function_pointers(
     }
 
   if(did_something)
-  {
     remove_skip(goto_program);
-    goto_program.update();
-  }
 
   return did_something;
 }

src/goto-programs/slice_global_inits.cpp

@@ -88,5 +88,4 @@ void slice_global_inits(goto_modelt &goto_model)
   }
 
   remove_skip(goto_functions);
-  goto_functions.update();
 }