Skip to content

Commit a037292

Browse files
Use rename_level0 instead of set_level
The set_level function shouldn't be called directly outside of the implementation of the rename function. This will make how expressions are transformed from one level to the other clearer and more abstract.
1 parent f91b1eb commit a037292

File tree

1 file changed

+3
-6
lines changed

1 file changed

+3
-6
lines changed

src/goto-symex/symex_start_thread.cpp

Lines changed: 3 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -36,7 +36,6 @@ void goto_symext::symex_start_thread(statet &state)
3636
instruction.get_target();
3737

3838
// put into thread vector
39-
std::size_t t=state.threads.size();
4039
state.threads.push_back(statet::threadt());
4140
// statet::threadt &cur_thread=state.threads[state.source.thread_nr];
4241
statet::threadt &new_thread=state.threads.back();
@@ -107,11 +106,9 @@ void goto_symext::symex_start_thread(statet &state)
107106
(symbol.is_extern && symbol.value.is_nil()))
108107
continue;
109108

110-
// get original name
111-
ssa_exprt lhs(symbol.symbol_expr());
112-
113109
// get L0 name for current thread
114-
lhs.set_level_0(t);
110+
const level0t<ssa_exprt> l0_lhs =
111+
state.rename_level0(symbol.symbol_expr(), ns);
115112

116113
exprt rhs=symbol.value;
117114
if(rhs.is_nil())
@@ -124,7 +121,7 @@ void goto_symext::symex_start_thread(statet &state)
124121
guardt guard{true_exprt{}};
125122
symex_assign_symbol(
126123
state,
127-
lhs,
124+
l0_lhs.expr,
128125
nil_exprt(),
129126
rhs,
130127
guard,

0 commit comments

Comments
 (0)