Skip to content

Commit 35f8a82

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 2ff6a73 commit 35f8a82

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();
@@ -105,11 +104,9 @@ void goto_symext::symex_start_thread(statet &state)
105104
(symbol.is_extern && symbol.value.is_nil()))
106105
continue;
107106

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

114111
exprt rhs=symbol.value;
115112
if(rhs.is_nil())
@@ -122,7 +119,7 @@ void goto_symext::symex_start_thread(statet &state)
122119
guardt guard{true_exprt{}};
123120
symex_assign_symbol(
124121
state,
125-
lhs,
122+
l0_lhs.expr,
126123
nil_exprt(),
127124
rhs,
128125
guard,

0 commit comments

Comments
 (0)