36 error() <<
"expected type as initializer for '" << symbol.
base_name <<
"'"
54 <<
"' is declared as reference but is not initialized" <<
eom;
102 fargs.has_object =
true;
117 "symbol type must match");
189 if(constructor.has_value())
190 symbol.
value = constructor.value();
209 error() <<
"cannot zero-initialize incomplete struct" <<
eom;
258 error() <<
"cannot zero-initialize incomplete union" <<
eom;
318 ops.push_back(assign);
323 if(!value.has_value())
338 ops.push_back(assign);
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
bitvector_typet c_index_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.
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)
virtual void do_initializer(exprt &initializer, const typet &type, bool force_constant)
A codet representing an assignment in the program.
void typecheck_type(typet &) override
void typecheck_code(codet &) override
void implicit_typecast(exprt &expr, const typet &type) override
bool cpp_is_pod(const typet &type) const
void convert_initializer(symbolt &symbol)
Initialize an object with a value.
std::optional< codet > cpp_constructor(const source_locationt &source_location, const exprt &object, const exprt::operandst &operands)
static bool has_auto(const typet &type)
void typecheck_expr(exprt &) override
std::string to_string(const typet &) override
void zero_initializer(const exprt &object, const typet &type, const source_locationt &source_location, exprt::operandst &ops)
exprt resolve(const cpp_namet &cpp_name, const cpp_typecheck_resolvet::wantt want, const cpp_typecheck_fargst &fargs, bool fail_with_exception=true)
void reference_initializer(exprt &expr, const reference_typet &type)
A reference to type "cv1 T1" is initialized by an expression of type "cv2 T2" as follows:
Base class for all expressions.
std::vector< exprt > operandst
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()
There are a large number of kinds of tree structured or tree-like data in CPROVER.
const irept & find(const irep_idt &name) const
void set(const irep_idt &name, const irep_idt &value)
const irep_idt & id() const
irept & add(const irep_idt &name)
Extract member of struct or union.
source_locationt source_location
message_handlert & get_message_handler()
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().
Expression to hold a symbol (variable)
source_locationt location
Source code location of definition of symbol.
typet type
Type of symbol.
irep_idt name
The unique identifier.
irep_idt irep_idt base_name
Name of module the symbol belongs to.
exprt value
Initial value of symbol.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
Fixed-width bit-vector with unsigned binary interpretation.
void cpp_convert_auto(typet &dest, const typet &src, message_handlert &message_handler)
cpp_namet & to_cpp_name(irept &cpp_name)
C++ Language Type Checking.
C++ Language Type Checking.
Expression Initialization.
API to expression classes for Pointers.
bool is_reference(const typet &type)
Returns true if the type is a reference.
const reference_typet & to_reference_type(const typet &type)
Cast a typet to a reference_typet.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
std::optional< exprt > size_of_expr(const typet &type, const namespacet &ns)
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,...
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_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.