39 original_scope(nullptr)
48 for(
const auto &id_ptr : id_set)
50 const cpp_idt &identifier = *id_ptr;
57 identifiers.push_back(e);
68 old_identifiers.swap(identifiers);
70 for(
const auto &old_id : old_identifiers)
79 identifiers.push_back(e);
90 old_identifiers.swap(identifiers);
92 for(
const auto &old_id : old_identifiers)
99 identifiers.push_back(e);
106 if(identifiers.size()==1)
109 exprt e=*identifiers.begin();
112 const symbolt &template_symbol=
128 identifiers.push_back(
137 old_identifiers.swap(identifiers);
139 for(
const auto &old_id : old_identifiers)
142 identifiers.push_back(old_id);
150 old_identifiers.swap(identifiers);
152 std::set<irep_idt> ids;
153 std::set<exprt> other;
155 for(
const auto &old_id : old_identifiers)
159 if(old_id.id() == ID_symbol)
161 else if(old_id.id() == ID_type && old_id.type().id() == ID_struct_tag)
163 else if(old_id.id() == ID_type && old_id.type().id() == ID_union_tag)
168 if(other.insert(old_id).second)
169 identifiers.push_back(old_id);
173 if(ids.insert(
id).second)
174 identifiers.push_back(old_id);
183 std::cout <<
"RESOLVE MAP:\n";
195 <<
"without instance:\n"
220 const symbolt &compound_symbol=
224 compound_symbol.
type.
id() == ID_struct ||
225 compound_symbol.
type.
id() == ID_union);
255 this_class_identifier <<
'\n';
258 const exprt &this_expr=
271 this_expr.
type().
id() == ID_pointer,
272 "this argument should be pointer");
275 object.copy_to_operands(this_expr);
281 object.set(ID_C_lvalue,
true);
288 if(object_type.
id()==ID_struct ||
289 object_type.
id()==ID_union)
300 if(
object.is_not_nil())
339 else if(symbol.
type.
id()==ID_c_enum)
343 else if(symbol.
type.
id() == ID_struct)
347 else if(symbol.
type.
id() == ID_union)
384 old_identifiers.swap(identifiers);
386 for(
const auto &old_id : old_identifiers)
393 match = (old_id.id() == ID_type);
397 match = (old_id.id() != ID_type);
409 identifiers.push_back(old_id);
421 old_identifiers.swap(identifiers);
426 for(
const auto &old_id : old_identifiers)
431 identifiers.push_back(old_id);
440 old_identifiers.swap(identifiers);
443 std::multimap<std::size_t, exprt> distance_map;
445 for(
const auto &old_id : old_identifiers)
447 unsigned args_distance;
451 std::size_t template_distance=0;
453 if(!old_id.type().get(ID_C_template).empty())
454 template_distance = old_id.type()
455 .find(ID_C_template_arguments)
462 std::size_t total_distance=
464 1000*template_distance+args_distance;
466 distance_map.insert({total_distance, old_id});
470 old_identifiers.clear();
473 if(!distance_map.empty())
475 auto range = distance_map.equal_range(distance_map.begin()->first);
476 for(
auto it = range.first; it != range.second; ++it)
477 old_identifiers.push_back(it->second);
480 if(old_identifiers.size() > 1 && fargs.
in_use)
484 for(resolve_identifierst::const_iterator old_it = old_identifiers.begin();
485 old_it != old_identifiers.end();
489 std::cout <<
"I1: " << old_it->get(ID_identifier) <<
'\n';
492 if(old_it->type().id() != ID_code)
494 identifiers.push_back(*old_it);
500 for(resolve_identifierst::const_iterator resolve_it = old_it + 1;
501 resolve_it != old_identifiers.end();
504 if(resolve_it->type().id() != ID_code)
512 "parameter numbers should match");
518 i<f1.
parameters().size() && (f1_better || f2_better);
530 if(type1.
id()==ID_pointer)
536 if(type2.
id()==ID_pointer)
545 if(followed1.
id() != ID_struct || followed2.
id() != ID_struct)
561 if(!f1_better || f2_better)
562 identifiers.push_back(*resolve_it);
568 identifiers.swap(old_identifiers);
579 for(
const auto &identifier : identifiers)
581 if(identifier.id() != ID_type)
584 new_identifiers.push_back(identifier);
599 exprt pod_constructor1(ID_pod_constructor, t1);
600 new_identifiers.push_back(pod_constructor1);
607 exprt pod_constructor2(ID_pod_constructor, t2);
608 new_identifiers.push_back(pod_constructor2);
612 if(symbol_type.
id()==ID_c_enum_tag)
616 exprt pod_constructor3(ID_pod_constructor, t3);
617 new_identifiers.push_back(pod_constructor3);
620 else if(symbol_type.
id()==ID_struct)
633 type.
id() == ID_code &&
640 new_identifiers.push_back(e);
646 identifiers.swap(new_identifiers);
653 if(argument.
id() == ID_ambiguous)
673 if(base_name==ID_unsignedbv ||
674 base_name==ID_signedbv)
676 if(arguments.size()!=1)
680 << base_name <<
" expects one template argument, but got "
685 exprt argument=arguments.front();
687 if(argument.
id()==ID_type)
691 << base_name <<
" expects one integer template argument, "
711 <<
"template argument must be greater than zero"
719 else if(base_name==ID_fixedbv)
721 if(arguments.size()!=2)
725 << base_name <<
" expects two template arguments, but got "
730 exprt argument0=arguments[0];
732 exprt argument1=arguments[1];
735 if(argument0.
id()==ID_type)
739 << base_name <<
" expects two integer template arguments, "
744 if(argument1.
id()==ID_type)
748 << base_name <<
" expects two integer template arguments, "
755 if(!width.has_value())
765 if(!integer_bits.has_value())
777 <<
"template argument must be greater than zero"
782 if(*integer_bits < 0)
786 <<
"template argument must be greater or equal zero"
791 if(*integer_bits > *width)
795 <<
"template argument must be smaller or equal width"
804 else if(base_name==ID_integer)
806 if(!arguments.empty())
810 << base_name <<
" expects no template arguments"
822 else if(base_name==
"dump_scopes")
830 else if(base_name==
"current_scope")
837 else if(base_name == ID_size_t)
841 else if(base_name == ID_ssize_t)
869 irept::subt::const_iterator
pos=cpp_name.
get_sub().begin();
881 std::string final_base_name;
886 if(
pos->id()==ID_name)
887 final_base_name+=
pos->get_string(ID_identifier);
888 else if(
pos->id()==ID_template_args)
890 else if(
pos->id()==
"::")
904 std::cout <<
"X: " << id_set.size() <<
'\n';
932 <<
"scope '" << final_base_name <<
"' not found" <<
messaget::eom;
935 else if(id_set.size()>=2)
958 final_base_name.clear();
960 else if(
pos->id()==ID_operator)
962 final_base_name+=
"operator";
964 irept::subt::const_iterator next=
pos+1;
968 next->id() == ID_cpp_name || next->id() == ID_pointer ||
969 next->id() == ID_int || next->id() == ID_char ||
970 next->id() == ID_c_bool || next->id() == ID_merged_type)
975 op_name.
swap(next_ir);
982 final_base_name+=
pos->id_string();
987 base_name=final_base_name;
1007 std::set<irep_idt> primary_templates;
1009 for(
const auto &id_ptr : id_set)
1011 const irep_idt id = id_ptr->identifier;
1019 if(!specialization_of.
empty())
1020 primary_templates.insert(specialization_of);
1022 primary_templates.insert(
id);
1027 if(primary_templates.size()>=2)
1036 const symbolt &primary_template_symbol=
1049 full_template_args_tc=
1052 primary_template_symbol,
1053 full_template_args);
1055 for(
auto &arg : full_template_args_tc.
arguments())
1057 if(arg.id() == ID_type)
1059 if(arg.id() == ID_symbol)
1079 std::vector<matcht> matches;
1083 matcht(full_template_args_tc, full_template_args_tc,
1084 primary_template_symbol.
name));
1086 for(
const auto &id_ptr : id_set)
1088 const irep_idt id = id_ptr->identifier;
1110 full_template_args_tc.
arguments().size() ==
1111 partial_specialization_args.
arguments().size(),
1112 "number of arguments should match");
1120 if(template_scope==
nullptr)
1124 <<
"class template instantiation error"
1132 for(std::size_t i=0; i<full_template_args_tc.
arguments().size(); i++)
1134 if(full_template_args_tc.
arguments()[i].id()==ID_type)
1136 full_template_args_tc.
arguments()[i].type());
1155 primary_template_symbol,
1156 partial_specialization_args);
1161 partial_specialization_args_tc.
arguments().size() ==
1162 full_template_args_tc.
arguments().size(),
1163 "argument numbers must match");
1165 if(partial_specialization_args_tc==
1166 full_template_args_tc)
1168 matches.push_back(
matcht(
1169 guessed_template_args, full_template_args_tc,
id));
1176 std::sort(matches.begin(), matches.end());
1179 for(std::vector<matcht>::const_iterator
1180 m_it=matches.begin();
1181 m_it!=matches.end();
1184 std::cout <<
"M: " << m_it->cost
1185 <<
" " << m_it->id <<
'\n';
1191 const matcht &match=*matches.begin();
1205 if(instance.
type.
id()!=ID_struct)
1258 else if(id_set.size()==1)
1277 for(
const auto &id_expr : identifiers)
1281 if(id_expr.id()==ID_type)
1289 if(id_expr.type().get_bool(ID_is_template))
1292 if(id_expr.id()==ID_member)
1297 else if(id_expr.id() == ID_pod_constructor)
1299 out <<
"constructor ";
1302 else if(id_expr.id()==ID_template_function_instance)
1312 if(id_expr.type().get_bool(ID_is_template))
1315 else if(id_expr.type().id()==ID_code)
1321 out <<
" " <<
id <<
"(";
1325 for(
const auto ¶meter : parameters)
1327 const typet ¶meter_type = parameter.type();
1339 if(!parameters.empty())
1349 if(id_expr.id()==ID_symbol)
1352 out <<
" (" << symbol.
location <<
")";
1354 else if(id_expr.id()==ID_template_function_instance)
1358 out <<
" (" << symbol.
location <<
")";
1370 bool fail_with_exception)
1383 std::cout <<
"base name: " << base_name <<
'\n';
1384 std::cout <<
"template args: " << template_args.
pretty() <<
'\n';
1396 return do_builtin(base_name, fargs, template_args);
1400 if(base_name==
"__func__" ||
1401 base_name==
"__FUNCTION__" ||
1402 base_name==
"__PRETTY_FUNCTION__")
1408 return std::move(s);
1417 if(template_args.
is_nil())
1429 id_set.insert(&builtin_id);
1445 if(!fail_with_exception)
1479 bool have_classes=
false, have_methods=
false;
1481 for(
const auto &id_ptr : id_set)
1483 const irep_idt id = id_ptr->identifier;
1492 if(want==
wantt::BOTH && have_classes && have_methods)
1494 if(!fail_with_exception)
1511 identifiers.push_back(
exprt(ID_type, instance));
1517 id_set, fargs, identifiers);
1520 identifiers, template_args, fargs);
1526 id_set, fargs, identifiers);
1533 filter(identifiers, want);
1536 std::cout <<
"P0 " << base_name <<
" " << identifiers.size() <<
'\n';
1549 std::cout <<
"P1 " << base_name <<
" " << new_identifiers.size() <<
'\n';
1558 std::cout <<
"P2 " << base_name <<
" " << new_identifiers.size() <<
'\n';
1564 if(new_identifiers.empty())
1566 new_identifiers=identifiers;
1568 if(template_args.
is_nil())
1572 if(new_identifiers.empty())
1573 new_identifiers=identifiers;
1579 std::cout <<
"P3 " << base_name <<
" " << new_identifiers.size() <<
'\n';
1588 std::cout <<
"P4 " << base_name <<
" " << new_identifiers.size() <<
'\n';
1593 if(new_identifiers.size()==1)
1595 result=*new_identifiers.begin();
1600 if(!fail_with_exception)
1603 if(new_identifiers.empty())
1607 <<
"found no match for symbol '" << base_name <<
"', candidates are:\n";
1614 <<
"symbol '" << base_name <<
"' does not uniquely resolve:\n";
1618 exprt e1=*new_identifiers.begin();
1619 exprt e2=*(++new_identifiers.begin());
1622 <<
"e1.type==e2.type: " << (e1.
type() == e2.
type()) <<
'\n';
1624 <<
"e1.id()==e2.id(): " << (e1.
id() == e2.
id()) <<
'\n';
1626 <<
"e1.iden==e2.iden: "
1627 << (e1.
get(ID_identifier) == e2.
get(ID_identifier)) <<
'\n';
1637 for(
const auto &op : fargs.
operands)
1654 if(result.
get_bool(ID_C_not_accessible))
1657 if(!fail_with_exception)
1662 <<
"error: member '" << result.
get(ID_component_name)
1663 <<
"' is not accessible";
1673 if(!fail_with_exception)
1679 <<
"error: expected expression, but got type '"
1687 if(result.
id()!=ID_type)
1689 if(!fail_with_exception)
1695 <<
"error: expected type, but got expression '"
1710 const exprt &template_expr,
1711 const exprt &desired_expr)
1713 if(template_expr.
id()==ID_cpp_name)
1730 for(
const auto &id_ptr : id_set)
1738 if(e.
id()==ID_unassigned)
1750 const typet &template_type,
1751 const typet &desired_type)
1784 std::cout <<
"TT: " << template_type.
pretty() <<
'\n';
1785 std::cout <<
"DT: " << desired_type.
pretty() <<
'\n';
1788 if(template_type.
id()==ID_cpp_name)
1815 for(
const auto &id_ptr : id_set)
1824 if(t.
id()==ID_unassigned)
1832 std::cout <<
"ASSIGN " <<
id.identifier <<
" := "
1841 else if(template_type.
id()==ID_merged_type)
1855 else if(template_type.
id()==ID_pointer)
1857 if(desired_type.
id() == ID_pointer)
1862 else if(template_type.
id()==ID_array)
1864 if(desired_type.
id() == ID_array)
1909 const symbolt &template_symbol=
1926 if(function_declarator.
type().
id()!=ID_function_type)
1930 <<
"expected function type for function template"
1942 if(template_scope==
nullptr)
1946 << template_identifier <<
'\n'
1947 <<
"function template instantiation error"
1959 exprt::operandst::const_iterator it=fargs.
operands.begin();
1960 for(
const auto ¶meter : parameters)
1965 if(parameter.id()==ID_cpp_declaration)
1972 arg_declaration.
declarators().size() == 1,
"exactly one declarator");
1977 merge_type(arg_declaration.
type());
2001 typet function_type=
2008 function_type.
set(ID_C_template, template_symbol.
name);
2009 function_type.
set(ID_C_template_arguments, template_args);
2013 exprt template_function_instance(
2014 ID_template_function_instance, function_type);
2016 return template_function_instance;
2024 if(expr.
id()!=ID_symbol)
2027 const symbolt &template_symbol =
2034 if(template_args_non_tc.
is_nil())
2055 template_args_non_tc);
2102 fargs.
operands.begin()->type().get(ID_identifier));
2110 "method should exist in struct");
2129 unsigned &args_distance,
2139 if(expr.
id()==ID_member ||
2154 const typet &object_type =
2157 object.set(ID_C_lvalue,
true);
2167 fargs.
operands.size() == parameters.size())
2199 for(
const auto &id_ptr : id_set)
2203 if(
id.is_class() ||
id.is_enum() ||
id.is_namespace())
2207 new_set.insert(&
id);
2209 else if(
id.is_typedef())
2223 if(symbol.
type.
id()==ID_struct)
2230 new_set.insert(&class_id);
2245 if(symbol.
type.
id() == ID_struct)
2247 id.print(std::cout);
2248 assert(
id.is_scope);
2249 new_set.insert(&
id);
2268 std::cout <<
"E: " << e.
pretty() <<
'\n';
2274 if(e.
type().
id() == ID_template_parameter_symbol_type)
2280 irep_idt identifier=type.get_identifier();
2285 if(symbol.
type.
id() == ID_template_parameter_symbol_type)
2287 else if(symbol.
type.
id()==ID_struct ||
2288 symbol.
type.
id()==ID_union ||
2289 symbol.
type.
id()==ID_c_enum)
2296 new_set.insert(&class_id);
2306 id_set.swap(new_set);
2313 for(cpp_scopest::id_sett::iterator
2318 if((*it)->is_namespace())
2322 cpp_scopest::id_sett::iterator old(it);
2335 for(
const auto &arg : fargs.
operands)
2339 if(final_type.
id()!=ID_struct && final_type.
id()!=ID_union)
2345 id_set.insert(tmp_set.begin(), tmp_set.end());
bool has_component_rec(const typet &type, const irep_idt &component_name, const namespacet &ns)
C Language Type Checking.
unsignedbv_typet size_type()
signedbv_typet signed_int_type()
pointer_typet pointer_type(const typet &subtype)
signedbv_typet signed_size_type()
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
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 has_ellipsis() const
const declaratorst & declarators() const
irep_idt get_specialization_of() const
bool is_class_template() const
cpp_template_args_non_tct & partial_specialization_args()
template_typet & template_type()
typet merge_type(const typet &declaration_type) const
void print(std::ostream &out, unsigned indent=0) const
irep_idt class_identifier
bool is_qualified() const
bool has_template_args() const
const source_locationt & source_location() const
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
bool has_unassigned() const
exprt::operandst operands
bool match(const code_typet &code_type, unsigned &distance, cpp_typecheckt &cpp_typecheck) const
void add_object(const exprt &expr)
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.
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.
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 typet & follow(const typet &) const
Resolve type symbol to the type it points to.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
const typet & base_type() const
The type of the data what we point to.
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.
const componentst & components() const
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
bool has_component(const irep_idt &component_name) const
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.
const irep_idt & get_identifier() const
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.
bool has_prefix(const std::string &s, const std::string &prefix)
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