diff --git a/src/cpp/cpp_template_parameter.h b/src/cpp/cpp_template_parameter.h index 696d278d430..c55b6c30a19 100644 --- a/src/cpp/cpp_template_parameter.h +++ b/src/cpp/cpp_template_parameter.h @@ -61,4 +61,48 @@ struct template_parametert:public exprt } }; +/// a template parameter symbol that is a type +struct template_parameter_symbol_typet : public typet +{ +public: + explicit template_parameter_symbol_typet(const irep_idt &identifier) + : typet(ID_template_parameter_symbol_type) + { + set_identifier(identifier); + } + + void set_identifier(const irep_idt &identifier) + { + set(ID_identifier, identifier); + } + + const irep_idt &get_identifier() const + { + return get(ID_identifier); + } +}; + +/// \brief Cast a typet to a \ref template_parameter_symbol_typet. +/// +/// This is an unchecked conversion. \a type must be known to be +/// \ref template_parameter_symbol_typet. Will fail with a +/// precondition violation if type doesn't match. +/// +/// \param type: Source type. +/// \return Object of type \ref template_parameter_symbol_typet. +inline const template_parameter_symbol_typet & +to_template_parameter_symbol_type(const typet &type) +{ + PRECONDITION(type.id() == ID_template_parameter_symbol_type); + return static_cast(type); +} + +/// \copydoc to_template_parameter_symbol_type(const typet &) +inline template_parameter_symbol_typet & +to_template_parameter_symbol_type(typet &type) +{ + PRECONDITION(type.id() == ID_template_parameter_symbol_type); + return static_cast(type); +} + #endif // CPROVER_CPP_CPP_TEMPLATE_PARAMETER_H diff --git a/src/cpp/cpp_typecheck_resolve.cpp b/src/cpp/cpp_typecheck_resolve.cpp index 405d4c3cf38..ef806a2fd44 100644 --- a/src/cpp/cpp_typecheck_resolve.cpp +++ b/src/cpp/cpp_typecheck_resolve.cpp @@ -2283,9 +2283,9 @@ void cpp_typecheck_resolvet::filter_for_named_scopes( if(e.id()!=ID_type) continue; // expressions are definitively not a scope - if(e.type().id() == ID_symbol_type) + if(e.type().id() == ID_template_parameter_symbol_type) { - symbol_typet type=to_symbol_type(e.type()); + auto type = to_template_parameter_symbol_type(e.type()); while(true) { @@ -2294,8 +2294,8 @@ void cpp_typecheck_resolvet::filter_for_named_scopes( const symbolt &symbol=cpp_typecheck.lookup(identifier); assert(symbol.is_type); - if(symbol.type.id() == ID_symbol_type) - type=to_symbol_type(symbol.type); + if(symbol.type.id() == ID_template_parameter_symbol_type) + type = to_template_parameter_symbol_type(symbol.type); else if(symbol.type.id()==ID_struct || symbol.type.id()==ID_union || symbol.type.id()==ID_c_enum) diff --git a/src/cpp/cpp_typecheck_template.cpp b/src/cpp/cpp_typecheck_template.cpp index 85d954bea12..b4dadc6422d 100644 --- a/src/cpp/cpp_typecheck_template.cpp +++ b/src/cpp/cpp_typecheck_template.cpp @@ -774,7 +774,7 @@ cpp_scopet &cpp_typecheckt::typecheck_template_parameters( // is it a type or not? if(declaration.get_bool(ID_is_type)) { - parameter = exprt(ID_type, symbol_typet(identifier)); + parameter = type_exprt(template_parameter_symbol_typet(identifier)); parameter.type().add_source_location()=declaration.find_source_location(); } else diff --git a/src/cpp/template_map.cpp b/src/cpp/template_map.cpp index 76f5174d068..625b11ec757 100644 --- a/src/cpp/template_map.cpp +++ b/src/cpp/template_map.cpp @@ -37,10 +37,10 @@ void template_mapt::apply(typet &type) const apply(subtype); } } - else if(type.id() == ID_symbol_type) + else if(type.id() == ID_template_parameter_symbol_type) { type_mapt::const_iterator m_it = - type_map.find(to_symbol_type(type).get_identifier()); + type_map.find(to_template_parameter_symbol_type(type).get_identifier()); if(m_it!=type_map.end()) { diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index 90c90f9e47b..b6fd76a8855 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -414,6 +414,7 @@ IREP_ID_ONE(template_function_instance) IREP_ID_ONE(template_type) IREP_ID_ONE(template_args) IREP_ID_ONE(template_parameter) +IREP_ID_ONE(template_parameter_symbol_type) IREP_ID_ONE(template_parameters) IREP_ID_TWO(C_template, #template) IREP_ID_TWO(C_template_arguments, #template_arguments)