@@ -156,6 +156,24 @@ class goto_symex_is_constantt : public is_constantt
156
156
}
157
157
};
158
158
159
+ renamedt<ssa_exprt, L0>
160
+ goto_symex_statet::set_l0_indices (ssa_exprt ssa_expr, const namespacet &ns)
161
+ {
162
+ return level0 (std::move (ssa_expr), ns, source.thread_nr );
163
+ }
164
+
165
+ renamedt<ssa_exprt, L1>
166
+ goto_symex_statet::set_l1_indices (ssa_exprt ssa_expr, const namespacet &ns)
167
+ {
168
+ return level1 (level0 (std::move (ssa_expr), ns, source.thread_nr ));
169
+ }
170
+
171
+ renamedt<ssa_exprt, L2>
172
+ goto_symex_statet::set_l2_indices (ssa_exprt ssa_expr, const namespacet &ns)
173
+ {
174
+ return level2 (level1 (level0 (std::move (ssa_expr), ns, source.thread_nr )));
175
+ }
176
+
159
177
void goto_symex_statet::assignment (
160
178
ssa_exprt &lhs, // L0/L1
161
179
const exprt &rhs, // L2
@@ -236,24 +254,6 @@ void goto_symex_statet::assignment(
236
254
#endif
237
255
}
238
256
239
- renamedt<ssa_exprt, L0>
240
- goto_symex_statet::set_l0_indices (ssa_exprt ssa_expr, const namespacet &ns)
241
- {
242
- return level0 (std::move (ssa_expr), ns, source.thread_nr );
243
- }
244
-
245
- renamedt<ssa_exprt, L1>
246
- goto_symex_statet::set_l1_indices (ssa_exprt ssa_expr, const namespacet &ns)
247
- {
248
- return level1 (level0 (std::move (ssa_expr), ns, source.thread_nr ));
249
- }
250
-
251
- renamedt<ssa_exprt, L2>
252
- goto_symex_statet::set_l2_indices (ssa_exprt ssa_expr, const namespacet &ns)
253
- {
254
- return level2 (level1 (level0 (std::move (ssa_expr), ns, source.thread_nr )));
255
- }
256
-
257
257
template <levelt level>
258
258
ssa_exprt goto_symex_statet::rename_ssa (ssa_exprt ssa, const namespacet &ns)
259
259
{
0 commit comments