Skip to content

Commit cae37d9

Browse files
author
Owen
committed
Do not store ref to goto_symext in symex_dereference_statet
The `goto_symext &` was only used to access a namespace. Just store a `namespacet &` instead.
1 parent dc4611f commit cae37d9

File tree

4 files changed

+6
-10
lines changed

4 files changed

+6
-10
lines changed

src/goto-symex/symex_clean_expr.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -122,7 +122,7 @@ process_array_expr(exprt &expr, bool do_simplify, const namespacet &ns)
122122

123123
void goto_symext::process_array_expr(statet &state, exprt &expr)
124124
{
125-
symex_dereference_statet symex_dereference_state(*this, state);
125+
symex_dereference_statet symex_dereference_state(state, ns);
126126

127127
value_set_dereferencet dereference(
128128
ns, state.symbol_table, symex_dereference_state, language_mode, false);

src/goto-symex/symex_dereference.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -224,7 +224,7 @@ void goto_symext::dereference_rec(exprt &expr, statet &state)
224224
dereference_rec(tmp1, state);
225225

226226
// we need to set up some elaborate call-backs
227-
symex_dereference_statet symex_dereference_state(*this, state);
227+
symex_dereference_statet symex_dereference_state(state, ns);
228228

229229
value_set_dereferencet dereference(
230230
ns,

src/goto-symex/symex_dereference_state.cpp

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -30,8 +30,6 @@ Author: Daniel Kroening, [email protected]
3030
const symbolt *
3131
symex_dereference_statet::get_or_create_failed_symbol(const exprt &expr)
3232
{
33-
const namespacet &ns=goto_symex.ns;
34-
3533
if(expr.id()==ID_symbol &&
3634
expr.get_bool(ID_C_SSA_symbol))
3735
{
@@ -86,7 +84,7 @@ void symex_dereference_statet::get_value_set(
8684
const exprt &expr,
8785
value_setst::valuest &value_set) const
8886
{
89-
state.value_set.get_value_set(expr, value_set, goto_symex.ns);
87+
state.value_set.get_value_set(expr, value_set, ns);
9088

9189
#if 0
9290
std::cout << "**************************\n";

src/goto-symex/symex_dereference_state.h

Lines changed: 3 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -25,16 +25,14 @@ class symex_dereference_statet:
2525
public dereference_callbackt
2626
{
2727
public:
28-
symex_dereference_statet(
29-
const goto_symext &_goto_symex,
30-
goto_symext::statet &_state)
31-
: goto_symex(_goto_symex), state(_state)
28+
symex_dereference_statet(goto_symext::statet &_state, const namespacet &ns)
29+
: state(_state), ns(ns)
3230
{
3331
}
3432

3533
protected:
36-
const goto_symext &goto_symex;
3734
goto_symext::statet &state;
35+
const namespacet &ns;
3836

3937
void get_value_set(const exprt &expr, value_setst::valuest &value_set)
4038
const override;

0 commit comments

Comments
 (0)