diff --git a/src/goto-programs/class_identifier.cpp b/src/goto-programs/class_identifier.cpp index 05fd4c989ce..3ab1e8286a8 100644 --- a/src/goto-programs/class_identifier.cpp +++ b/src/goto-programs/class_identifier.cpp @@ -28,8 +28,8 @@ static exprt build_class_identifier( while(1) { - const typet &type=ns.follow(e.type()); - const struct_typet &struct_type=to_struct_type(type); + const struct_typet &struct_type = + ns.follow_tag(to_struct_tag_type(e.type())); const struct_typet::componentst &components=struct_type.components(); INVARIANT(!components.empty(), "class structs cannot be empty"); @@ -85,7 +85,8 @@ void set_class_identifier( const namespacet &ns, const struct_tag_typet &class_type) { - const struct_typet &struct_type=to_struct_type(ns.follow(expr.type())); + const struct_typet &struct_type = + ns.follow_tag(to_struct_tag_type(expr.type())); const struct_typet::componentst &components=struct_type.components(); if(components.empty()) diff --git a/src/goto-programs/destructor.cpp b/src/goto-programs/destructor.cpp index 29ff573929b..9ad197dc572 100644 --- a/src/goto-programs/destructor.cpp +++ b/src/goto-programs/destructor.cpp @@ -38,9 +38,13 @@ code_function_callt get_destructor( { const typet &arg_type=code_type.parameters().front().type(); + if(arg_type.id() != ID_pointer) + continue; + + const typet &base_type = to_pointer_type(arg_type).base_type(); if( - arg_type.id() == ID_pointer && - ns.follow(to_pointer_type(arg_type).base_type()) == type) + base_type.id() == ID_struct_tag && + ns.follow_tag(to_struct_tag_type(base_type)) == type) { const symbol_exprt symbol_expr(op.get(ID_name), op.type()); return code_function_callt(symbol_expr); diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp index 50aa2e3bcb2..31a6e8c2ac3 100644 --- a/src/goto-programs/graphml_witness.cpp +++ b/src/goto-programs/graphml_witness.cpp @@ -132,10 +132,13 @@ std::string graphml_witnesst::convert_assign_rec( return convert_assign_rec(identifier, tmp); } - const struct_union_typet &type= - to_struct_union_type(ns.follow(assign.lhs().type())); - const struct_union_typet::componentst &components= - type.components(); + const typet &lhs_type = assign.lhs().type(); + const struct_union_typet::componentst &components = + lhs_type.id() == ID_struct_tag + ? ns.follow_tag(to_struct_tag_type(lhs_type)).components() + : lhs_type.id() == ID_union_tag + ? ns.follow_tag(to_union_tag_type(lhs_type)).components() + : to_struct_union_type(lhs_type).components(); exprt::operandst::const_iterator it= assign.rhs().operands().begin(); diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp index 7761d4d091f..29d0f766f56 100644 --- a/src/goto-programs/interpreter.cpp +++ b/src/goto-programs/interpreter.cpp @@ -424,11 +424,11 @@ void interpretert::execute_decl() struct_typet::componentt interpretert::get_component(const typet &object_type, const mp_integer &offset) { - const typet real_type = ns.follow(object_type); - if(real_type.id()!=ID_struct) + if(object_type.id() != ID_struct_tag) throw "request for member of non-struct"; - const struct_typet &struct_type=to_struct_type(real_type); + const struct_typet &struct_type = + ns.follow_tag(to_struct_tag_type(object_type)); const struct_typet::componentst &components=struct_type.components(); mp_integer tmp_offset=offset; @@ -460,11 +460,10 @@ exprt interpretert::get_value( const mp_integer &offset, bool use_non_det) { - const typet real_type=ns.follow(type); - if(real_type.id()==ID_struct) + if(type.id() == ID_struct_tag) { - struct_exprt result({}, real_type); - const struct_typet &struct_type=to_struct_type(real_type); + struct_exprt result({}, type); + const struct_typet &struct_type = ns.follow_tag(to_struct_tag_type(type)); const struct_typet::componentst &components=struct_type.components(); // Retrieve the values for the individual members @@ -482,10 +481,10 @@ exprt interpretert::get_value( return std::move(result); } - else if(real_type.id()==ID_array) + else if(type.id() == ID_array) { // Get size of array - array_exprt result({}, to_array_type(real_type)); + array_exprt result({}, to_array_type(type)); const exprt &size_expr = to_array_type(type).size(); mp_integer subtype_size = get_size(to_array_type(type).element_type()); mp_integer count; @@ -526,13 +525,12 @@ exprt interpretert::get_value( mp_vectort &rhs, const mp_integer &offset) { - const typet real_type=ns.follow(type); PRECONDITION(!rhs.empty()); - if(real_type.id()==ID_struct) + if(type.id() == ID_struct_tag) { - struct_exprt result({}, real_type); - const struct_typet &struct_type=to_struct_type(real_type); + struct_exprt result({}, type); + const struct_typet &struct_type = ns.follow_tag(to_struct_tag_type(type)); const struct_typet::componentst &components=struct_type.components(); // Retrieve the values for the individual members @@ -548,10 +546,10 @@ exprt interpretert::get_value( } return std::move(result); } - else if(real_type.id()==ID_array) + else if(type.id() == ID_array) { - array_exprt result({}, to_array_type(real_type)); - const exprt &size_expr = to_array_type(real_type).size(); + array_exprt result({}, to_array_type(type)); + const exprt &size_expr = to_array_type(type).size(); // Get size of array mp_integer subtype_size = get_size(to_array_type(type).element_type()); @@ -576,34 +574,34 @@ exprt interpretert::get_value( } return std::move(result); } - else if(real_type.id()==ID_floatbv) + else if(type.id() == ID_floatbv) { ieee_floatt f(to_floatbv_type(type)); f.unpack(rhs[numeric_cast_v(offset)]); return f.to_expr(); } - else if(real_type.id()==ID_fixedbv) + else if(type.id() == ID_fixedbv) { fixedbvt f; f.from_integer(rhs[numeric_cast_v(offset)]); return f.to_expr(); } - else if(real_type.id()==ID_bool) + else if(type.id() == ID_bool) { if(rhs[numeric_cast_v(offset)] != 0) return true_exprt(); else false_exprt(); } - else if(real_type.id()==ID_c_bool) + else if(type.id() == ID_c_bool) { return from_integer( rhs[numeric_cast_v(offset)] != 0 ? 1 : 0, type); } - else if(real_type.id() == ID_pointer) + else if(type.id() == ID_pointer) { if(rhs[numeric_cast_v(offset)] == 0) - return null_pointer_exprt(to_pointer_type(real_type)); // NULL pointer + return null_pointer_exprt(to_pointer_type(type)); // NULL pointer if(rhs[numeric_cast_v(offset)] < memory.size()) { @@ -634,7 +632,7 @@ exprt interpretert::get_value( throw "interpreter: reading from invalid pointer"; } - else if(real_type.id()==ID_string) + else if(type.id() == ID_string) { // Strings are currently encoded by their irep_idt ID. return constant_exprt( diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp index 65570975ce9..cdb413e351e 100644 --- a/src/goto-programs/interpreter_evaluate.cpp +++ b/src/goto-programs/interpreter_evaluate.cpp @@ -1042,7 +1042,7 @@ mp_integer interpretert::evaluate_address( else if(expr.id()==ID_member) { const struct_typet &struct_type = - to_struct_type(ns.follow(to_member_expr(expr).compound().type())); + ns.follow_tag(to_struct_tag_type(to_member_expr(expr).compound().type())); const irep_idt &component_name= to_member_expr(expr).get_component_name(); diff --git a/src/goto-programs/json_expr.cpp b/src/goto-programs/json_expr.cpp index 6b49f5114c3..16139131b90 100644 --- a/src/goto-programs/json_expr.cpp +++ b/src/goto-programs/json_expr.cpp @@ -361,24 +361,22 @@ json_objectt json(const exprt &expr, const namespacet &ns, const irep_idt &mode) { result["name"] = json_stringt("struct"); - const typet &type = ns.follow(expr.type()); + const struct_typet &struct_type = + expr.type().id() == ID_struct_tag + ? ns.follow_tag(to_struct_tag_type(expr.type())) + : to_struct_type(expr.type()); + const struct_typet::componentst &components = struct_type.components(); + DATA_INVARIANT( + components.size() == expr.operands().size(), + "number of struct components should match with its type"); - // these are expected to have a struct type - if(type.id() == ID_struct) + json_arrayt &members = result["members"].make_array(); + for(std::size_t m = 0; m < expr.operands().size(); m++) { - const struct_typet &struct_type = to_struct_type(type); - const struct_typet::componentst &components = struct_type.components(); - DATA_INVARIANT( - components.size() == expr.operands().size(), - "number of struct components should match with its type"); - - json_arrayt &members = result["members"].make_array(); - for(std::size_t m = 0; m < expr.operands().size(); m++) - { - json_objectt e{{"value", json(expr.operands()[m], ns, mode)}, - {"name", json_stringt(components[m].get_name())}}; - members.push_back(std::move(e)); - } + json_objectt e{ + {"value", json(expr.operands()[m], ns, mode)}, + {"name", json_stringt(components[m].get_name())}}; + members.push_back(std::move(e)); } } else if(expr.id() == ID_union) diff --git a/src/goto-programs/remove_const_function_pointers.cpp b/src/goto-programs/remove_const_function_pointers.cpp index 0ea7b54f96a..043a3107184 100644 --- a/src/goto-programs/remove_const_function_pointers.cpp +++ b/src/goto-programs/remove_const_function_pointers.cpp @@ -800,7 +800,8 @@ bool remove_const_function_pointerst::is_const_type(const typet &type) const exprt remove_const_function_pointerst::get_component_value( const struct_exprt &struct_expr, const member_exprt &member_expr) { - const struct_typet &struct_type=to_struct_type(ns.follow(struct_expr.type())); + const struct_typet &struct_type = + ns.follow_tag(to_struct_tag_type(struct_expr.type())); size_t component_number= struct_type.component_number(member_expr.get_component_name()); diff --git a/src/goto-programs/rewrite_union.cpp b/src/goto-programs/rewrite_union.cpp index 3fcb4b33e91..71b37ed0c54 100644 --- a/src/goto-programs/rewrite_union.cpp +++ b/src/goto-programs/rewrite_union.cpp @@ -139,7 +139,10 @@ static bool restore_union_rec(exprt &expr, const namespacet &ns) byte_extract_exprt &be = to_byte_extract_expr(expr); if(be.op().type().id() == ID_union || be.op().type().id() == ID_union_tag) { - const union_typet &union_type = to_union_type(ns.follow(be.op().type())); + const union_typet &union_type = + be.op().type().id() == ID_union_tag + ? ns.follow_tag(to_union_tag_type(be.op().type())) + : to_union_type(be.op().type()); for(const auto &comp : union_type.components()) { diff --git a/src/goto-programs/string_abstraction.cpp b/src/goto-programs/string_abstraction.cpp index 5f0178c6a64..82faec7f2b0 100644 --- a/src/goto-programs/string_abstraction.cpp +++ b/src/goto-programs/string_abstraction.cpp @@ -353,14 +353,14 @@ exprt string_abstractiont::make_val_or_dummy_rec(goto_programt &dest, symbol.type.id() == ID_union_tag || (symbol.type.id() == ID_struct_tag && symbol.type != string_struct)) { - const struct_union_typet &su_source = - to_struct_union_type(ns.follow(source_type)); - const struct_union_typet::componentst &s_components= - su_source.components(); - const struct_union_typet &struct_union_type = - to_struct_union_type(ns.follow(symbol.type)); - const struct_union_typet::componentst &components= - struct_union_type.components(); + const struct_union_typet::componentst &s_components = + source_type.id() == ID_struct_tag + ? ns.follow_tag(to_struct_tag_type(source_type)).components() + : ns.follow_tag(to_union_tag_type(source_type)).components(); + const struct_union_typet::componentst &components = + symbol.type.id() == ID_struct_tag + ? ns.follow_tag(to_struct_tag_type(symbol.type)).components() + : ns.follow_tag(to_union_tag_type(symbol.type)).components(); unsigned seen=0; struct_union_typet::componentst::const_iterator it2=components.begin(); @@ -732,7 +732,10 @@ const typet &string_abstractiont::build_abstraction_type_rec(const typet &type, else if(type.id() == ID_struct_tag || type.id() == ID_union_tag) { const struct_union_typet &struct_union_type = - to_struct_union_type(ns.follow(type)); + type.id() == ID_struct_tag ? static_cast( + ns.follow_tag(to_struct_tag_type(type))) + : static_cast( + ns.follow_tag(to_union_tag_type(type))); struct_union_typet::componentst new_comp; for(const auto &comp : struct_union_type.components()) diff --git a/src/goto-programs/xml_expr.cpp b/src/goto-programs/xml_expr.cpp index 801149d62cb..da90516dace 100644 --- a/src/goto-programs/xml_expr.cpp +++ b/src/goto-programs/xml_expr.cpp @@ -253,21 +253,18 @@ xmlt xml(const exprt &expr, const namespacet &ns) { result.name = "struct"; - const typet &type = ns.follow(expr.type()); + const struct_typet &struct_type = + expr.type().id() == ID_struct_tag + ? ns.follow_tag(to_struct_tag_type(expr.type())) + : to_struct_type(expr.type()); + const struct_typet::componentst &components = struct_type.components(); + PRECONDITION(components.size() == expr.operands().size()); - // these are expected to have a struct type - if(type.id() == ID_struct) + for(unsigned m = 0; m < expr.operands().size(); m++) { - const struct_typet &struct_type = to_struct_type(type); - const struct_typet::componentst &components = struct_type.components(); - PRECONDITION(components.size() == expr.operands().size()); - - for(unsigned m = 0; m < expr.operands().size(); m++) - { - xmlt &e = result.new_element("member"); - e.new_element() = xml(expr.operands()[m], ns); - e.set_attribute("name", id2string(components[m].get_name())); - } + xmlt &e = result.new_element("member"); + e.new_element() = xml(expr.operands()[m], ns); + e.set_attribute("name", id2string(components[m].get_name())); } } else if(expr.id() == ID_union)