Add perform_symex for resuming from state

Author: peterschrammel

src/goto-checker/bmc_util.cpp

@@ -343,3 +343,25 @@ void perform_symex(
 
   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);
+  };
+
+  // perform symbolic execution
+  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

@@ -15,6 +15,7 @@ Author: Daniel Kroening, Peter Schrammel
 #include <memory>
 
 #include <goto-programs/safety_checker.h>
+#include <goto-symex/path_storage.h>
 
 #include "properties.h"
 
@@ -79,6 +80,16 @@ void perform_symex(
   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 &);
+
 void output_coverage_report(
   const std::string &cov_out,
   const abstract_goto_modelt &goto_model,