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);
98 str <<
"template declaration of '" << base_name.
c_str()
99 <<
" does not match previous declaration\n";
100 str <<
"location of previous definition: " << previous.
location;
123 error() <<
"template struct '" << base_name <<
"' defined previously\n"
140 std::cout <<
"*****\n";
142 std::cout <<
"*****\n";
162 "symbol should be in template scope");
175 symbol.module=
module;
187 error() <<
"cpp_typecheckt::typecheck_compound_type: "
188 <<
"symbol_table.move() failed"
204 "symbol should be in template scope");
224 error() <<
"function template must have simple name" <<
eom;
259 error() <<
"function template symbol '" << base_name
260 <<
"' declared previously\n"
261 <<
"location of previous definition: "
282 symbol.module=
module;
293 error() <<
"cpp_typecheckt::typecheck_compound_type: "
294 <<
"symbol_table.move() failed"
308 template_scope.is_template_scope(),
"symbol should be in template scope");
332 else if(
cpp_name.get_sub().size()==5 &&
345 error() <<
"bad template name" <<
eom;
360 error() <<
"class template '"
368 error() <<
"class template '"
377 error() <<
"class template '"
379 <<
"' is not a template" <<
eom;
428 std::string identifier=
436 for(template_typet::template_parameterst::const_iterator
445 identifier+=
"Type"+std::to_string(
counter);
447 identifier+=
"Non_Type"+std::to_string(
counter);
454 if(!partial_specialization_args.
arguments().empty())
456 identifier+=
"_specialized_to_<";
459 for(cpp_template_args_non_tct::argumentst::const_iterator
460 it=partial_specialization_args.
arguments().begin();
461 it!=partial_specialization_args.
arguments().end();
485 const typet &function_type)
489 std::string identifier=
491 partial_specialization_args);
514 error() <<
"qualifiers not expected here" <<
eom;
525 error() <<
"bad template-class-specialization name" <<
eom;
545 for(cpp_scopest::id_sett::iterator
550 cpp_scopest::id_sett::iterator next=it;
563 error() <<
"class template '" << base_name <<
"' not found" <<
eom;
569 error() <<
"class template '" << base_name <<
"' is ambiguous" <<
eom;
573 symbol_tablet::symbolst::const_iterator
s_it=
583 error() <<
"expected a template" <<
eom;
588 if(
declaration.template_type().parameters().empty())
626 error() <<
"expected function template specialization" <<
eom;
649 error() <<
"bad template-function-specialization name" <<
eom;
653 std::string base_name=
662 error() <<
"template function '" << base_name <<
"' not found" <<
eom;
668 error() <<
"template function '" << base_name <<
"' is ambiguous" <<
eom;
727 unsigned anon_count=0;
729 for(template_typet::template_parameterst::iterator
730 it=parameters.begin();
731 it!=parameters.end();
748 declarator.
name() =
cpp_namet(
"anon#" + std::to_string(++anon_count));
756 error() <<
"template parameter must be simple name" <<
eom;
849 if(parameters.size()<args.size())
852 error() <<
"too many template arguments (expected "
853 << parameters.size() <<
", but got "
854 << args.size() <<
")" <<
eom;
863 for(std::size_t
i=0;
i<parameters.size();
i++)
875 error() <<
"not enough template arguments (expected "
876 << parameters.size() <<
", but got " << args.size()
881 args.push_back(
parameter.default_argument());
910 error() <<
"expected type, but got expression" <<
eom;
919 error() <<
"expected expression, but got type" <<
eom;
940 "template_scope is null");
962 assert(args.size()==parameters.size());
975 error() <<
"invalid use of 'virtual' in template declaration"
983 error() <<
"template declaration for typedef" <<
eom;
1001 error() <<
"class template not expected to have declarators"
1010 error() <<
"expected class template" <<
eom;
1035 error() <<
"non-class template is expected to have a declarator"
1042 if(
declaration.template_type().template_parameters().empty())
Generic exception types primarily designed for use with invariants.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
symbol_tablet & symbol_table
template_typet & template_type()
typet merge_type(const typet &declaration_type) const
cpp_idt & put_into_scope(const symbolt &symbol, cpp_scopet &scope, bool is_friend=false)
cpp_scopet & current_scope()
class cpp_scopet & new_scope(const irep_idt &new_scope_name)
cpp_idt & insert(const irep_idt &_base_name)
id_sett lookup(const irep_idt &base_name_to_lookup, lookup_kindt kind)
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.
typet & type()
Return the type of the expression.
const source_locationt & source_location() const
There are a large number of kinds of tree structured or tree-like data in CPROVER.
const irept & find(const irep_idt &name) const
const irep_idt & id() const
irept & add(const irep_idt &name)
source_locationt source_location
message_handlert & get_message_handler()
mstreamt & result() const
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
A struct tag type, i.e., struct_typet with an identifier.
Expression to hold a symbol (variable)
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) override
Find a symbol in the symbol table for read-write access.
virtual bool move(symbolt &symbol, symbolt *&new_symbol) override
Move a symbol into the symbol table.
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.
irep_idt pretty_name
Language-specific display name.
irep_idt irep_idt base_name
Name of module the symbol belongs to.
exprt value
Initial value of symbol.
irep_idt mode
Language mode.
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
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 PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
a template parameter symbol that is a type