Go to the documentation of this file.
36 error() <<
"expected type as initializer for '" << symbol.
base_name <<
"'"
54 <<
"' is declared as reference but is not initialized" <<
eom;
81 symbol.
value.
id() == ID_address_of &&
93 for(
const auto ¶meter : code_type.
parameters())
95 exprt new_object(ID_new_object, parameter.type());
96 new_object.
set(ID_C_lvalue,
true);
98 if(parameter.get_this())
104 fargs.
operands.push_back(new_object);
115 if(resolved_expr.
id()==ID_symbol)
120 else if(resolved_expr.
id()==ID_member)
148 if(symbol.
value.
id()==ID_initializer_list ||
149 symbol.
value.
id()==ID_string_constant)
180 ops.push_back(symbol.
value);
185 if(constructor.has_value())
186 symbol.
value = constructor.value();
200 if(final_type.
id()==ID_struct)
204 if(struct_type.is_incomplete())
207 error() <<
"cannot zero-initialize incomplete struct" <<
eom;
211 for(
const auto &
component : struct_type.components())
228 else if(final_type.
id()==ID_array &&
232 const exprt &size_expr=array_type.
size();
234 if(size_expr.
id()==ID_infinity)
249 else if(final_type.
id()==ID_union)
253 if(union_type.is_incomplete())
256 error() <<
"cannot zero-initialize incomplete union" <<
eom;
265 for(
const auto &
component : union_type.components())
274 const auto size_int =
275 numeric_cast<mp_integer>(component_size_opt.value_or(
nil_exprt()));
276 if(size_int.has_value())
278 if(*size_int > max_comp_size)
280 max_comp_size = *size_int;
290 exprt member(ID_member);
292 member.
set(ID_component_cpp_name, cpp_name);
296 else if(final_type.
id()==ID_c_enum)
311 assign.
lhs().
type().
set(ID_C_constant,
false);
315 ops.push_back(assign);
320 if(!value.has_value())
323 error() <<
"cannot zero-initialize '" <<
to_string(final_type) <<
"'"
332 assign.
lhs().
type().
set(ID_C_constant,
false);
336 ops.push_back(assign);
virtual void do_initializer(exprt &initializer, const typet &type, bool force_constant)
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 union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
static exprt conditional_cast(const exprt &expr, const typet &type)
const typet & subtype() const
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
#define CHECK_RETURN(CONDITION)
The type of an expression, extends irept.
C++ Language Type Checking.
typet type
Type of symbol.
irept & add(const irep_namet &name)
exprt::operandst operands
const irept & find(const irep_namet &name) const
const symbolt & lookup(const irep_idt &name) const
Lookup a symbol in the namespace.
Base class for all expressions.
optionalt< codet > cpp_constructor(const source_locationt &source_location, const exprt &object, const exprt::operandst &operands)
irep_idt base_name
Base (non-scoped) name.
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
void zero_initializer(const exprt &object, const typet &type, const source_locationt &source_location, exprt::operandst &ops)
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Expression to hold a symbol (variable)
bitvector_typet index_type()
Fixed-width bit-vector with unsigned binary interpretation.
const exprt & size() const
bool cpp_is_pod(const typet &type) const
typet & type()
Return the type of the expression.
void typecheck_type(typet &) override
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Expression Initialization.
static void make_already_typechecked(exprt &expr)
void convert_initializer(symbolt &symbol)
Initialize an object with a value.
const exprt & compound() const
source_locationt source_location
void reference_initializer(exprt &expr, const typet &type)
A reference to type "cv1 T1" is initialized by an expression of type "cv2 T2" as follows:
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
API to expression classes for Pointers.
bool simplify(exprt &expr, const namespacet &ns)
const irep_idt & id() const
std::vector< exprt > operandst
const parameterst & parameters() const
C++ Language Type Checking.
std::size_t get_width() const
Extract member of struct or union.
void typecheck_expr(exprt &) override
exprt value
Initial value of symbol.
message_handlert & get_message_handler()
bool is_reference(const typet &type)
Returns true if the type is a reference.
void typecheck_code(codet &) override
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
const irep_idt & get(const irep_namet &name) const
source_locationt location
Source code location of definition of symbol.
void set(const irep_namet &name, const irep_idt &value)
static bool has_auto(const typet &type)
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 cpp_convert_auto(typet &dest, const typet &src, message_handlert &message_handler)
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
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.
Operator to return the address of an object.
source_locationt & add_source_location()
const irep_idt & get_base_name() const
A codet representing an assignment in the program.
exprt resolve(const cpp_namet &cpp_name, const cpp_typecheck_resolvet::wantt want, const cpp_typecheck_fargst &fargs, bool fail_with_exception=true)
const source_locationt & source_location() const
irep_idt name
The unique identifier.
cpp_namet & to_cpp_name(irept &cpp_name)
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.