From 99e33bdcc268e4813ad5eb7850801f34dd5dc494 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 7 Aug 2018 16:17:19 +0100 Subject: [PATCH 1/2] fix typo in comments for struct_tag_typet --- src/util/std_types.h | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/util/std_types.h b/src/util/std_types.h index 792f7e40ab8..00f9566926b 100644 --- a/src/util/std_types.h +++ b/src/util/std_types.h @@ -553,13 +553,13 @@ class struct_tag_typet:public tag_typet } }; -/*! \brief Cast a generic typet to a \ref union_tag_typet +/*! \brief Cast a generic typet to a \ref struct_tag_typet * * This is an unchecked conversion. \a type must be known to be \ref - * union_tag_typet. + * struct_tag_typet. * * \param type Source type - * \return Object of type \ref union_tag_typet + * \return Object of type \ref struct_tag_typet * * \ingroup gr_std_types */ From f94d5e2979535e89afbe77d03039240e0c54bd82 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 7 Aug 2018 19:46:50 +0100 Subject: [PATCH 2/2] follow union, struct and enum tags --- src/ansi-c/c_typecast.cpp | 17 ++++++++++------- src/ansi-c/c_typecheck_expr.cpp | 3 +-- src/ansi-c/padding.cpp | 4 ++++ src/util/namespace.cpp | 6 ++++++ src/util/pointer_offset_size.cpp | 16 ++++++++++++++++ 5 files changed, 37 insertions(+), 9 deletions(-) diff --git a/src/ansi-c/c_typecast.cpp b/src/ansi-c/c_typecast.cpp index df332a9cb1c..b0f3aeda819 100644 --- a/src/ansi-c/c_typecast.cpp +++ b/src/ansi-c/c_typecast.cpp @@ -252,21 +252,24 @@ bool check_c_implicit_typecast( typet c_typecastt::follow_with_qualifiers(const typet &src_type) { - if(src_type.id()!=ID_symbol) + if( + src_type.id() != ID_symbol && src_type.id() != ID_struct_tag && + src_type.id() != ID_union_tag) + { return src_type; + } typet result_type=src_type; // collect qualifiers c_qualifierst qualifiers(src_type); - while(result_type.id()==ID_symbol) + while(result_type.id() == ID_symbol || result_type.id() == ID_struct_tag || + result_type.id() == ID_union_tag) { - const symbolt &followed_type_symbol = - ns.lookup(to_symbol_type(result_type)); - - result_type=followed_type_symbol.type; - qualifiers+=c_qualifierst(followed_type_symbol.type); + const typet &followed_type = ns.follow(result_type); + result_type = followed_type; + qualifiers += c_qualifierst(followed_type); } qualifiers.write(result_type); diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 26091bb88ca..24567080b52 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -524,8 +524,7 @@ void c_typecheck_baset::typecheck_expr_builtin_offsetof(exprt &expr) forall_operands(m_it, member) { - if(type.id()==ID_symbol) - type=follow(type); + type = follow(type); if(m_it->id()==ID_member) { diff --git a/src/ansi-c/padding.cpp b/src/ansi-c/padding.cpp index ed6c21c4b83..78489fde8ab 100644 --- a/src/ansi-c/padding.cpp +++ b/src/ansi-c/padding.cpp @@ -82,6 +82,10 @@ mp_integer alignment(const typet &type, const namespacet &ns) result=alignment(type.subtype(), ns); else if(type.id()==ID_c_enum_tag) result=alignment(ns.follow_tag(to_c_enum_tag_type(type)), ns); + else if(type.id() == ID_struct_tag) + result = alignment(ns.follow_tag(to_struct_tag_type(type)), ns); + else if(type.id() == ID_union_tag) + result = alignment(ns.follow_tag(to_union_tag_type(type)), ns); else if(type.id()==ID_symbol) result=alignment(ns.follow(type), ns); else if(type.id()==ID_c_bit_field) diff --git a/src/util/namespace.cpp b/src/util/namespace.cpp index 255b97c8eb9..04a6f260db8 100644 --- a/src/util/namespace.cpp +++ b/src/util/namespace.cpp @@ -54,6 +54,12 @@ const symbolt &namespace_baset::lookup(const tag_typet &type) const const typet &namespace_baset::follow(const typet &src) const { + if(src.id() == ID_union_tag) + return follow_tag(to_union_tag_type(src)); + + if(src.id() == ID_struct_tag) + return follow_tag(to_struct_tag_type(src)); + if(src.id()!=ID_symbol) return src; diff --git a/src/util/pointer_offset_size.cpp b/src/util/pointer_offset_size.cpp index 2e315ba242f..872e69a65fc 100644 --- a/src/util/pointer_offset_size.cpp +++ b/src/util/pointer_offset_size.cpp @@ -238,6 +238,14 @@ mp_integer pointer_offset_bits( { return pointer_offset_bits(ns.follow(type), ns); } + else if(type.id() == ID_union_tag) + { + return pointer_offset_bits(ns.follow_tag(to_union_tag_type(type)), ns); + } + else if(type.id() == ID_struct_tag) + { + return pointer_offset_bits(ns.follow_tag(to_struct_tag_type(type)), ns); + } else if(type.id()==ID_code) { return 0; @@ -506,6 +514,14 @@ exprt size_of_expr( { return size_of_expr(ns.follow(type), ns); } + else if(type.id() == ID_union_tag) + { + return size_of_expr(ns.follow_tag(to_union_tag_type(type)), ns); + } + else if(type.id() == ID_struct_tag) + { + return size_of_expr(ns.follow_tag(to_struct_tag_type(type)), ns); + } else if(type.id()==ID_code) { return from_integer(0, size_type());