Go to the documentation of this file.
41 const irep_idt &
id = b.type().get_identifier();
42 if(
lookup(
id).base_name == base_name)
55 if(expr.
id()==ID_cpp_name)
57 else if(expr.
id()==
"cpp-this")
59 else if(expr.
id() == ID_pointer_to_member)
61 else if(expr.
id() == ID_new_object)
67 else if(expr.
id()==
"explicit-typecast")
69 else if(expr.
id()==
"explicit-constructor-call")
71 else if(expr.
id()==ID_code)
74 std::cerr <<
"E: " << expr.
pretty() <<
'\n';
75 std::cerr <<
"cpp_typecheckt::typecheck_expr_main got code\n";
79 else if(expr.
id()==ID_symbol)
83 std::cerr <<
"E: " << expr.
pretty() <<
'\n';
84 std::cerr <<
"cpp_typecheckt::typecheck_expr_main got symbol\n";
87 else if(expr.
id()==
"__is_base_of")
101 if(base.
id()!=ID_struct || deriv.
id()!=ID_struct)
114 else if(expr.
id()==ID_msc_uuidof)
119 expr.
set(ID_C_lvalue,
true);
121 else if(expr.
id()==ID_noexcept)
126 else if(expr.
id()==ID_initializer_list)
128 expr.
type().
id(ID_initializer_list);
149 error() <<
"error: lvalue to rvalue conversion" <<
eom;
160 error() <<
"error: array to pointer conversion" <<
eom;
171 error() <<
"error: function to pointer conversion" <<
eom;
182 error() <<
"error: lvalue to rvalue conversion" <<
eom;
193 error() <<
"error: array to pointer conversion" <<
eom;
204 error() <<
"error: function to pointer conversion" <<
eom;
209 if(expr.
op1().
get(ID_statement)==ID_throw &&
210 expr.
op2().
get(ID_statement)!=ID_throw)
212 else if(expr.
op2().
get(ID_statement)==ID_throw &&
213 expr.
op1().
get(ID_statement)!=ID_throw)
215 else if(expr.
op1().
type().
id()==ID_empty &&
221 error() <<
"error: bad types for operands" <<
eom;
276 error() <<
"error: types are incompatible.\n"
285 expr.
set(ID_C_lvalue,
true);
305 static_cast<const typet &
>(expr.
find(ID_type_arg));
307 if(type.
id()==ID_cpp_name)
319 if(symbol_expr.
id()!=ID_type)
325 else if(type.
id()==ID_array)
339 if(symbol_expr.
id()!=ID_type)
362 if(expr.
id()==ID_cpp_name)
364 else if(expr.
id()==ID_member)
369 else if(expr.
id()==ID_ptrmember)
377 std::string op_name=
"operator->";
385 {to_unary_expr(expr).op()},
411 typet t = it->type();
417 t.
id() == ID_struct || t.
id() == ID_union || t.
id() == ID_c_enum ||
418 t.
id() == ID_c_enum_tag || t.
id() == ID_struct_tag ||
419 t.
id() == ID_union_tag)
443 { ID_unary_minus,
"-" },
455 { ID_notequal,
"!=" },
456 { ID_dereference,
"*" },
457 { ID_ptrmember,
"->" },
468 else if(expr.
id()==ID_dereference &&
474 if(expr.
id()==
"explicit-typecast")
480 std::string op_name=std::string(
"operator")+
"("+
cpp_type2name(t)+
")";
486 bool found_in_struct=
false;
490 if(t0.
id()==ID_struct)
494 if(!c.get_bool(ID_from_base) && c.get_base_name() == op_name)
496 found_in_struct=
true;
505 exprt member(ID_member);
506 member.
add(ID_component_cpp_name) = cpp_name;
517 for(exprt::operandst::const_iterator
519 it!=(expr).operands().end();
521 function_call.
arguments().push_back(*it);
526 if(expr.
id()==ID_ptrmember)
535 expr.
swap(function_call);
545 if(expr.
id()==ID_dereference)
546 assert(!expr.
get_bool(ID_C_implicit));
548 std::string op_name=std::string(
"operator")+e->op_name;
590 exprt member(ID_member);
591 member.
add(ID_component_cpp_name) = cpp_name;
606 for(exprt::operandst::const_iterator
610 function_call.
arguments().push_back(*it);
643 function_call.
arguments().push_back(*it);
647 if(expr.
id()==ID_ptrmember)
672 error() <<
"address_of expects one operand" <<
eom;
681 error() <<
"expr not an lvalue" <<
eom;
685 if(op.
type().
id() == ID_code)
691 address.
set(ID_C_implicit,
true);
695 if(op.
id() == ID_address_of && op.
get_bool(ID_C_implicit))
702 if(!args.empty() && args.front().get_this())
706 op.
type().
add(ID_to_member) = symbol;
708 if(code_type.
get_bool(ID_C_is_virtual))
711 error() <<
"error: pointers to virtual methods"
712 <<
" are currently not implemented" <<
eom;
717 else if(op.
id() == ID_ptrmember &&
to_unary_expr(op).op().
id() ==
"cpp-this")
720 expr.
type().
add(ID_to_member) =
744 if(exception_type.
id() == ID_empty)
747 error() <<
"cannot throw void" <<
eom;
752 expr.
set(ID_exception_list,
761 if(expr.
type().
id()==ID_array)
770 bool size_is_unsigned=(size.
type().
id()==ID_unsignedbv);
775 expr.
set(ID_statement, ID_cpp_new_array);
790 expr.
set(ID_statement, ID_cpp_new);
797 object_expr.
set(ID_C_lvalue,
true);
802 exprt &initializer=
static_cast<exprt &
>(expr.
add(ID_initializer));
805 if(!initializer.
operands().empty() &&
806 expr.
get(ID_statement)==ID_cpp_new_array)
810 error() <<
"new with array type must not use initializer" <<
eom;
818 expr.
add(ID_initializer).
swap(code.value());
827 if(size_of_opt.has_value())
829 auto &sizeof_expr =
static_cast<exprt &
>(expr.
add(ID_sizeof));
830 sizeof_expr = size_of_opt.value();
831 sizeof_expr.
add(ID_C_c_sizeof_type) =
840 if(src.
id()==ID_comma)
862 if(!new_expr.has_value())
883 if(expr.
type().
id()==ID_cpp_name)
894 if(symbol_expr.
id()==ID_type)
901 static_cast<const exprt &
>(
static_cast<const irept &
>(expr.
type())),
918 if(op.id() == ID_initializer_list)
927 exprt tmp(ID_compound_literal, expr.
type());
930 expr.
set(ID_C_lvalue,
true);
947 error() <<
"invalid explicit cast:\n"
948 <<
"operand type: '" <<
to_string(op.type()) <<
"'\n"
956 error() <<
"explicit typecast expects 0 or 1 operands" <<
eom;
967 expr.
id(
"explicit-typecast");
972 assert(expr.
type().
id()==ID_struct);
987 error() <<
"`this' is not allowed here" <<
eom;
995 assert(this_expr.
type().
id()==ID_pointer);
1006 error() <<
"delete expects one operand" <<
eom;
1012 if(statement==ID_cpp_delete)
1015 else if(statement==ID_cpp_delete_array)
1026 error() <<
"delete takes a pointer type operand, but got '"
1042 new_object.
set(ID_C_lvalue,
true);
1048 if(destructor_code.has_value())
1052 expr.
set(ID_destructor, destructor_code.value());
1062 std::cout <<
"E: " << expr.pretty() <<
'\n';
1074 error() <<
"error: member operator expects one operand" <<
eom;
1089 op0.
type().
id() != ID_struct && op0.
type().
id() != ID_struct_tag)
1091 exprt tmp(ID_cpp_dummy_destructor);
1102 if(followed_op0_type.
id()!=ID_struct &&
1103 followed_op0_type.
id()!=ID_union)
1106 error() <<
"error: member operator requires struct/union type "
1107 <<
"on left hand side but got '" <<
to_string(followed_op0_type)
1118 error() <<
"error: member operator got incomplete type "
1119 <<
"on left hand side" <<
eom;
1143 if(symbol_expr.
id()==ID_dereference)
1145 assert(symbol_expr.
get_bool(ID_C_implicit));
1147 symbol_expr.
swap(tmp);
1150 assert(symbol_expr.
id()==ID_symbol ||
1151 symbol_expr.
id()==ID_member ||
1152 symbol_expr.
id()==ID_constant);
1158 if(symbol_expr.
id()==ID_symbol)
1161 symbol_expr.
type().
id() == ID_code &&
1165 error() <<
"error: member '"
1166 <<
lookup(symbol_expr.
get(ID_identifier)).base_name
1167 <<
"' is a constructor" <<
eom;
1179 error() <<
"error: '" << symbol_expr.
get(ID_identifier)
1180 <<
"' is not static member "
1189 else if(symbol_expr.
id()==ID_constant)
1195 const irep_idt component_name=symbol_expr.
get(ID_component_name);
1197 expr.
remove(ID_component_cpp_name);
1198 expr.
set(ID_component_name, component_name);
1201 const irep_idt &component_name=expr.
get(ID_component_name);
1202 INVARIANT(!component_name.
empty(),
"component name should not be empty");
1208 op0.
type().
id() == ID_struct || op0.
type().
id() == ID_union ||
1209 op0.
type().
id() == ID_struct_tag || op0.
type().
id() == ID_union_tag);
1221 error() <<
"error: member '" << component_name <<
"' of '"
1228 if(expr.
type().
id()==ID_code)
1231 symbol_tablet::symbolst::const_iterator it=
1236 if(it->second.value.id() == ID_cpp_not_typechecked)
1246 assert(expr.
id()==ID_ptrmember);
1251 error() <<
"error: ptrmember operator expects one operand" <<
eom;
1259 if(op.type().id() != ID_pointer)
1262 error() <<
"error: ptrmember operator requires pointer type "
1263 <<
"on left hand side, but got '" <<
to_string(op.type()) <<
"'"
1271 op.id(ID_dereference);
1272 op.add_to_operands(std::move(tmp));
1288 error() <<
"cast expressions expect one operand" <<
eom;
1298 f_op.
get_sub().front().get(ID_identifier);
1300 if(f_op.
get_sub().size()!=2 ||
1301 f_op.
get_sub()[1].id()!=ID_template_args)
1304 error() <<
id <<
" expects template argument" <<
eom;
1308 irept &template_arguments=f_op.
get_sub()[1].add(ID_arguments);
1310 if(template_arguments.
get_sub().size()!=1)
1313 error() <<
id <<
" expects one template argument" <<
eom;
1317 irept &template_arg=template_arguments.
get_sub().front();
1319 if(template_arg.
id() != ID_type && template_arg.
id() != ID_ambiguous)
1322 error() <<
id <<
" expects a type as template argument" <<
eom;
1327 template_arguments.
get_sub().front().add(ID_type));
1334 if(
id==ID_const_cast)
1339 error() <<
"type mismatch on const_cast:\n"
1345 else if(
id==ID_dynamic_cast)
1350 error() <<
"type mismatch on dynamic_cast:\n"
1356 else if(
id==ID_reinterpret_cast)
1361 error() <<
"type mismatch on reinterpret_cast:\n"
1367 else if(
id==ID_static_cast)
1372 error() <<
"type mismatch on static_cast:\n"
1381 expr.
swap(new_expr);
1391 if(expr.
get_sub().size()==1 &&
1392 expr.
get_sub()[0].id()==ID_name)
1398 identifier, fargs.
operands, source_location))
1400 expr = std::move(*gcc_polymorphic);
1405 for(std::size_t i=0; i<expr.
get_sub().size(); i++)
1407 if(expr.
get_sub()[i].id()==ID_cpp_name)
1414 typet name(ID_name);
1415 name.
set(ID_identifier, tmp);
1422 if(expr.
get_sub().size()>=1 &&
1423 expr.
get_sub().front().id()==ID_name)
1427 if(
id==ID_const_cast ||
1428 id==ID_dynamic_cast ||
1429 id==ID_reinterpret_cast ||
1432 expr.
id(ID_cast_expression);
1444 assert(symbol_expr.
id()!=ID_type);
1446 if(symbol_expr.
id()==ID_member)
1456 if(symbol_expr.
type().
id()!=ID_code)
1459 error() <<
"object missing" <<
eom;
1468 exprt ptrmem(ID_ptrmember);
1472 ptrmem.
add(ID_component_cpp_name)=expr;
1476 symbol_expr.
swap(ptrmem);
1485 if(expr.
id()==ID_symbol)
1497 tmp.
set(ID_C_implicit,
true);
1499 tmp.
set(ID_C_lvalue,
true);
1510 bool is_qualified=
false;
1515 if(expr.
function().
get(ID_component_cpp_name)==ID_cpp_name)
1534 if(expr.
function().
id() == ID_pod_constructor)
1546 exprt typecast(
"explicit-typecast");
1547 typecast.
type()=pod;
1552 expr.
swap(typecast);
1557 error() <<
"zero or one argument expected" <<
eom;
1563 else if(expr.
function().
id() == ID_cast_expression)
1571 else if(expr.
function().
id() == ID_cpp_dummy_destructor)
1587 const exprt &bound =
1593 error() <<
"pointer-to-member not bound" <<
eom;
1598 assert(bound.
type().
id()==ID_pointer);
1623 error() <<
"expecting code as argument" <<
eom;
1632 if(op0.
id()==ID_member || op0.
id()==ID_ptrmember)
1634 vtptr_member.
id(op0.
id());
1639 vtptr_member.
id(ID_ptrmember);
1640 exprt this_expr(
"cpp-this");
1648 this_type.base_type().get_string(ID_identifier) +
"::@vtable_pointer";
1658 vtptr_member.
set(ID_component_name, vtable_name);
1665 exprt vtentry_member(ID_ptrmember);
1667 vtentry_member.
set(ID_component_name, vtentry_component_name);
1670 assert(vtentry_member.
type().
id()==ID_pointer);
1675 vtentry_member.
swap(tmp);
1698 exprt member(ID_member);
1699 member.
add(ID_component_cpp_name)=cppname;
1711 error() <<
"function call expects function or function "
1712 <<
"pointer as argument, but got '"
1720 if(expr.
type().
id()==ID_constructor)
1727 assert(parameters.size()>=1);
1732 expr.
type() = this_type.base_type();
1737 tmp_object_expr.
set(ID_C_lvalue,
true);
1738 tmp_object_expr.
set(ID_mode, ID_cpp);
1742 exprt new_object(ID_new_object, tmp_object_expr.
type());
1743 new_object.
set(ID_C_lvalue,
true);
1753 if(member.
get_bool(ID_C_not_accessible))
1756 tmp_object_expr.
set(ID_C_not_accessible,
true);
1757 tmp_object_expr.
set(ID_C_access, member.
get(ID_C_access));
1767 for(
const auto &c : components)
1769 const typet &type = c.type();
1772 !c.get_bool(ID_from_base) && type.
id() == ID_code &&
1787 tmp_object_expr.
add(ID_initializer)=new_code;
1788 expr.
swap(tmp_object_expr);
1806 !parameters.empty() && parameters.front().get_this() &&
1813 parameter.
type().
id() == ID_pointer,
1814 "`this' parameter should be a pointer");
1817 operand.
type().
id() != ID_pointer &&
1851 if(parameters.size()>expr.
arguments().size())
1855 for(; i<parameters.size(); i++)
1857 if(!parameters[i].has_default_value())
1860 const exprt &value=parameters[i].default_value();
1865 exprt::operandst::iterator arg_it=expr.
arguments().begin();
1866 for(
const auto ¶meter : parameters)
1868 if(parameter.get_bool(ID_C_call_by_value))
1872 if(arg_it->id()!=ID_temporary_object)
1878 arg_it->source_location(),
1882 arg_it->swap(temporary);
1897 if(statement==ID_cpp_new ||
1898 statement==ID_cpp_new_array)
1902 else if(statement==ID_cpp_delete ||
1903 statement==ID_cpp_delete_array)
1907 else if(statement==ID_preincrement ||
1908 statement==ID_predecrement ||
1909 statement==ID_postincrement ||
1910 statement==ID_postdecrement)
1914 else if(statement==ID_throw)
1918 else if(statement==ID_temporary_object)
1948 const irept &template_type = tag_symbol.
type.
find(ID_C_template);
1949 const irept &template_args = tag_symbol.
type.
find(ID_C_template_arguments);
1955 std::cout <<
"MAP for " << symbol <<
":\n";
1973 assert(this_type.
id()==ID_pointer);
1974 this_type.
set(ID_C_reference,
true);
1975 this_type.
set(ID_C_this,
true);
1986 expr.
arguments().front().type().remove(ID_C_reference);
2000 symbol.
value.
id() == ID_cpp_not_typechecked &&
2012 error() <<
"assignment side effect expected to have two operands"
2026 if(type0.
id() == ID_struct_tag)
2033 expr.
set(ID_C_lvalue,
true);
2040 std::string strop=
"operator";
2044 if(statement==ID_assign)
2046 else if(statement==ID_assign_shl)
2048 else if(statement==ID_assign_shr)
2050 else if(statement==ID_assign_plus)
2052 else if(statement==ID_assign_minus)
2054 else if(statement==ID_assign_mult)
2056 else if(statement==ID_assign_div)
2058 else if(statement==ID_assign_bitand)
2060 else if(statement==ID_assign_bitor)
2062 else if(statement==ID_assign_bitxor)
2067 error() <<
"bad assignment operator '" << statement <<
"'" <<
eom;
2074 exprt member(ID_member);
2075 member.
set(ID_component_cpp_name, cpp_name);
2096 <<
" expected to have one operand" <<
eom;
2104 const typet &tmp_type = op.type();
2107 tmp_type.
id()==ID_pointer)
2116 std::string str_op=
"operator";
2119 if(expr.
get(ID_statement)==ID_preincrement)
2121 else if(expr.
get(ID_statement)==ID_predecrement)
2123 else if(expr.
get(ID_statement)==ID_postincrement)
2128 else if(expr.
get(ID_statement)==ID_postdecrement)
2143 exprt member(ID_member);
2144 member.
set(ID_component_cpp_name, cpp_name);
2156 expr.
swap(new_expr);
2164 error() <<
"unary operator * expects one operand" <<
eom;
2174 error() <<
"pointer-to-member must use "
2175 <<
"the .* or ->* operators" <<
eom;
2190 if(op1.type().id() != ID_pointer || op1.type().find(ID_to_member).is_nil())
2193 error() <<
"pointer-to-member expected" <<
eom;
2197 typet t0 = op0.type().
id() == ID_pointer
2201 typet t1((
const typet &)op1.type().find(ID_to_member));
2206 if(t0.
id()!=ID_struct)
2209 error() <<
"pointer-to-member type error" <<
eom;
2219 error() <<
"pointer-to-member type error" <<
eom;
2225 if(op0.type().id() != ID_pointer)
2227 if(op0.id() == ID_dereference)
2234 op0.get_bool(ID_C_lvalue),
2235 "pointer-to-member must have lvalue operand");
2241 tmp.
type().
set(ID_C_bound, op0);
2248 if(expr.
id()==ID_symbol)
2251 symbol_tablet::symbolst::const_iterator it=
2256 if(it->second.value.id() == ID_cpp_not_typechecked)
2265 bool override_constantness = expr.
get_bool(ID_C_override_constantness);
2272 if(expr.
id()==ID_cpp_name)
2280 if(override_constantness)
2281 expr.
type().
set(ID_C_constant,
false);
2294 if(expr.
id()!=
"explicit-typecast")
2302 expr.
type().
id() == ID_cpp_name &&
2304 (op0_id == ID_unary_plus || op0_id == ID_unary_minus ||
2305 op0_id == ID_address_of || op0_id == ID_dereference))
2307 exprt resolve_result=
2313 if(resolve_result.
id()!=ID_type)
2317 exprt new_binary_expr;
2319 new_binary_expr.
operands().resize(2);
2325 if(op0_id==ID_unary_plus)
2326 new_binary_expr.
id(ID_plus);
2327 else if(op0_id==ID_unary_minus)
2328 new_binary_expr.
id(ID_minus);
2329 else if(op0_id==ID_address_of)
2330 new_binary_expr.
id(ID_bitand);
2331 else if(op0_id==ID_dereference)
2332 new_binary_expr.
id(ID_mult);
2336 expr.
swap(new_binary_expr);
2346 error() <<
"operator '" << expr.
id() <<
"' expects two operands" <<
eom;
2366 error() <<
"comma operator expects two operands" <<
eom;
2372 if(op0_type.id() == ID_struct || op0_type.id() == ID_struct_tag)
virtual void do_initializer(exprt &initializer, const typet &type, bool force_constant)
virtual void read(const typet &src) override
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
#define UNREACHABLE
This should be used to mark dead code.
const componentst & components() const
virtual void typecheck_expr_side_effect(side_effect_exprt &expr)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
irep_idt class_identifier
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
void typecheck_expr_side_effect(side_effect_exprt &) override
void elaborate_class_template(const typet &type)
elaborate class template instances
void typecheck_expr_dereference(exprt &) override
bool is_number(const typet &type)
Returns true if the type is a rational, real, integer, natural, complex, unsignedbv,...
void typecheck_expr_trinary(if_exprt &) override
void convert_pmop(exprt &expr)
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
void typecheck_expr_explicit_constructor_call(exprt &)
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
void typecheck_expr_cpp_name(exprt &, const cpp_typecheck_fargst &)
void typecheck_expr_typecast(exprt &) override
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
virtual exprt do_special_functions(side_effect_expr_function_callt &expr)
The type of an expression, extends irept.
std::vector< parametert > parameterst
bool operator_is_overloaded(exprt &)
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const class_typet & to_class_type(const typet &type)
Cast a typet to a class_typet.
bool reinterpret_typecast(const exprt &expr, const typet &type, exprt &new_expr, bool check_constantness=true)
const irept & find(const irep_idt &name) const
Base type for structs and unions.
typet type
Type of symbol.
Operator to dereference a pointer.
void typecheck_side_effect_assignment(side_effect_exprt &) override
A side_effect_exprt representation of a function call side effect.
The trinary if-then-else operator.
bool has_base(const irep_idt &id) const
Test whether id is a base class/struct.
exprt::operandst operands
virtual void typecheck_function_call_arguments(side_effect_expr_function_callt &expr)
Typecheck the parameters in a function call expression, and where necessary, make implicit casts arou...
void new_temporary(const source_locationt &source_location, const typet &, const exprt::operandst &ops, exprt &temporary)
bool standard_conversion_lvalue_to_rvalue(const exprt &expr, exprt &new_expr) const
Lvalue-to-rvalue conversion.
void typecheck_expr_member(exprt &) override
Base class for all expressions.
bool is_destructor() const
std::vector< componentt > componentst
optionalt< codet > cpp_constructor(const source_locationt &source_location, const exprt &object, const exprt::operandst &operands)
A struct tag type, i.e., struct_typet with an identifier.
virtual void typecheck_expr_address_of(exprt &expr)
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
void typecheck_side_effect_inc_dec(side_effect_exprt &)
bool overloadable(const exprt &)
void zero_initializer(const exprt &object, const typet &type, const source_locationt &source_location, exprt::operandst &ops)
virtual void typecheck_expr_binary_arithmetic(exprt &expr)
struct configt::ansi_ct ansi_c
virtual bool is_subset_of(const qualifierst &other) const override
static exprt collect_comma_expression(const exprt &src)
void typecheck_expr_delete(exprt &)
bool standard_conversion_array_to_pointer(const exprt &expr, exprt &new_expr) const
Array-to-pointer conversion.
void typecheck_expr_function_identifier(exprt &) override
const irep_idt & get(const irep_idt &name) const
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
virtual void typecheck_expr_operands(exprt &expr)
const exprt & size() const
bool cpp_is_pod(const typet &type) const
typet & type()
Return the type of the expression.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
void typecheck_type(typet &) override
void typecheck_expr_sizeof(exprt &) override
void typecheck_function_expr(exprt &, const cpp_typecheck_fargst &)
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
virtual void typecheck_expr_rel(binary_relation_exprt &expr)
void typecheck_side_effect_function_call(side_effect_expr_function_callt &) override
signedbv_typet signed_int_type()
void add_method_body(symbolt *_method_symbol)
static void make_already_typechecked(exprt &expr)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
irept cpp_exception_list(const typet &src, const namespacet &ns)
turns a type into a list of relevant exception IDs
void add_implicit_dereference(exprt &)
cpp_scopet & current_scope()
const exprt & compound() const
source_locationt source_location
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
virtual void typecheck_expr_function_identifier(exprt &expr)
#define forall_operands(it, expr)
void print(std::ostream &out) const
std::string type2cpp(const typet &type, const namespacet &ns)
void set(const irep_idt &name, const irep_idt &value)
virtual void typecheck_expr_dereference(exprt &expr)
#define PRECONDITION(CONDITION)
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
symbol_exprt cpp_symbol_expr(const symbolt &symbol)
void typecheck_expr_explicit_typecast(exprt &)
void typecheck_expr_rel(binary_relation_exprt &) override
void typecheck_function_call_arguments(side_effect_expr_function_callt &) override
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const std::string & get_string(const irep_idt &name) const
const basest & bases() const
Get the collection of base classes/structs.
virtual optionalt< symbol_exprt > typecheck_gcc_polymorphic_builtin(const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location)
symbol_tablet & symbol_table
pointer_typet pointer_type(const typet &subtype)
const reference_typet & to_reference_type(const typet &type)
Cast a typet to a reference_typet.
void typecheck_cast_expr(exprt &)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
bool subtype_typecast(const struct_typet &from, const struct_typet &to) const
const irep_idt & id() const
bool standard_conversion_function_to_pointer(const exprt &expr, exprt &new_expr) const
Function-to-pointer conversion.
void add_object(const exprt &expr)
bool get_component(const source_locationt &source_location, const exprt &object, const irep_idt &component_name, exprt &member)
The Boolean constant false.
void typecheck_expr_throw(exprt &)
const parameterst & parameters() const
source_locationt & add_source_location()
virtual void typecheck_side_effect_assignment(side_effect_exprt &expr)
bool static_typecast(const exprt &expr, const typet &type, exprt &new_expr, bool check_constantness=true)
bool is_qualified() const
const irep_idt & get_statement() const
virtual void typecheck_expr(exprt &expr)
void typecheck_expr_main(exprt &) override
Called after the operands are done.
reference_typet reference_type(const typet &subtype)
void typecheck_expr(exprt &) override
void typecheck_expr_comma(exprt &) override
exprt value
Initial value of symbol.
bool is_reference(const typet &type)
Returns true if the type is a reference.
Structure type, corresponds to C style structs.
void typecheck_expr_new(exprt &)
irept & add(const irep_idt &name)
const source_locationt & source_location() const
bool const_typecast(const exprt &expr, const typet &type, exprt &new_expr)
virtual void typecheck_expr_main(exprt &expr)
void typecheck_code(codet &) override
Base class of fixed-width bit-vector types.
std::string cpp_type2name(const typet &type)
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
struct operator_entryt operators[]
const exprt & as_expr() const
exprt::operandst & arguments()
void typecheck_expr_this(exprt &)
const symbolst & symbols
Read-only field, used to look up symbols given their names.
A base class for relations, i.e., binary predicates whose two operands have the same type.
const typet & base_type() const
The type of the data what we point to.
void typecheck_expr_index(exprt &) override
void implicit_typecast(exprt &expr, const typet &type) override
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
void typecheck_expr_binary_arithmetic(exprt &) override
bool find_parent(const symbolt &symb, const irep_idt &base_name, irep_idt &identifier)
const typet & return_type() const
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
bool implicit_conversion_sequence(const exprt &expr, const typet &type, exprt &new_expr, unsigned &rank)
implicit conversion sequence
bool dynamic_typecast(const exprt &expr, const typet &type, exprt &new_expr)
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
There are a large number of kinds of tree structured or tree-like data in CPROVER.
std::string to_string(const typet &) override
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
void build(const template_typet &template_type, const cpp_template_args_tct &template_args)
void remove(const irep_idt &name)
Operator to return the address of an object.
source_locationt & add_source_location()
Semantic type conversion.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
void explicit_typecast_ambiguity(exprt &)
optionalt< codet > cpp_destructor(const source_locationt &source_location, const exprt &object)
The Boolean constant true.
exprt resolve(const cpp_namet &cpp_name, const cpp_typecheck_resolvet::wantt want, const cpp_typecheck_fargst &fargs, bool fail_with_exception=true)
template_mapt template_map
void typecheck_method_application(side_effect_expr_function_callt &)
virtual void typecheck_expr_sizeof(exprt &expr)
bitvector_typet c_index_type()
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
void typecheck_expr_address_of(exprt &) override
const source_locationt & source_location() const
bool is_incomplete() const
A struct/union may be incomplete.
irep_idt name
The unique identifier.
cpp_scopet & set_scope(const irep_idt &identifier)
bool get_bool(const irep_idt &name) const
An expression containing a side effect.
void typecheck_expr_ptrmember(exprt &) override
virtual void typecheck_expr_index(exprt &expr)
cpp_namet & to_cpp_name(irept &cpp_name)
codet representation of an expression statement.
const typet & element_type() const
The type of the elements of the array.
virtual void typecheck_expr_comma(exprt &expr)