diff --git a/src/goto-symex/symex_clean_expr.cpp b/src/goto-symex/symex_clean_expr.cpp index ad8e87465ef..05b497e0350 100644 --- a/src/goto-symex/symex_clean_expr.cpp +++ b/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); diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp index 552ad65b4ef..d098466b5c3 100644 --- a/src/goto-symex/symex_dereference.cpp +++ b/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, diff --git a/src/goto-symex/symex_dereference_state.cpp b/src/goto-symex/symex_dereference_state.cpp index 6cf0d0dce1c..b224759ab93 100644 --- a/src/goto-symex/symex_dereference_state.cpp +++ b/src/goto-symex/symex_dereference_state.cpp @@ -30,8 +30,6 @@ Author: Daniel Kroening, kroening@kroening.com 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 } diff --git a/src/goto-symex/symex_dereference_state.h b/src/goto-symex/symex_dereference_state.h index 82df24efb42..b0c0e15682a 100644 --- a/src/goto-symex/symex_dereference_state.h +++ b/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;