Skip to content
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.

Commit 9a0f990

Browse files
committedMar 5, 2019
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 95a8dbc commit 9a0f990

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)
Please sign in to comment.