32 for(std::size_t i=0; i<new_parameters.size(); i++)
34 if(i<old_parameters.size() &&
35 old_parameters[i].has_default_argument() &&
36 !new_parameters[i].has_default_argument())
39 new_parameters[i].default_argument()=old_parameters[i].default_argument();
62 error() <<
"class templates must not be anonymous" <<
eom;
69 error() <<
"simple name expected as class template tag" <<
eom;
80 base_name, template_type, partial_specialization_args);
90 cpp_scopet::TEMPLATE);
94 const symbolt &previous=
lookup((*id_set.begin())->identifier);
95 if(previous.
name!=symbol_name || id_set.
size()>1)
98 str <<
"template declaration of '" << base_name.
c_str()
99 <<
" does not match previous declaration\n";
100 str <<
"location of previous definition: " << previous.
location;
112 symbolt &previous_symbol=*maybe_symbol;
116 bool previous_has_body=
120 if(has_body && previous_has_body)
123 error() <<
"template struct '" << base_name <<
"' defined previously\n"
124 <<
"location of previous definition: " << previous_symbol.
location
137 previous_symbol.
type.
swap(declaration);
140 std::cout <<
"*****\n";
142 std::cout <<
"*****\n";
143 std::cout <<
"II: " << symbol_name <<
'\n';
162 "symbol should be in template scope");
170 symbol.base_name=base_name;
173 symbol.type.
swap(declaration);
174 symbol.value =
exprt(ID_template_decls);
183 error() <<
"cpp_typecheckt::typecheck_compound_type: "
184 <<
"symbol_table.move() failed"
200 "symbol should be in template scope");
220 error() <<
"function template must have simple name" <<
eom;
252 if(has_value && previous_has_value)
255 error() <<
"function template symbol '" << base_name
256 <<
"' declared previously\n"
257 <<
"location of previous definition: "
264 previous_symbol->
type.
swap(declaration);
274 symbol.base_name=base_name;
277 symbol.type.
swap(declaration);
285 error() <<
"cpp_typecheckt::typecheck_compound_type: "
286 <<
"symbol_table.move() failed"
316 if(cpp_name.
get_sub().size()==4 &&
317 cpp_name.
get_sub()[0].id()==ID_name &&
318 cpp_name.
get_sub()[1].id()==ID_template_args &&
319 cpp_name.
get_sub()[2].id()==
"::" &&
320 cpp_name.
get_sub()[3].id()==ID_name)
323 else if(cpp_name.
get_sub().size()==5 &&
324 cpp_name.
get_sub()[0].id()==ID_name &&
325 cpp_name.
get_sub()[1].id()==ID_template_args &&
326 cpp_name.
get_sub()[2].id()==
"::" &&
327 cpp_name.
get_sub()[3].id()==ID_operator)
336 error() <<
"bad template name" <<
eom;
343 cpp_name.
get_sub().front().get(ID_identifier),
351 error() <<
"class template '"
352 << cpp_name.
get_sub().front().get(ID_identifier) <<
"' not found"
356 else if(id_set.size()>1)
359 error() <<
"class template '"
360 << cpp_name.
get_sub().front().get(ID_identifier) <<
"' is ambiguous"
368 error() <<
"class template '"
369 << cpp_name.
get_sub().front().get(ID_identifier)
370 <<
"' is not a template" <<
eom;
374 const cpp_idt &cpp_id=**(id_set.begin());
377 exprt &template_methods =
378 static_cast<exprt &
>(template_symbol.
value.
add(ID_template_methods));
385 const irept &instantiated_with =
386 template_symbol.
value.
add(ID_instantiated_with);
388 for(std::size_t i=0; i<instantiated_with.
get_sub().size(); i++)
392 instantiated_with.
get_sub()[i]);
406 decl_tmp.
remove(ID_template_type);
407 decl_tmp.
remove(ID_is_template);
419 std::string identifier=
427 for(template_typet::template_parameterst::const_iterator
435 if(it->id()==ID_type)
445 if(!partial_specialization_args.
arguments().empty())
447 identifier+=
"_specialized_to_<";
450 for(cpp_template_args_non_tct::argumentst::const_iterator
451 it=partial_specialization_args.
arguments().begin();
452 it!=partial_specialization_args.
arguments().end();
461 if(it->id() == ID_type || it->id() == ID_ambiguous)
476 const typet &function_type)
480 std::string identifier=
482 partial_specialization_args);
505 error() <<
"qualifiers not expected here" <<
eom;
509 if(cpp_name.
get_sub().size()!=2 ||
510 cpp_name.
get_sub()[0].id()!=ID_name ||
511 cpp_name.
get_sub()[1].id()!=ID_template_args)
516 error() <<
"bad template-class-specialization name" <<
eom;
521 cpp_name.
get_sub()[0].get(ID_identifier);
536 for(cpp_scopest::id_sett::iterator
541 cpp_scopest::id_sett::iterator next=it;
554 error() <<
"class template '" << base_name <<
"' not found" <<
eom;
557 else if(id_set.size()>1)
560 error() <<
"class template '" << base_name <<
"' is ambiguous" <<
eom;
564 symbol_table_baset::symbolst::const_iterator s_it =
569 const symbolt &template_symbol=s_it->second;
574 error() <<
"expected a template" <<
eom;
586 template_args_non_tc);
614 declaration.
declarators().front().type().id()!=ID_function_type)
617 error() <<
"expected function template specialization" <<
eom;
630 if(cpp_name.
get_sub().back().id()==ID_template_args)
633 if(cpp_name.
get_sub().size()!=2 ||
634 cpp_name.
get_sub()[0].id()!=ID_name ||
635 cpp_name.
get_sub()[1].id()!=ID_template_args)
640 error() <<
"bad template-function-specialization name" <<
eom;
644 std::string base_name=
645 cpp_name.
get_sub()[0].get(ID_identifier).c_str();
653 error() <<
"template function '" << base_name <<
"' not found" <<
eom;
656 else if(id_set.size()>1)
659 error() <<
"template function '" << base_name <<
"' is ambiguous" <<
eom;
663 const symbolt &template_symbol=
664 lookup((*id_set.begin())->identifier);
674 typet specialization;
675 specialization.
swap(declarator);
691 new_declaration.
remove(ID_template_type);
692 new_declaration.
remove(ID_is_template);
693 new_declaration.
set(ID_C_template,
"");
718 unsigned anon_count=0;
720 for(template_typet::template_parameterst::iterator
721 it=parameters.begin();
722 it!=parameters.end();
725 exprt ¶meter=*it;
747 error() <<
"template parameter must be simple name" <<
eom;
762 if(declaration.
get_bool(ID_is_type))
778 parameter.
add(ID_C_default_value)=declarator.
value();
794 cpp_declarator_converter.
convert(declaration, declarator);
806 parameter.
add(ID_C_default_value)=default_value;
812 return template_scope;
819 const symbolt &template_symbol,
840 if(parameters.size()<args.size())
843 error() <<
"too many template arguments (expected "
844 << parameters.size() <<
", but got "
845 << args.size() <<
")" <<
eom;
854 for(std::size_t i=0; i<parameters.size(); i++)
866 error() <<
"not enough template arguments (expected "
867 << parameters.size() <<
", but got " << args.size()
886 if(parameter.
id()==ID_type)
888 if(arg.
id()==ID_type)
892 else if(arg.
id() == ID_ambiguous)
896 arg=
exprt(ID_type, t);
901 error() <<
"expected type, but got expression" <<
eom;
907 if(arg.
id()==ID_type)
910 error() <<
"expected expression, but got type" <<
eom;
913 else if(arg.
id() == ID_ambiguous)
929 template_scope!=
nullptr,
931 "template_scope is null");
954 args.size() == parameters.size(),
955 "argument and parameter numbers must match");
968 error() <<
"invalid use of 'virtual' in template declaration"
976 error() <<
"template declaration for typedef" <<
eom;
994 error() <<
"class template not expected to have declarators"
1000 if(type.
id()!=ID_struct)
1003 error() <<
"expected class template" <<
eom;
1011 type.
find(ID_tag))).has_template_args())
1028 error() <<
"non-class template is expected to have a declarator"
1045 declaration.
declarators().size() >= 1,
"declarator required");
Generic exception types primarily designed for use with invariants.
symbol_table_baset & symbol_table
const declaratorst & declarators() const
void set_specialization_of(const irep_idt &id)
const cpp_member_spect & member_spec() const
bool is_class_template() const
template_typet & template_type()
cpp_template_args_non_tct & partial_specialization_args()
symbolt & convert(const typet &type, const cpp_storage_spect &storage_spec, const cpp_member_spect &member_spec, cpp_declaratort &declarator)
bool is_template_parameter
typet merge_type(const typet &declaration_type) const
bool is_template_scope() const
bool is_qualified() const
irep_idt get_base_name() const
const source_locationt & source_location() const
bool has_template_args() const
bool is_simple_name() const
cpp_scopet & current_scope()
cpp_idt & put_into_scope(const symbolt &symbol, cpp_scopet &scope, bool is_friend=false)
class cpp_scopet & new_scope(const irep_idt &new_scope_name)
id_sett lookup(const irep_idt &base_name_to_lookup, lookup_kindt kind)
cpp_idt & insert(const irep_idt &_base_name)
exprt::operandst argumentst
std::string class_template_identifier(const irep_idt &base_name, const template_typet &template_type, const cpp_template_args_non_tct &partial_specialization_args)
void typecheck_type(typet &) override
template_mapt template_map
std::string function_template_identifier(const irep_idt &base_name, const template_typet &template_type, const typet &function_type)
void convert_template_declaration(cpp_declarationt &declaration)
void implicit_typecast(exprt &expr, const typet &type) override
void salvage_default_arguments(const template_typet &old_type, template_typet &new_type)
void convert_non_template_declaration(cpp_declarationt &declaration)
void typecheck_function_template(cpp_declarationt &declaration)
typecheck function templates
unsigned template_counter
void typecheck_class_template_member(cpp_declarationt &declaration)
typecheck class template members; these can be methods or static members
cpp_template_args_tct typecheck_template_args(const source_locationt &source_location, const symbolt &template_symbol, const cpp_template_args_non_tct &template_args)
void convert(cpp_linkage_spect &)
void typecheck_expr(exprt &) override
cpp_scopet & typecheck_template_parameters(template_typet &type)
void typecheck_class_template(cpp_declarationt &declaration)
const symbolt & instantiate_template(const source_locationt &source_location, const symbolt &symbol, const cpp_template_args_tct &specialization_template_args, const cpp_template_args_tct &full_template_args, const typet &specialization=uninitialized_typet{})
void convert_template_function_or_member_specialization(cpp_declarationt &declaration)
void convert_class_template_specialization(cpp_declarationt &declaration)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const char * c_str() const
Base class for all expressions.
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
source_locationt & add_source_location()
const source_locationt & source_location() const
typet & type()
Return the type of the expression.
There are a large number of kinds of tree structured or tree-like data in CPROVER.
bool get_bool(const irep_idt &name) const
const irept & find(const irep_idt &name) const
void remove(const irep_idt &name)
void set(const irep_idt &name, const irep_idt &value)
const irep_idt & id() const
irept & add(const irep_idt &name)
source_locationt source_location
mstreamt & result() const
message_handlert & get_message_handler()
const symbolt & lookup(const irep_idt &name) const
Lookup a symbol in the namespace.
A struct tag type, i.e., struct_typet with an identifier.
Expression to hold a symbol (variable)
virtual bool move(symbolt &symbol, symbolt *&new_symbol)=0
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
virtual symbolt * get_writeable(const irep_idt &name)=0
Find a symbol in the symbol table for read-write access.
irep_idt base_name
Base (non-scoped) name.
source_locationt location
Source code location of definition of symbol.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
typet type
Type of symbol.
irep_idt name
The unique identifier.
exprt value
Initial value of symbol.
void build(const template_typet &template_type, const cpp_template_args_tct &template_args)
void set(const template_parametert ¶meter, const exprt &value)
void swap(template_mapt &template_map)
template_parameterst & template_parameters()
std::vector< template_parametert > template_parameterst
An expression denoting a type.
The type of an expression, extends irept.
const source_locationt & source_location() const
source_locationt & add_source_location()
void cpp_convert_plain_type(typet &type, message_handlert &message_handler)
cpp_declarationt & to_cpp_declaration(irept &irep)
C++ Language Type Checking.
C++ Language Type Checking.
cpp_template_args_non_tct & to_cpp_template_args_non_tc(irept &irep)
std::string cpp_type2name(const typet &type)
std::string cpp_expr2name(const exprt &expr)
C++ Language Type Checking.
const std::string & id2string(const irep_idt &d)
bool simplify(exprt &expr, const namespacet &ns)
#define INVARIANT_STRUCTURED(CONDITION, TYPENAME,...)
#define CHECK_RETURN(CONDITION)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
a template parameter symbol that is a type
exprt & default_argument()
bool has_default_argument() const