Skip to content

Commit 908d29b

Browse files
Replace symex field by namespace
symex was only used for its namespace.
1 parent 12211bf commit 908d29b

File tree

3 files changed

+5
-7
lines changed

3 files changed

+5
-7
lines changed

src/goto-symex/symex_dereference.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -276,7 +276,7 @@ void goto_symext::dereference_rec(
276276
dereference_rec(tmp1, state, guard, false);
277277

278278
// we need to set up some elaborate call-backs
279-
symex_dereference_statet symex_dereference_state(*this, state);
279+
symex_dereference_statet symex_dereference_state(ns, state);
280280

281281
value_set_dereferencet dereference(
282282
ns,

src/goto-symex/symex_dereference_state.cpp

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -17,8 +17,6 @@ bool symex_dereference_statet::has_failed_symbol(
1717
const exprt &expr,
1818
const symbolt *&symbol)
1919
{
20-
const namespacet &ns=goto_symex.ns;
21-
2220
if(expr.id()==ID_symbol &&
2321
expr.get_bool(ID_C_SSA_symbol))
2422
{
@@ -72,7 +70,7 @@ void symex_dereference_statet::get_value_set(
7270
const exprt &expr,
7371
value_setst::valuest &value_set)
7472
{
75-
state.value_set.get_value_set(expr, value_set, goto_symex.ns);
73+
state.value_set.get_value_set(expr, value_set, ns);
7674

7775
#if 0
7876
std::cout << "**************************\n";

src/goto-symex/symex_dereference_state.h

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -21,15 +21,15 @@ class symex_dereference_statet:
2121
{
2222
public:
2323
symex_dereference_statet(
24-
goto_symext &_goto_symex,
24+
namespacet &ns,
2525
goto_symext::statet &_state):
26-
goto_symex(_goto_symex),
26+
ns(ns),
2727
state(_state)
2828
{
2929
}
3030

3131
protected:
32-
goto_symext &goto_symex;
32+
namespacet &ns;
3333
goto_symext::statet &state;
3434

3535
void get_value_set(

0 commit comments

Comments
 (0)