41 const irep_idt &
id =
b.type().get_identifier();
42 if(
lookup(
id).base_name == base_name)
57 else if(expr.
id()==
"cpp-this")
67 else if(expr.
id()==
"explicit-typecast")
69 else if(expr.
id()==
"explicit-constructor-call")
74 std::cerr <<
"E: " << expr.
pretty() <<
'\n';
75 std::cerr <<
"cpp_typecheckt::typecheck_expr_main got code\n";
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")
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;
221 error() <<
"error: bad types for operands" <<
eom;
274 error() <<
"error: types are incompatible.\n"
374 std::string op_name=
"operator->";
382 {to_unary_expr(expr).op()},
408 typet t = it->type();
471 if(expr.
id()==
"explicit-typecast")
477 std::string op_name=std::string(
"operator")+
"("+
cpp_type2name(t)+
")";
514 for(exprt::operandst::const_iterator
516 it!=(expr).operands().end();
518 function_call.
arguments().push_back(*it);
532 expr.
swap(function_call);
545 std::string op_name=std::string(
"operator")+e->op_name;
577 fargs.has_object=
true;
603 for(exprt::operandst::const_iterator
607 function_call.
arguments().push_back(*it);
622 fargs.has_object=
false;
640 function_call.
arguments().push_back(*it);
669 error() <<
"address_of expects one operand" <<
eom;
678 error() <<
"expr not an lvalue" <<
eom;
698 if(!args.empty() && args.front().get_this())
707 error() <<
"error: pointers to virtual methods"
708 <<
" are currently not implemented" <<
eom;
742 error() <<
"cannot throw void" <<
eom;
800 if(!initializer.
operands().empty() &&
805 error() <<
"new with array type must not use initializer" <<
eom;
894 static_cast<const exprt &
>(
static_cast<const irept &
>(expr.
type())),
921 tmp.add_to_operands(std::move(op));
940 error() <<
"invalid explicit cast:\n"
941 <<
"operand type: '" <<
to_string(op.type()) <<
"'\n"
949 error() <<
"explicit typecast expects 0 or 1 operands" <<
eom;
960 expr.
id(
"explicit-typecast");
980 error() <<
"`this' is not allowed here" <<
eom;
999 error() <<
"delete expects one operand" <<
eom;
1019 error() <<
"delete takes a pointer type operand, but got '"
1055 std::cout <<
"E: " << expr.pretty() <<
'\n';
1067 error() <<
"error: member operator expects one operand" <<
eom;
1099 error() <<
"error: member operator requires struct/union type "
1111 error() <<
"error: member operator got incomplete type "
1112 <<
"on left hand side" <<
eom;
1158 error() <<
"error: member '"
1160 <<
"' is a constructor" <<
eom;
1173 <<
"' is not static member "
1195 INVARIANT(!component_name.
empty(),
"component name should not be empty");
1214 error() <<
"error: member '" << component_name <<
"' of '"
1224 symbol_tablet::symbolst::const_iterator it=
1244 error() <<
"error: ptrmember operator expects one operand" <<
eom;
1255 error() <<
"error: ptrmember operator requires pointer type "
1256 <<
"on left hand side, but got '" <<
to_string(op.type()) <<
"'"
1265 op.add_to_operands(std::move(
tmp));
1281 error() <<
"cast expressions expect one operand" <<
eom;
1293 if(
f_op.get_sub().size()!=2 ||
1297 error() <<
id <<
" expects template argument" <<
eom;
1306 error() <<
id <<
" expects one template argument" <<
eom;
1315 error() <<
id <<
" expects a type as template argument" <<
eom;
1332 error() <<
"type mismatch on const_cast:\n"
1343 error() <<
"type mismatch on dynamic_cast:\n"
1354 error() <<
"type mismatch on reinterpret_cast:\n"
1365 error() <<
"type mismatch on static_cast:\n"
1384 if(expr.
get_sub().size()==1 &&
1391 identifier,
fargs.operands, source_location))
1398 for(std::size_t
i=0;
i<expr.
get_sub().size();
i++)
1415 if(expr.
get_sub().size()>=1 &&
1452 error() <<
"object missing" <<
eom;
1462 ptrmem.operands().push_back(
1467 ptrmem.add_source_location()=source_location;
1503 bool is_qualified=
false;
1512 is_qualified=
cpp_name.is_qualified();
1518 is_qualified=
cpp_name.is_qualified();
1539 exprt typecast(
"explicit-typecast");
1545 expr.
swap(typecast);
1550 error() <<
"zero or one argument expected" <<
eom;
1586 error() <<
"pointer-to-member not bound" <<
eom;
1616 error() <<
"expecting code as argument" <<
eom;
1633 exprt this_expr(
"cpp-this");
1704 error() <<
"function call expects function or function "
1705 <<
"pointer as argument, but got '"
1720 assert(parameters.size()>=1);
1760 for(
const auto &
c : components)
1762 const typet &type =
c.type();
1799 !parameters.empty() && parameters.front().get_this() &&
1807 "`this' parameter should be a pointer");
1814 tmp.add_source_location()=
operand.source_location();
1830 if(
tmp.is_not_nil())
1844 if(parameters.size()>expr.
arguments().size())
1848 for(;
i<parameters.size();
i++)
1850 if(!parameters[
i].has_default_value())
1853 const exprt &value=parameters[
i].default_value();
1871 arg_it->source_location(),
1948 std::cout <<
"MAP for " << symbol <<
":\n";
2005 error() <<
"assignment side effect expected to have two operands"
2033 std::string
strop=
"operator";
2060 error() <<
"bad assignment operator '" << statement <<
"'" <<
eom;
2089 <<
" expected to have one operand" <<
eom;
2109 std::string
str_op=
"operator";
2157 error() <<
"unary operator * expects one operand" <<
eom;
2167 error() <<
"pointer-to-member must use "
2168 <<
"the .* or ->* operators" <<
eom;
2186 error() <<
"pointer-to-member expected" <<
eom;
2200 error() <<
"pointer-to-member type error" <<
eom;
2210 error() <<
"pointer-to-member type error" <<
eom;
2226 "pointer-to-member must have lvalue operand");
2242 symbol_tablet::symbolst::const_iterator it=
2285 if(expr.
id()!=
"explicit-typecast")
2337 error() <<
"operator '" << expr.
id() <<
"' expects two operands" <<
eom;
2357 error() <<
"comma operator expects two operands" <<
eom;
reference_typet reference_type(const typet &subtype)
signedbv_typet signed_int_type()
pointer_typet pointer_type(const typet &subtype)
bitvector_typet c_index_type()
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
static void make_already_typechecked(exprt &expr)
const exprt & size() const
A base class for relations, i.e., binary predicates whose two operands have the same type.
Base class of fixed-width bit-vector types.
virtual void typecheck_expr_main(exprt &expr)
virtual void typecheck_expr_address_of(exprt &expr)
virtual void typecheck_expr(exprt &expr)
virtual void do_initializer(exprt &initializer, const typet &type, bool force_constant)
virtual void typecheck_expr_binary_arithmetic(exprt &expr)
virtual void typecheck_expr_sizeof(exprt &expr)
virtual void typecheck_expr_side_effect(side_effect_exprt &expr)
virtual void typecheck_expr_index(exprt &expr)
virtual void typecheck_expr_function_identifier(exprt &expr)
virtual void typecheck_expr_comma(exprt &expr)
symbol_tablet & symbol_table
virtual exprt do_special_functions(side_effect_expr_function_callt &expr)
virtual void typecheck_side_effect_assignment(side_effect_exprt &expr)
virtual optionalt< symbol_exprt > typecheck_gcc_polymorphic_builtin(const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location)
virtual void typecheck_expr_operands(exprt &expr)
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...
virtual void typecheck_expr_dereference(exprt &expr)
virtual void typecheck_expr_rel(binary_relation_exprt &expr)
codet representation of an expression statement.
std::vector< parametert > parameterst
const parameterst & parameters() const
const typet & return_type() const
struct configt::ansi_ct ansi_c
irep_idt class_identifier
bool is_destructor() const
const source_locationt & source_location() const
cpp_scopet & set_scope(const irep_idt &identifier)
cpp_scopet & current_scope()
bool find_parent(const symbolt &symb, const irep_idt &base_name, irep_idt &identifier)
void typecheck_expr_typecast(exprt &) override
void typecheck_side_effect_assignment(side_effect_exprt &) override
bool implicit_conversion_sequence(const exprt &expr, const typet &type, exprt &new_expr, unsigned &rank)
implicit conversion sequence
optionalt< codet > cpp_destructor(const source_locationt &source_location, const exprt &object)
void typecheck_type(typet &) override
void explicit_typecast_ambiguity(exprt &)
template_mapt template_map
bool reinterpret_typecast(const exprt &expr, const typet &type, exprt &new_expr, bool check_constantness=true)
void convert_pmop(exprt &expr)
void typecheck_expr_sizeof(exprt &) override
void typecheck_code(codet &) override
void typecheck_expr_explicit_typecast(exprt &)
void implicit_typecast(exprt &expr, const typet &type) override
void typecheck_cast_expr(exprt &)
void typecheck_expr_dereference(exprt &) override
void typecheck_side_effect_function_call(side_effect_expr_function_callt &) override
bool cpp_is_pod(const typet &type) const
bool get_component(const source_locationt &source_location, const exprt &object, const irep_idt &component_name, exprt &member)
bool const_typecast(const exprt &expr, const typet &type, exprt &new_expr)
void new_temporary(const source_locationt &source_location, const typet &, const exprt::operandst &ops, exprt &temporary)
void typecheck_expr_trinary(if_exprt &) override
void typecheck_expr_rel(binary_relation_exprt &) override
bool standard_conversion_function_to_pointer(const exprt &expr, exprt &new_expr) const
Function-to-pointer conversion.
bool standard_conversion_array_to_pointer(const exprt &expr, exprt &new_expr) const
Array-to-pointer conversion.
bool dynamic_typecast(const exprt &expr, const typet &type, exprt &new_expr)
void add_method_body(symbolt *_method_symbol)
void typecheck_expr_binary_arithmetic(exprt &) override
void typecheck_expr_delete(exprt &)
optionalt< codet > cpp_constructor(const source_locationt &source_location, const exprt &object, const exprt::operandst &operands)
void typecheck_expr_main(exprt &) override
Called after the operands are done.
void elaborate_class_template(const typet &type)
elaborate class template instances
bool operator_is_overloaded(exprt &)
bool standard_conversion_lvalue_to_rvalue(const exprt &expr, exprt &new_expr) const
Lvalue-to-rvalue conversion.
void typecheck_expr_new(exprt &)
void add_implicit_dereference(exprt &)
void typecheck_expr_cpp_name(exprt &, const cpp_typecheck_fargst &)
void typecheck_expr(exprt &) override
void typecheck_expr_side_effect(side_effect_exprt &) override
void typecheck_expr_comma(exprt &) override
bool static_typecast(const exprt &expr, const typet &type, exprt &new_expr, bool check_constantness=true)
bool subtype_typecast(const struct_typet &from, const struct_typet &to) const
void typecheck_expr_explicit_constructor_call(exprt &)
void typecheck_function_expr(exprt &, const cpp_typecheck_fargst &)
void typecheck_method_application(side_effect_expr_function_callt &)
std::string to_string(const typet &) override
void typecheck_expr_this(exprt &)
void typecheck_expr_throw(exprt &)
bool overloadable(const exprt &)
void typecheck_expr_index(exprt &) override
void typecheck_side_effect_inc_dec(side_effect_exprt &)
void zero_initializer(const exprt &object, const typet &type, const source_locationt &source_location, exprt::operandst &ops)
void typecheck_function_call_arguments(side_effect_expr_function_callt &) override
void typecheck_expr_ptrmember(exprt &) override
exprt resolve(const cpp_namet &cpp_name, const cpp_typecheck_resolvet::wantt want, const cpp_typecheck_fargst &fargs, bool fail_with_exception=true)
void typecheck_expr_address_of(exprt &) override
void typecheck_expr_function_identifier(exprt &) override
void typecheck_expr_member(exprt &) override
Operator to dereference a pointer.
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.
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.
The Boolean constant false.
The trinary if-then-else operator.
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
irept & add(const irep_idt &name)
const std::string & get_string(const irep_idt &name) const
const exprt & compound() const
source_locationt source_location
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().
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
A side_effect_exprt representation of a function call side effect.
exprt::operandst & arguments()
An expression containing a side effect.
const irep_idt & get_statement() const
A struct tag type, i.e., struct_typet with an identifier.
Structure type, corresponds to C style structs.
const basest & bases() const
Get the collection of base classes/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 is_incomplete() const
A struct/union may be incomplete.
std::vector< componentt > componentst
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.
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 print(std::ostream &out) const
The Boolean constant true.
Semantic type conversion.
The type of an expression, extends irept.
const typet & subtype() const
source_locationt & add_source_location()
irept cpp_exception_list(const typet &src, const namespacet &ns)
turns a type into a list of relevant exception IDs
C++ Language Type Checking.
cpp_namet & to_cpp_name(irept &cpp_name)
std::string cpp_type2name(const typet &type)
C++ Language Type Checking.
static exprt collect_comma_expression(const exprt &src)
struct operator_entryt operators[]
C++ Language Type Checking.
symbol_exprt cpp_symbol_expr(const symbolt &symbol)
std::string type2cpp(const typet &type, const namespacet &ns)
#define forall_operands(it, expr)
Expression Initialization.
bool is_number(const typet &type)
Returns true if the type is a rational, real, integer, natural, complex, unsignedbv,...
API to expression classes for Pointers.
bool is_reference(const typet &type)
Returns true if the type is a reference.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
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)
#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'.
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
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 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.
const class_typet & to_class_type(const typet &type)
Cast a typet to a class_typet.