Skip to content

Commit 888bad3

Browse files
Avoid calling rename with level=L0
Instead rename_level0 should be called directly. This will allow us to get rid of the L0 case in rename, and make it return a type which reflects the level of renaming.
1 parent 29fb816 commit 888bad3

File tree

2 files changed

+19
-5
lines changed

2 files changed

+19
-5
lines changed

src/goto-symex/goto_symex_state.cpp

Lines changed: 18 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -597,6 +597,13 @@ void goto_symex_statet::rename_address(
597597
const namespacet &ns,
598598
levelt level)
599599
{
600+
auto rename_expr = [&](exprt &e) {
601+
if(level == L0)
602+
rename_level0(e, ns);
603+
else
604+
rename(e, ns, level);
605+
};
606+
600607
if(expr.id()==ID_symbol &&
601608
expr.get_bool(ID_C_SSA_symbol))
602609
{
@@ -624,13 +631,13 @@ void goto_symex_statet::rename_address(
624631
expr.type() = to_array_type(index_expr.array().type()).subtype();
625632

626633
// the index is not an address
627-
rename(index_expr.index(), ns, level);
634+
rename_expr(index_expr.index());
628635
}
629636
else if(expr.id()==ID_if)
630637
{
631638
// the condition is not an address
632639
if_exprt &if_expr=to_if_expr(expr);
633-
rename(if_expr.cond(), ns, level);
640+
rename_expr(if_expr.cond());
634641
rename_address(if_expr.true_case(), ns, level);
635642
rename_address(if_expr.false_case(), ns, level);
636643

@@ -692,6 +699,13 @@ void goto_symex_statet::rename(
692699
const namespacet &ns,
693700
levelt level)
694701
{
702+
auto rename_expr = [&](exprt &e) {
703+
if(level == L0)
704+
rename_level0(e, ns);
705+
else
706+
rename(e, ns, level);
707+
};
708+
695709
// rename all the symbols with their last known value
696710
// to the given level
697711

@@ -721,7 +735,7 @@ void goto_symex_statet::rename(
721735
if(const auto &array_type = type_try_dynamic_cast<array_typet>(type))
722736
{
723737
rename(array_type->subtype(), irep_idt(), ns, level);
724-
rename(array_type->size(), ns, level);
738+
rename_expr(array_type->size());
725739
}
726740
else if(
727741
const auto &s_u_type = type_try_dynamic_cast<struct_union_typet>(type))
@@ -730,7 +744,7 @@ void goto_symex_statet::rename(
730744
{
731745
// be careful, or it might get cyclic
732746
if(component.type().id() == ID_array)
733-
rename(to_array_type(component.type()).size(), ns, level);
747+
rename_expr(to_array_type(component.type()).size());
734748
else if(component.type().id() != ID_pointer)
735749
rename(component.type(), irep_idt(), ns, level);
736750
}

src/goto-symex/symex_function_call.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -400,7 +400,7 @@ void goto_symext::locality(
400400
{
401401
// get L0 name
402402
ssa_exprt ssa(ns.lookup(*it).symbol_expr());
403-
state.rename(ssa, ns, goto_symex_statet::L0);
403+
state.rename_level0(ssa, ns);
404404
const irep_idt l0_name=ssa.get_identifier();
405405

406406
// save old L1 name for popping the frame

0 commit comments

Comments
 (0)