Merge pull request #4292 from owen-jones-diffblue/refactor-fields-of-symex-dereference-statet

Do not store ref to goto_symext in symex_dereference_statet

Author: owen-jones-diffblue

src/goto-symex/symex_clean_expr.cpp

@@ -122,7 +122,7 @@ process_array_expr(exprt &expr, bool do_simplify, const namespacet &ns)
 
 void goto_symext::process_array_expr(statet &state, exprt &expr)
 {
-  symex_dereference_statet symex_dereference_state(*this, state);
+  symex_dereference_statet symex_dereference_state(state, ns);
 
   value_set_dereferencet dereference(
     ns, state.symbol_table, symex_dereference_state, language_mode, false);

src/goto-symex/symex_dereference.cpp

@@ -224,7 +224,7 @@ void goto_symext::dereference_rec(exprt &expr, statet &state)
     dereference_rec(tmp1, state);
 
     // we need to set up some elaborate call-backs
-    symex_dereference_statet symex_dereference_state(*this, state);
+    symex_dereference_statet symex_dereference_state(state, ns);
 
     value_set_dereferencet dereference(
       ns,

src/goto-symex/symex_dereference_state.cpp

@@ -30,8 +30,6 @@ Author: Daniel Kroening, [email protected]
 const symbolt *
 symex_dereference_statet::get_or_create_failed_symbol(const exprt &expr)
 {
-  const namespacet &ns=goto_symex.ns;
-
   if(expr.id()==ID_symbol &&
      expr.get_bool(ID_C_SSA_symbol))
   {
@@ -86,24 +84,24 @@ void symex_dereference_statet::get_value_set(
   const exprt &expr,
   value_setst::valuest &value_set) const
 {
-  state.value_set.get_value_set(expr, value_set, goto_symex.ns);
+  state.value_set.get_value_set(expr, value_set, ns);
 
-  #if 0
+#if 0
   std::cout << "**************************\n";
   state.value_set.output(goto_symex.ns, std::cout);
   std::cout << "**************************\n";
-  #endif
+#endif
 
-  #if 0
+#if 0
   std::cout << "E: " << from_expr(goto_symex.ns, "", expr) << '\n';
-  #endif
+#endif
 
-  #if 0
+#if 0
   std::cout << "**************************\n";
   for(value_setst::valuest::const_iterator it=value_set.begin();
       it!=value_set.end();
       it++)
     std::cout << from_expr(goto_symex.ns, "", *it) << '\n';
   std::cout << "**************************\n";
-  #endif
+#endif
 }

src/goto-symex/symex_dereference_state.h

@@ -25,16 +25,14 @@ class symex_dereference_statet:
   public dereference_callbackt
 {
 public:
-  symex_dereference_statet(
-    const goto_symext &_goto_symex,
-    goto_symext::statet &_state)
-    : goto_symex(_goto_symex), state(_state)
+  symex_dereference_statet(goto_symext::statet &_state, const namespacet &ns)
+    : state(_state), ns(ns)
   {
   }
 
 protected:
-  const goto_symext &goto_symex;
   goto_symext::statet &state;
+  const namespacet &ns;
 
   void get_value_set(const exprt &expr, value_setst::valuest &value_set)
     const override;