@@ -246,15 +246,18 @@ static void set_l0_indices(
246
246
level0 (ssa_expr, ns, thread_nr);
247
247
}
248
248
249
- void goto_symex_statet::set_l1_indices (
249
+ static void set_l1_indices (
250
+ symex_level0t level0,
251
+ symex_level1t level1,
250
252
ssa_exprt &ssa_expr,
253
+ unsigned int thread_nr,
251
254
const namespacet &ns)
252
255
{
253
256
if (!ssa_expr.get_level_2 ().empty ())
254
257
return ;
255
258
if (!ssa_expr.get_level_1 ().empty ())
256
259
return ;
257
- level0 (ssa_expr, ns, source. thread_nr );
260
+ level0 (ssa_expr, ns, thread_nr);
258
261
level1 (ssa_expr);
259
262
}
260
263
@@ -289,13 +292,13 @@ void goto_symex_statet::rename(
289
292
}
290
293
else if (level == L1)
291
294
{
292
- set_l1_indices (ssa, ns);
295
+ set_l1_indices (level0, level1, ssa, source. thread_nr , ns);
293
296
rename (expr.type (), ssa.get_identifier (), ns, level);
294
297
ssa.update_type ();
295
298
}
296
299
else if (level==L2)
297
300
{
298
- set_l1_indices (ssa, ns);
301
+ set_l1_indices (level0, level1, ssa, source. thread_nr , ns);
299
302
rename (expr.type (), ssa.get_identifier (), ns, level);
300
303
ssa.update_type ();
301
304
@@ -551,7 +554,7 @@ void goto_symex_statet::rename_address(
551
554
ssa_exprt &ssa=to_ssa_expr (expr);
552
555
553
556
// only do L1!
554
- set_l1_indices (ssa, ns);
557
+ set_l1_indices (level0, level1, ssa, source. thread_nr , ns);
555
558
556
559
rename (expr.type (), ssa.get_identifier (), ns, level);
557
560
ssa.update_type ();
0 commit comments