38 "any array must have a size");
69 <<
"' is still incomplete -- cannot initialize" <<
eom;
103 error() <<
"array size needs to be constant, got "
111 error() <<
"array size must not be negative" <<
eom;
127 if(!zero.has_value())
130 error() <<
"cannot zero-initialize array with subtype '"
165 error() <<
"array size needs to be constant, got "
173 error() <<
"array size must not be negative" <<
eom;
191 if(!zero.has_value())
194 error() <<
"cannot zero-initialize array with subtype '"
211 <<
"' cannot be initialized with '" <<
to_string(value) <<
"'"
220 <<
"' cannot be initialized with designated initializer" <<
eom;
293 if(
c.type().id() !=
ID_code && !
c.get_is_padding())
334 error() <<
"array has non-constant size '"
349 if(!vector_size.has_value())
352 error() <<
"vector has non-constant size '"
370 exprt::operandst::const_iterator
init_it,
399 for(
size_t i=0;
i<designator.
size();
i++)
401 size_t index=designator[
i].index;
402 const typet &type=designator[
i].type;
418 error() <<
"cannot zero-initialize array with element type '"
428 if(index>=
dest->operands().size())
439 if(!zero.has_value())
442 error() <<
"cannot zero-initialize array with element type '"
447 dest->operands().resize(
455 error() <<
"array index designator " << index
456 <<
" out of bounds (" <<
dest->operands().size()
469 if(index>=
dest->operands().size())
472 error() <<
"structure member designator " << index
473 <<
" out of bounds (" <<
dest->operands().size()
479 "member designator is bounded by components size");
481 !components[index].get_is_padding(),
482 "member designator points at data member");
493 if(components.empty())
496 error() <<
"union member designator found for empty union" <<
eom;
504 error() <<
"too many initializers" <<
eom;
510 warning() <<
"excess elements in union initializer" <<
eom;
515 else if(index >= components.size())
518 error() <<
"union member designator " << index <<
" out of bounds ("
519 << components.size() <<
")" <<
eom;
543 if(!zero.has_value())
546 error() <<
"cannot zero-initialize union component of type '"
623 if(!components.empty())
630 if(!zero.has_value())
633 error() <<
"cannot zero-initialize union component of type '"
690 if(
dest->operands().empty())
694 <<
" requires initializer list, found " << value.
id()
695 <<
" instead" <<
eom;
757 (components[entry.
index].get_is_padding() ||
758 (components[entry.
index].get_anonymous() &&
773 if(designator.
size()==1)
803 error() <<
"expected array index designator" <<
eom;
815 error() <<
"expected constant array index designator" <<
eom;
828 error() <<
"expected constant array size" <<
eom;
845 error() <<
"expected member designator" <<
eom;
869 std::size_t number = 0;
873 for(
const auto &
c : components)
875 if(
c.get_name() == component_name)
879 entry.
size=components.size();
890 entry.
size=components.size();
907 error() <<
"failed to find struct component '" << component_name
917 error() <<
"designated initializers cannot initialize '"
953 warning() <<
"ignoring excess initializers" <<
eom;
967 if(!zero.has_value())
970 error() <<
"cannot zero-initialize '" <<
to_string(full_type) <<
"'"
988 if(!zero.has_value())
991 error() <<
"cannot zero-initialize '" <<
to_string(full_type) <<
"'"
1009 <<
"' with an initializer list" <<
eom;
1018 for(exprt::operandst::const_iterator it=operands.begin();
1019 it!=operands.end(); )
1039 size_t size=
result.operands().size();
bool has_component_rec(const typet &type, const irep_idt &component_name, const namespacet &ns)
C Language Type Checking.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Expression classes for byte-level operators.
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
ANSI-C Language Type Checking.
bitvector_typet char_type()
bitvector_typet c_index_type()
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Array constructor from list of elements.
const exprt & size() const
const typet & element_type() const
The type of the elements of the array.
std::size_t get_width() const
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
virtual exprt do_initializer_list(const exprt &value, const typet &type, bool force_constant)
virtual void implicit_typecast(exprt &expr, const typet &type)
virtual exprt do_initializer_rec(const exprt &value, const typet &type, bool force_constant)
initialize something of type ‘type’ with given value ‘value’
virtual void typecheck_expr(exprt &expr)
virtual void do_initializer(exprt &initializer, const typet &type, bool force_constant)
virtual void make_constant(exprt &expr)
virtual std::string to_string(const exprt &expr)
void increment_designator(designatort &designator)
virtual exprt::operandst::const_iterator do_designated_initializer(exprt &result, designatort &designator, const exprt &initializer_list, exprt::operandst::const_iterator init_it, bool force_constant)
virtual void make_constant_index(exprt &expr)
designatort make_designator(const typet &type, const exprt &src)
void designator_enter(const typet &type, designatort &designator)
struct configt::ansi_ct ansi_c
const entryt & front() const
void push_entry(const entryt &entry)
const entryt & back() const
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).
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
bool get_bool(const irep_idt &name) const
const irept & find(const irep_idt &name) const
const irep_idt & id() const
source_locationt source_location
mstreamt & warning() const
mstreamt & result() const
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Structure type, corresponds to C style structs.
Base type for structs and unions.
const componentst & components() const
std::vector< componentt > componentst
typet type
Type of symbol.
irep_idt name
The unique identifier.
exprt value
Initial value of symbol.
The type of an expression, extends irept.
Union constructor from single element.
irep_idt get_component_name() const
bool has_prefix(const std::string &s, const std::string &prefix)
#define forall_operands(it, expr)
#define Forall_operands(it, expr)
optionalt< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
Expression Initialization.
const std::string & id2string(const irep_idt &d)
#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 array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_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 union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_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 string_constantt & to_string_constant(const exprt &expr)
const type_with_subtypet & to_type_with_subtype(const typet &type)
byte_update_exprt make_byte_update(const exprt &_op, const exprt &_offset, const exprt &_value)
Construct a byte_update_exprt with endianness and byte width matching the current configuration.