Remove obsolete variant of symex_with_state

This variant did not support lazy loading
and was only used by scratch_program,
which can as well use the more general variant.

Author: peterschrammel

src/goto-instrument/accelerate/scratch_program.cpp

@@ -35,7 +35,12 @@ bool scratch_programt::check_sat(bool do_slice)
   output(ns, "scratch", std::cout);
 #endif
 
-  symex.symex_with_state(symex_state, functions, symex_symbol_table);
+  symex.symex_with_state(
+    symex_state,
+    [this](const irep_idt &key) -> const goto_functionst::goto_functiont & {
+      return functions.function_map.at(key);
+    },
+    symex_symbol_table);
 
   if(do_slice)
   {

src/goto-symex/goto_symex.h

@@ -15,7 +15,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/options.h>
 #include <util/message.h>
 
-#include <goto-programs/goto_functions.h>
+#include <goto-programs/abstract_goto_model.h>
 
 #include "goto_symex_state.h"
 #include "path_storage.h"
@@ -97,6 +97,9 @@ class goto_symext
     std::function<const goto_functionst::goto_functiont &(const irep_idt &)>
     get_goto_functiont;
 
+  /// Return a function to get/load a goto function from the given goto model
+  static get_goto_functiont get_goto_function(abstract_goto_modelt &);
+
   /// \brief symex entire program starting from entry point
   ///
   /// The state that goto_symext maintains has a large memory footprint.
@@ -117,18 +120,6 @@ class goto_symext
     symex_target_equationt *saved_equation,
     symbol_tablet &new_symbol_table);
 
-  //// \brief symex entire program starting from entry point
-  ///
-  /// This method uses the `state` argument as the symbolic execution
-  /// state, which is useful for examining the state after this method
-  /// returns. The state that goto_symext maintains has a large memory
-  /// footprint, so if keeping the state around is not necessary,
-  /// clients should instead call goto_symext::symex_from_entry_point_of().
-  virtual void symex_with_state(
-    statet &,
-    const goto_functionst &,
-    symbol_tablet &);
-
   //// \brief symex entire program starting from entry point
   ///
   /// This method uses the `state` argument as the symbolic execution

src/goto-symex/symex_main.cpp

@@ -229,26 +229,6 @@ void goto_symext::symex_threaded_step(
   }
 }
 
-static goto_symext::get_goto_functiont get_function_from_goto_functions(
-  const goto_functionst &goto_functions)
-{
-  return [&goto_functions](
-           const irep_idt &key) -> const goto_functionst::goto_functiont & {
-    return goto_functions.function_map.at(key);
-  };
-}
-
-void goto_symext::symex_with_state(
-  statet &state,
-  const goto_functionst &goto_functions,
-  symbol_tablet &new_symbol_table)
-{
-  symex_with_state(
-    state,
-    get_function_from_goto_functions(goto_functions),
-    new_symbol_table);
-}
-
 void goto_symext::symex_with_state(
   statet &state,
   const get_goto_functiont &get_goto_function,
@@ -354,6 +334,15 @@ void goto_symext::symex_from_entry_point_of(
     state, get_goto_function, new_symbol_table);
 }
 
+goto_symext::get_goto_functiont
+goto_symext::get_goto_function(abstract_goto_modelt &goto_model)
+{
+  return [&goto_model](
+           const irep_idt &id) -> const goto_functionst::goto_functiont & {
+    return goto_model.get_goto_function(id);
+  };
+}
+
 /// do just one step
 void goto_symext::symex_step(
   const get_goto_functiont &get_goto_function,