Skip to content

Commit caa3289

Browse files
Use rename_ssa 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 0bd3e06 commit caa3289

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();
@@ -108,11 +107,9 @@ void goto_symext::symex_start_thread(statet &state)
108107
(symbol.is_extern && symbol.value.is_nil()))
109108
continue;
110109

111-
// get original name
112-
ssa_exprt lhs(symbol.symbol_expr());
113-
114110
// get L0 name for current thread
115-
lhs.set_level_0(t);
111+
const renamedt<ssa_exprt, L0> l0_lhs =
112+
state.rename_ssa<L0>(ssa_exprt{symbol.symbol_expr()}, ns);
116113

117114
exprt rhs=symbol.value;
118115
if(rhs.is_nil())
@@ -125,7 +122,7 @@ void goto_symext::symex_start_thread(statet &state)
125122
guardt guard{true_exprt{}};
126123
symex_assign_symbol(
127124
state,
128-
lhs,
125+
l0_lhs.value,
129126
nil_exprt(),
130127
rhs,
131128
guard,

0 commit comments

Comments
 (0)