diff --git a/src/analyses/custom_bitvector_analysis.cpp b/src/analyses/custom_bitvector_analysis.cpp index 4a4f0823391..7687ee51e5c 100644 --- a/src/analyses/custom_bitvector_analysis.cpp +++ b/src/analyses/custom_bitvector_analysis.cpp @@ -233,8 +233,10 @@ void custom_bitvector_domaint::assign_struct_rec( { if(lhs.type().id() == ID_struct || lhs.type().id() == ID_struct_tag) { - const struct_typet &struct_type= - to_struct_type(ns.follow(lhs.type())); + const struct_typet &struct_type = + lhs.type().id() == ID_struct + ? to_struct_type(lhs.type()) + : ns.follow_tag(to_struct_tag_type(lhs.type())); // assign member-by-member for(const auto &c : struct_type.components()) diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp index cbd36d3ccb6..a47497dddc4 100644 --- a/src/analyses/goto_rw.cpp +++ b/src/analyses/goto_rw.cpp @@ -250,7 +250,9 @@ void rw_range_sett::get_objects_member( return; } - const struct_typet &struct_type = to_struct_type(ns.follow(type)); + const struct_typet &struct_type = type.id() == ID_struct + ? to_struct_type(type) + : ns.follow_tag(to_struct_tag_type(type)); auto offset_bits = member_offset_bits(struct_type, expr.get_component_name(), ns); @@ -367,8 +369,10 @@ void rw_range_sett::get_objects_struct( const range_spect &range_start, const range_spect &size) { - const struct_typet &struct_type= - to_struct_type(ns.follow(expr.type())); + const struct_typet &struct_type = + expr.type().id() == ID_struct + ? to_struct_type(expr.type()) + : ns.follow_tag(to_struct_tag_type(expr.type())); auto struct_bits = pointer_offset_bits(struct_type, ns); diff --git a/src/analyses/invariant_propagation.cpp b/src/analyses/invariant_propagation.cpp index a7cc24007b1..a8fb79e2a77 100644 --- a/src/analyses/invariant_propagation.cpp +++ b/src/analyses/invariant_propagation.cpp @@ -131,7 +131,10 @@ void invariant_propagationt::get_objects_rec( t.id() == ID_struct || t.id() == ID_union || t.id() == ID_struct_tag || t.id() == ID_union_tag) { - const struct_union_typet &struct_type = to_struct_union_type(ns.follow(t)); + const struct_union_typet &struct_type = + (t.id() == ID_struct_tag || t.id() == ID_union_tag) + ? ns.follow_tag(to_struct_or_union_tag_type(t)) + : to_struct_union_type(t); for(const auto &component : struct_type.components()) { @@ -223,7 +226,9 @@ bool invariant_propagationt::check_type(const typet &type) const else if( type.id() == ID_struct || type.id() == ID_union || type.id() == ID_struct_tag || type.id() == ID_union_tag) + { return false; + } else if(type.id()==ID_array) return false; else if(type.id()==ID_unsignedbv || diff --git a/src/analyses/invariant_set.cpp b/src/analyses/invariant_set.cpp index 0ff174e3098..49c3c8b2324 100644 --- a/src/analyses/invariant_set.cpp +++ b/src/analyses/invariant_set.cpp @@ -474,7 +474,9 @@ void invariant_sett::strengthen_rec(const exprt &expr) if(op_type.id() == ID_struct || op_type.id() == ID_struct_tag) { - const struct_typet &struct_type = to_struct_type(ns.follow(op_type)); + const struct_typet &struct_type = + op_type.id() == ID_struct ? to_struct_type(op_type) + : ns.follow_tag(to_struct_tag_type(op_type)); for(const auto &comp : struct_type.components()) { diff --git a/src/analyses/variable-sensitivity/abstract_aggregate_object.h b/src/analyses/variable-sensitivity/abstract_aggregate_object.h index 98fbe7c11fb..ca9797cf47e 100644 --- a/src/analyses/variable-sensitivity/abstract_aggregate_object.h +++ b/src/analyses/variable-sensitivity/abstract_aggregate_object.h @@ -33,7 +33,13 @@ class abstract_aggregate_objectt : public abstract_objectt, abstract_aggregate_objectt(const typet &type, bool tp, bool bttm) : abstract_objectt(type, tp, bttm) { - PRECONDITION(type.id() == aggregate_traitst::TYPE_ID()); + PRECONDITION( + type.id() != ID_struct_tag || ID_struct == aggregate_traitst::TYPE_ID()); + PRECONDITION( + type.id() != ID_union_tag || ID_union == aggregate_traitst::TYPE_ID()); + PRECONDITION( + type.id() == ID_struct_tag || type.id() == ID_union_tag || + type.id() == aggregate_traitst::TYPE_ID()); } abstract_aggregate_objectt( @@ -42,7 +48,15 @@ class abstract_aggregate_objectt : public abstract_objectt, const namespacet &ns) : abstract_objectt(expr, environment, ns) { - PRECONDITION(ns.follow(expr.type()).id() == aggregate_traitst::TYPE_ID()); + PRECONDITION( + expr.type().id() != ID_struct_tag || + ID_struct == aggregate_traitst::TYPE_ID()); + PRECONDITION( + expr.type().id() != ID_union_tag || + ID_union == aggregate_traitst::TYPE_ID()); + PRECONDITION( + expr.type().id() == ID_struct_tag || expr.type().id() == ID_union_tag || + expr.type().id() == aggregate_traitst::TYPE_ID()); } abstract_object_pointert expression_transform( diff --git a/src/analyses/variable-sensitivity/abstract_environment.cpp b/src/analyses/variable-sensitivity/abstract_environment.cpp index d1a9cdad5dd..4eedf918105 100644 --- a/src/analyses/variable-sensitivity/abstract_environment.cpp +++ b/src/analyses/variable-sensitivity/abstract_environment.cpp @@ -209,19 +209,16 @@ bool abstract_environmentt::assign( final_value = value; } - const typet &lhs_type = ns.follow(lhs_value->type()); - const typet &rhs_type = ns.follow(final_value->type()); - // Write the value for the root symbol back into the map INVARIANT( - lhs_type == rhs_type, + lhs_value->type() == final_value->type(), "Assignment types must match" "\n" "lhs_type :" + - lhs_type.pretty() + + lhs_value->type().pretty() + "\n" "rhs_type :" + - rhs_type.pretty()); + final_value->type().pretty()); // If LHS was directly the symbol if(s.id() == ID_symbol) diff --git a/src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp b/src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp index b4bf1a6312b..3706931aba1 100644 --- a/src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp @@ -10,7 +10,6 @@ #include #include -#include #include #include @@ -225,8 +224,7 @@ abstract_object_pointert constant_pointer_abstract_objectt::write_dereference( if(stack.empty()) { // We should not be changing the type of an abstract object - PRECONDITION( - new_value->type() == ns.follow(to_pointer_type(type()).base_type())); + PRECONDITION(new_value->type() == to_pointer_type(type()).base_type()); // Get an expression that we can assign to exprt value = to_address_of_expr(value_stack.to_expression()).object(); diff --git a/src/analyses/variable-sensitivity/full_struct_abstract_object.cpp b/src/analyses/variable-sensitivity/full_struct_abstract_object.cpp index a2b2a6f9cbc..ab1ae403d46 100644 --- a/src/analyses/variable-sensitivity/full_struct_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/full_struct_abstract_object.cpp @@ -33,7 +33,7 @@ full_struct_abstract_objectt::full_struct_abstract_objectt( bool bottom) : abstract_aggregate_baset(t, top, bottom) { - PRECONDITION(t.id() == ID_struct); + PRECONDITION(t.id() == ID_struct || t.id() == ID_struct_tag); DATA_INVARIANT(verify(), "Structural invariants maintained"); } @@ -43,9 +43,11 @@ full_struct_abstract_objectt::full_struct_abstract_objectt( const namespacet &ns) : abstract_aggregate_baset(e, environment, ns) { - PRECONDITION(ns.follow(e.type()).id() == ID_struct); + PRECONDITION(e.type().id() == ID_struct || e.type().id() == ID_struct_tag); - const struct_typet struct_type_def = to_struct_type(ns.follow(e.type())); + const struct_typet &struct_type_def = + e.type().id() == ID_struct ? to_struct_type(e.type()) + : ns.follow_tag(to_struct_tag_type(e.type())); bool did_initialize_values = false; auto struct_type_it = struct_type_def.components().begin(); @@ -204,7 +206,10 @@ void full_struct_abstract_objectt::output( // To ensure that a consistent ordering of fields is output, use // the underlying type declaration for this struct to determine // the ordering - struct_union_typet type_decl = to_struct_union_type(ns.follow(type())); + struct_union_typet type_decl = + (type().id() == ID_struct_tag || type().id() == ID_union_tag) + ? ns.follow_tag(to_struct_or_union_tag_type(type())) + : to_struct_union_type(type()); bool first = true; diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp b/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp index 50ee5b624c9..c86ece4c8f4 100644 --- a/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp +++ b/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp @@ -8,8 +8,6 @@ #include "variable_sensitivity_object_factory.h" -#include - #include "constant_abstract_value.h" #include "constant_pointer_abstract_object.h" #include "data_dependency_context.h" @@ -44,7 +42,7 @@ abstract_object_pointert create_abstract_object( if(top || bottom) return std::make_shared(type, top, bottom); - PRECONDITION(type == ns.follow(e.type())); + PRECONDITION(type == e.type()); return std::make_shared(e, environment, ns); } @@ -124,11 +122,11 @@ variable_sensitivity_object_factoryt::get_abstract_object_type( { return configuration.pointer_abstract_type; } - else if(type.id() == ID_struct) + else if(type.id() == ID_struct || type.id() == ID_struct_tag) { return configuration.struct_abstract_type; } - else if(type.id() == ID_union) + else if(type.id() == ID_union || type.id() == ID_union_tag) { return configuration.union_abstract_type; } @@ -149,52 +147,50 @@ variable_sensitivity_object_factoryt::get_abstract_object( const abstract_environmentt &environment, const namespacet &ns) const { - const typet &followed_type = ns.follow(type); - ABSTRACT_OBJECT_TYPET abstract_object_type = - get_abstract_object_type(followed_type); + ABSTRACT_OBJECT_TYPET abstract_object_type = get_abstract_object_type(type); switch(abstract_object_type) { case TWO_VALUE: return initialize_abstract_object( - followed_type, top, bottom, e, environment, ns, configuration); + type, top, bottom, e, environment, ns, configuration); case CONSTANT: return initialize_abstract_object( - followed_type, top, bottom, e, environment, ns, configuration); + type, top, bottom, e, environment, ns, configuration); case INTERVAL: return initialize_abstract_object( - followed_type, top, bottom, e, environment, ns, configuration); + type, top, bottom, e, environment, ns, configuration); case VALUE_SET: return initialize_abstract_object( - followed_type, top, bottom, e, environment, ns, configuration); + type, top, bottom, e, environment, ns, configuration); case ARRAY_INSENSITIVE: return initialize_abstract_object( - followed_type, top, bottom, e, environment, ns, configuration); + type, top, bottom, e, environment, ns, configuration); case ARRAY_SENSITIVE: return initialize_abstract_object( - followed_type, top, bottom, e, environment, ns, configuration); + type, top, bottom, e, environment, ns, configuration); case POINTER_INSENSITIVE: return initialize_abstract_object( - followed_type, top, bottom, e, environment, ns, configuration); + type, top, bottom, e, environment, ns, configuration); case POINTER_SENSITIVE: return initialize_abstract_object( - followed_type, top, bottom, e, environment, ns, configuration); + type, top, bottom, e, environment, ns, configuration); case VALUE_SET_OF_POINTERS: return initialize_abstract_object( - followed_type, top, bottom, e, environment, ns, configuration); + type, top, bottom, e, environment, ns, configuration); case STRUCT_INSENSITIVE: return initialize_abstract_object( - followed_type, top, bottom, e, environment, ns, configuration); + type, top, bottom, e, environment, ns, configuration); case STRUCT_SENSITIVE: return initialize_abstract_object( - followed_type, top, bottom, e, environment, ns, configuration); + type, top, bottom, e, environment, ns, configuration); case UNION_INSENSITIVE: return initialize_abstract_object( - followed_type, top, bottom, e, environment, ns, configuration); + type, top, bottom, e, environment, ns, configuration); case HEAP_ALLOCATION: { @@ -210,7 +206,7 @@ variable_sensitivity_object_factoryt::get_abstract_object( default: UNREACHABLE; return initialize_abstract_object( - followed_type, top, bottom, e, environment, ns, configuration); + type, top, bottom, e, environment, ns, configuration); } }