56 identifiers.push_back(e);
78 identifiers.push_back(e);
98 identifiers.push_back(e);
105 if(identifiers.size()==1)
108 exprt e=*identifiers.begin();
127 identifiers.push_back(
142 ?
static_cast<const typet &
>(
145 ?
static_cast<const typet &
>(
148 ?
static_cast<const typet &
>(
152 identifiers.push_back(
old_id);
162 std::set<irep_idt>
ids;
163 std::set<exprt> other;
178 if(other.insert(
old_id).second)
179 identifiers.push_back(
old_id);
183 if(
ids.insert(
id).second)
184 identifiers.push_back(
old_id);
193 std::cout <<
"RESOLVE MAP:\n";
205 <<
"without instance:\n"
268 const exprt &this_expr=
275 object=
fargs.operands.front();
282 "this argument should be pointer");
285 object.copy_to_operands(this_expr);
305 if(
object.is_not_nil())
417 identifiers.push_back(
old_id);
439 identifiers.push_back(
old_id);
484 for(
auto it = range.first; it != range.second; ++it)
502 identifiers.push_back(*
old_it);
520 "parameter numbers should match");
587 for(
const auto &identifier : identifiers)
683 if(arguments.size()!=1)
687 << base_name <<
" expects one template argument, but got "
698 << base_name <<
" expects one integer template argument, "
718 <<
"template argument must be greater than zero"
728 if(arguments.size()!=2)
732 << base_name <<
" expects two template arguments, but got "
746 << base_name <<
" expects two integer template arguments, "
755 << base_name <<
" expects two integer template arguments, "
762 if(!width.has_value())
772 if(!integer_bits.has_value())
784 <<
"template argument must be greater than zero"
789 if(*integer_bits < 0)
793 <<
"template argument must be greater or equal zero"
798 if(*integer_bits > *width)
802 <<
"template argument must be smaller or equal width"
813 if(!arguments.empty())
817 << base_name <<
" expects no template arguments"
824 else if(base_name.
starts_with(
"constant_infinity"))
829 else if(base_name==
"dump_scopes")
837 else if(base_name==
"current_scope")
876 irept::subt::const_iterator
pos=
cpp_name.get_sub().begin();
897 else if(
pos->id()==
"::")
911 std::cout <<
"X: " <<
id_set.size() <<
'\n';
971 irept::subt::const_iterator next=
pos+1;
1060 full_template_args);
1086 std::vector<matcht> matches;
1118 partial_specialization_args.
arguments().size(),
1119 "number of arguments should match");
1131 <<
"class template instantiation error"
1163 partial_specialization_args);
1170 "argument numbers must match");
1175 matches.push_back(
matcht(
1183 std::sort(matches.begin(), matches.end());
1186 for(std::vector<matcht>::const_iterator
1187 m_it=matches.begin();
1188 m_it!=matches.end();
1191 std::cout <<
"M: " <<
m_it->cost
1192 <<
" " <<
m_it->id <<
'\n';
1198 const matcht &match=*matches.begin();
1265 else if(
id_set.size()==1)
1284 for(
const auto &
id_expr : identifiers)
1306 out <<
"constructor ";
1328 out <<
" " <<
id <<
"(";
1346 if(!parameters.empty())
1359 out <<
" (" << symbol.
location <<
")";
1365 out <<
" (" << symbol.
location <<
")";
1390 std::cout <<
"base name: " << base_name <<
'\n';
1391 std::cout <<
"template args: " <<
template_args.pretty() <<
'\n';
1407 if(base_name==
"__func__" ||
1408 base_name==
"__FUNCTION__" ||
1409 base_name==
"__PRETTY_FUNCTION__")
1415 return std::move(s);
1543 std::cout <<
"P0 " << base_name <<
" " << identifiers.
size() <<
'\n';
1556 std::cout <<
"P1 " << base_name <<
" " <<
new_identifiers.size() <<
'\n';
1565 std::cout <<
"P2 " << base_name <<
" " <<
new_identifiers.size() <<
'\n';
1586 std::cout <<
"P3 " << base_name <<
" " <<
new_identifiers.size() <<
'\n';
1595 std::cout <<
"P4 " << base_name <<
" " <<
new_identifiers.size() <<
'\n';
1614 <<
"found no match for symbol '" << base_name <<
"', candidates are:\n";
1621 <<
"symbol '" << base_name <<
"' does not uniquely resolve:\n";
1629 <<
"e1.type==e2.type: " << (
e1.type() ==
e2.type()) <<
'\n';
1631 <<
"e1.id()==e2.id(): " << (
e1.id() ==
e2.id()) <<
'\n';
1633 <<
"e1.iden==e2.iden: "
1644 for(
const auto &op :
fargs.operands)
1685 <<
"expected expression, but got type '"
1701 <<
"expected type, but got expression '"
1756 const typet &template_type,
1790 std::cout <<
"TT: " << template_type.
pretty() <<
'\n';
1838 std::cout <<
"ASSIGN " <<
id.identifier <<
" := "
1892 ?
static_cast<const typet &
>(
1895 ?
static_cast<const typet &
>(
1898 ?
static_cast<const typet &
>(
1917 if(
fargs.operands.empty())
1946 <<
"expected function type for function template"
1963 <<
"function template instantiation error"
1975 exprt::operandst::const_iterator it=
fargs.operands.begin();
1978 if(it==
fargs.operands.end())
2017 typet function_type=
2111 code_type.parameters().front().get_this())
2114 if(
fargs.has_object)
2126 "method should exist in struct");
2129 *
fargs.operands.begin(),
2160 if(!
fargs.has_object)
2170 const typet &object_type =
2183 fargs.operands.size() == parameters.size())
2195 else if(
fargs.has_object)
2219 if(
id.is_class() ||
id.is_enum() ||
id.is_namespace())
2225 else if(
id.is_typedef())
2263 id.print(std::cout);
2284 std::cout <<
"E: " << e.
pretty() <<
'\n';
2296 irep_idt identifier=type.get_identifier();
2329 for(cpp_scopest::id_sett::iterator
2334 if((*it)->is_namespace())
2338 cpp_scopest::id_sett::iterator old(it);
2351 for(
const auto &arg :
fargs.operands)
bool has_component_rec(const typet &type, const irep_idt &component_name, const namespacet &ns)
C Language Type Checking.
signedbv_typet signed_int_type()
pointer_typet pointer_type(const typet &subtype)
signedbv_typet signed_size_type()
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
virtual void clear()
Reset the abstract state.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
C enum tag type, i.e., c_enum_typet with an identifier.
std::vector< parametert > parameterst
const parameterst & parameters() const
const typet & return_type() const
bool is_class_template() const
void print(std::ostream &out, unsigned indent=0) const
irep_idt class_identifier
cpp_idt & get_id(const irep_idt &identifier)
std::set< cpp_idt * > id_sett
cpp_scopet & get_scope(const irep_idt &identifier)
cpp_scopet & current_scope()
cpp_scopet & get_root_scope()
cpp_scopet & get_parent() const
cpp_idt & insert(const irep_idt &_base_name)
id_sett lookup(const irep_idt &base_name_to_lookup, lookup_kindt kind)
bool is_root_scope() const
exprt::operandst argumentst
void remove_templates(resolve_identifierst &identifiers)
void filter(resolve_identifierst &identifiers, const wantt want)
exprt convert_template_parameter(const cpp_idt &id)
exprt convert_identifier(const cpp_idt &id, const cpp_typecheck_fargst &fargs)
cpp_scopet & resolve_namespace(const cpp_namet &cpp_name)
std::vector< exprt > resolve_identifierst
cpp_typecheck_resolvet(class cpp_typecheckt &_cpp_typecheck)
void remove_duplicates(resolve_identifierst &identifiers)
void filter_for_namespaces(cpp_scopest::id_sett &id_set)
exprt resolve(const cpp_namet &cpp_name, const wantt want, const cpp_typecheck_fargst &fargs, bool fail_with_exception=true)
void resolve_argument(exprt &argument, const cpp_typecheck_fargst &fargs)
exprt do_builtin(const irep_idt &base_name, const cpp_typecheck_fargst &fargs, const cpp_template_args_non_tct &template_args)
void show_identifiers(const irep_idt &base_name, const resolve_identifierst &identifiers, std::ostream &out)
void filter_for_named_scopes(cpp_scopest::id_sett &id_set)
void make_constructors(resolve_identifierst &identifiers)
void guess_function_template_args(resolve_identifierst &identifiers, const cpp_typecheck_fargst &fargs)
guess arguments of function templates
void convert_identifiers(const cpp_scopest::id_sett &id_set, const cpp_typecheck_fargst &fargs, resolve_identifierst &identifiers)
source_locationt source_location
void disambiguate_functions(resolve_identifierst &identifiers, const cpp_typecheck_fargst &fargs)
void apply_template_args(resolve_identifierst &identifiers, const cpp_template_args_non_tct &template_args, const cpp_typecheck_fargst &fargs)
cpp_scopet * original_scope
void resolve_with_arguments(cpp_scopest::id_sett &id_set, const irep_idt &base_name, const cpp_typecheck_fargst &fargs)
cpp_scopet & resolve_scope(const cpp_namet &cpp_name, irep_idt &base_name, cpp_template_args_non_tct &template_args)
struct_tag_typet disambiguate_template_classes(const irep_idt &base_name, const cpp_scopest::id_sett &id_set, const cpp_template_args_non_tct &template_args)
disambiguate partial specialization
cpp_typecheckt & cpp_typecheck
void exact_match_functions(resolve_identifierst &identifiers, const cpp_typecheck_fargst &fargs)
void guess_template_args(const typet &template_parameter, const typet &desired_type)
void typecheck_type(typet &) override
instantiation_stackt instantiation_stack
template_mapt template_map
bool cpp_is_pod(const typet &type) const
void show_instantiation_stack(std::ostream &)
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 elaborate_class_template(const typet &type)
elaborate class template instances
bool builtin_factory(const irep_idt &) override
bool subtype_typecast(const struct_typet &from, const struct_typet &to) const
std::string to_string(const typet &) override
bool disable_access_control
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{})
const symbolt & class_template_symbol(const source_locationt &source_location, const symbolt &template_symbol, const cpp_template_args_tct &specialization_template_args, const cpp_template_args_tct &full_template_args)
void typecheck_expr_member(exprt &) override
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
bool starts_with(const char *s) const
equivalent of as_string().starts_with(s)
Base class for all expressions.
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
bool is_constant() const
Return whether the expression is a constant.
typet & type()
Return the type of the expression.
const source_locationt & source_location() const
source_locationt & add_source_location()
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
There are a large number of kinds of tree structured or tree-like data in CPROVER.
bool get_bool(const irep_idt &name) const
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const irept & find(const irep_idt &name) const
const irep_idt & get(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
Extract member of struct or union.
source_locationt source_location
message_handlert & get_message_handler()
mstreamt & warning() const
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
const irep_idt & get_function() const
A struct tag type, i.e., struct_typet with an identifier.
Structure type, corresponds to C style structs.
Base type for structs and unions.
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
source_locationt location
Source code location of definition of symbol.
typet type
Type of symbol.
irep_idt name
The unique identifier.
exprt value
Initial value of symbol.
A tag-based type, i.e., typet with an identifier.
exprt lookup(const irep_idt &identifier) const
void build_unassigned(const template_typet &template_type)
void print(std::ostream &out) const
cpp_template_args_tct build_template_args(const template_typet &template_type) const
An expression denoting a type.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
source_locationt & add_source_location()
A union tag type, i.e., union_typet with an identifier.
void cpp_convert_plain_type(typet &type, message_handlert &message_handler)
cpp_declarationt & to_cpp_declaration(irept &irep)
cpp_namet & to_cpp_name(irept &cpp_name)
cpp_template_args_non_tct & to_cpp_template_args_non_tc(irept &irep)
cpp_template_args_tct & to_cpp_template_args_tc(irept &irep)
const template_parameter_symbol_typet & to_template_parameter_symbol_type(const typet &type)
Cast a typet to a template_parameter_symbol_typet.
std::string cpp_type2name(const typet &type)
bool cpp_typecheck(cpp_parse_treet &cpp_parse_tree, symbol_table_baset &symbol_table, const std::string &module, message_handlert &message_handler)
C++ Language Type Checking.
C++ Language Type Checking.
C++ Language Type Checking.
symbol_exprt cpp_symbol_expr(const symbolt &symbol)
const std::string & id2string(const irep_idt &d)
bool is_number(const typet &type)
Returns true if the type is a rational, real, integer, natural, complex, unsignedbv,...
const merged_typet & to_merged_type(const typet &type)
conversion to merged_typet
const std::string integer2string(const mp_integer &n, unsigned base)
bool is_reference(const typet &type)
Returns true if the type is a reference.
bool is_rvalue_reference(const typet &type)
Returns if the type is an R value reference.
const reference_typet & to_reference_type(const typet &type)
Cast a typet to a reference_typet.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
bool simplify(exprt &expr, const namespacet &ns)
#define CHECK_RETURN(CONDITION)
#define UNREACHABLE
This should be used to mark dead code.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
API to expression classes.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
cpp_template_args_tct full_args
cpp_template_args_tct specialization_args