@@ -629,6 +629,20 @@ void goto_symex_statet::rename_address(
629
629
}
630
630
}
631
631
632
+ // / Return the type corresponding to a symbol or tag. Empty optional if \p type
633
+ // / is neither a symbol or a tag.
634
+ static optionalt<typet>
635
+ type_of_symbol_or_tag (const typet &type, const namespacet &ns)
636
+ {
637
+ if (type.id () == ID_symbol_type)
638
+ return ns.lookup (to_symbol_type (type)).type ;
639
+ if (type.id () == ID_union_tag)
640
+ return ns.lookup (to_union_tag_type (type)).type ;
641
+ if (type.id () == ID_struct_tag)
642
+ return ns.lookup (to_struct_tag_type (type)).type ;
643
+ return {};
644
+ }
645
+
632
646
void goto_symex_statet::rename (
633
647
typet &type,
634
648
const irep_idt &l1_identifier,
@@ -685,22 +699,9 @@ void goto_symex_statet::rename(
685
699
{
686
700
rename (to_pointer_type (type).subtype (), irep_idt (), ns, level);
687
701
}
688
- else if (type.id () == ID_symbol_type)
689
- {
690
- const symbolt &symbol = ns.lookup (to_symbol_type (type));
691
- type = symbol.type ;
692
- rename (type, l1_identifier, ns, level);
693
- }
694
- else if (type.id () == ID_union_tag)
695
- {
696
- const symbolt &symbol = ns.lookup (to_union_tag_type (type));
697
- type = symbol.type ;
698
- rename (type, l1_identifier, ns, level);
699
- }
700
- else if (type.id () == ID_struct_tag)
702
+ else if (const auto &followed_type = type_of_symbol_or_tag (type, ns))
701
703
{
702
- const symbolt &symbol = ns.lookup (to_struct_tag_type (type));
703
- type=symbol.type ;
704
+ type = *followed_type;
704
705
rename (type, l1_identifier, ns, level);
705
706
}
706
707
0 commit comments