@@ -622,6 +622,20 @@ void goto_symex_statet::rename_address(
622
622
}
623
623
}
624
624
625
+ // / Return the type corresponding to a symbol or tag. Empty optional if \p type
626
+ // / is neither a symbol or a tag.
627
+ static optionalt<typet>
628
+ type_of_symbol_or_tag (const typet &type, const namespacet &ns)
629
+ {
630
+ if (type.id () == ID_symbol_type)
631
+ return ns.lookup (to_symbol_type (type)).type ;
632
+ if (type.id () == ID_union_tag)
633
+ return ns.lookup (to_union_tag_type (type)).type ;
634
+ if (type.id () == ID_struct_tag)
635
+ return ns.lookup (to_struct_tag_type (type)).type ;
636
+ return {};
637
+ }
638
+
625
639
void goto_symex_statet::rename (
626
640
typet &type,
627
641
const irep_idt &l1_identifier,
@@ -678,22 +692,9 @@ void goto_symex_statet::rename(
678
692
{
679
693
rename (to_pointer_type (type).subtype (), irep_idt (), ns, level);
680
694
}
681
- else if (type.id () == ID_symbol_type)
682
- {
683
- const symbolt &symbol = ns.lookup (to_symbol_type (type));
684
- type = symbol.type ;
685
- rename (type, l1_identifier, ns, level);
686
- }
687
- else if (type.id () == ID_union_tag)
688
- {
689
- const symbolt &symbol = ns.lookup (to_union_tag_type (type));
690
- type = symbol.type ;
691
- rename (type, l1_identifier, ns, level);
692
- }
693
- else if (type.id () == ID_struct_tag)
695
+ else if (const auto &followed_type = type_of_symbol_or_tag (type, ns))
694
696
{
695
- const symbolt &symbol = ns.lookup (to_struct_tag_type (type));
696
- type=symbol.type ;
697
+ type = *followed_type;
697
698
rename (type, l1_identifier, ns, level);
698
699
}
699
700
0 commit comments