Inline perform_symex utility functions

Only used once resp. obsolete.

Author: peterschrammel

src/goto-checker/bmc_util.cpp

@@ -329,44 +329,3 @@ void postprocess_equation(
     symex.validate(validation_modet::INVARIANT);
   }
 }
-
-void perform_symex(
-  abstract_goto_modelt &goto_model,
-  symex_bmct &symex,
-  symbol_tablet &symex_symbol_table,
-  symex_target_equationt &equation,
-  const optionst &options,
-  const namespacet &ns,
-  ui_message_handlert &ui_message_handler)
-{
-  auto get_goto_function =
-    [&goto_model](
-      const irep_idt &id) -> const goto_functionst::goto_functiont & {
-    return goto_model.get_goto_function(id);
-  };
-
-  symex.symex_from_entry_point_of(get_goto_function, symex_symbol_table);
-
-  postprocess_equation(symex, equation, options, ns, ui_message_handler);
-}
-
-void perform_symex(
-  abstract_goto_modelt &goto_model,
-  symex_bmct &symex,
-  path_storaget::patht &resume,
-  symbol_tablet &symex_symbol_table,
-  const optionst &options,
-  const namespacet &ns,
-  ui_message_handlert &ui_message_handler)
-{
-  auto get_goto_function =
-    [&goto_model](
-      const irep_idt &id) -> const goto_functionst::goto_functiont & {
-    return goto_model.get_goto_function(id);
-  };
-
-  symex.resume_symex_from_saved_state(
-    get_goto_function, resume.state, &resume.equation, symex_symbol_table);
-
-  postprocess_equation(symex, resume.equation, options, ns, ui_message_handler);
-}

src/goto-checker/bmc_util.h

@@ -81,26 +81,6 @@ void postprocess_equation(
   const namespacet &ns,
   ui_message_handlert &ui_message_handler);
 
-/// Perform symbolic execution from the entry point
-void perform_symex(
-  abstract_goto_modelt &,
-  symex_bmct &,
-  symbol_tablet &,
-  symex_target_equationt &,
-  const optionst &,
-  const namespacet &,
-  ui_message_handlert &);
-
-/// Perform symbolic execution starting from \p resume.
-void perform_symex(
-  abstract_goto_modelt &,
-  symex_bmct &,
-  path_storaget::patht &resume,
-  symbol_tablet &,
-  const optionst &,
-  const namespacet &,
-  ui_message_handlert &);
-
 /// Output a coverage report as generated by \ref symex_coveraget
 /// if \p cov_out is non-empty.
 /// \param cov_out: file to write the report to; no report is generated

src/goto-checker/multi_path_symex_checker.cpp

@@ -41,14 +41,13 @@ operator()(propertiest &properties)
   // we haven't got an equation yet
   if(!equation_generated)
   {
-    perform_symex(
-      goto_model,
-      symex,
-      symex_symbol_table,
-      equation,
-      options,
-      ns,
-      ui_message_handler);
+    auto get_goto_function =
+      [this](const irep_idt &id) -> const goto_functionst::goto_functiont & {
+      return goto_model.get_goto_function(id);
+    };
+
+    symex.symex_from_entry_point_of(get_goto_function, symex_symbol_table);
+    postprocess_equation(symex, equation, options, ns, ui_message_handler);
 
     output_coverage_report(
       options.get_option("symex-coverage-report"),

src/goto-checker/multi_path_symex_only_checker.cpp

@@ -39,14 +39,13 @@ multi_path_symex_only_checkert::multi_path_symex_only_checkert(
 incremental_goto_checkert::resultt multi_path_symex_only_checkert::
 operator()(propertiest &properties)
 {
-  perform_symex(
-    goto_model,
-    symex,
-    symex_symbol_table,
-    equation,
-    options,
-    ns,
-    ui_message_handler);
+  auto get_goto_function =
+    [this](const irep_idt &id) -> const goto_functionst::goto_functiont & {
+    return goto_model.get_goto_function(id);
+  };
+
+  symex.symex_from_entry_point_of(get_goto_function, symex_symbol_table);
+  postprocess_equation(symex, equation, options, ns, ui_message_handler);
 
   output_coverage_report(
     options.get_option("symex-coverage-report"),