@@ -644,6 +644,20 @@ void goto_symex_statet::rename_address(
644
644
}
645
645
}
646
646
647
+ // / Return the type corresponding to a symbol or tag. Empty optional if \p type
648
+ // / is neither a symbol or a tag.
649
+ static optionalt<typet>
650
+ type_of_symbol_or_tag (const typet &type, const namespacet &ns)
651
+ {
652
+ if (type.id () == ID_symbol_type)
653
+ return ns.lookup (to_symbol_type (type)).type ;
654
+ if (type.id () == ID_union_tag)
655
+ return ns.lookup (to_union_tag_type (type)).type ;
656
+ if (type.id () == ID_struct_tag)
657
+ return ns.lookup (to_struct_tag_type (type)).type ;
658
+ return {};
659
+ }
660
+
647
661
void goto_symex_statet::rename (
648
662
typet &type,
649
663
const irep_idt &l1_identifier,
@@ -700,22 +714,9 @@ void goto_symex_statet::rename(
700
714
{
701
715
rename (to_pointer_type (type).subtype (), irep_idt (), ns, level);
702
716
}
703
- else if (type.id () == ID_symbol_type)
704
- {
705
- const symbolt &symbol = ns.lookup (to_symbol_type (type));
706
- type = symbol.type ;
707
- rename (type, l1_identifier, ns, level);
708
- }
709
- else if (type.id () == ID_union_tag)
710
- {
711
- const symbolt &symbol = ns.lookup (to_union_tag_type (type));
712
- type = symbol.type ;
713
- rename (type, l1_identifier, ns, level);
714
- }
715
- else if (type.id () == ID_struct_tag)
717
+ else if (const auto &followed_type = type_of_symbol_or_tag (type, ns))
716
718
{
717
- const symbolt &symbol = ns.lookup (to_struct_tag_type (type));
718
- type=symbol.type ;
719
+ type = *followed_type;
719
720
rename (type, l1_identifier, ns, level);
720
721
}
721
722
0 commit comments