39 "any array must have a size");
70 <<
"' is still incomplete -- cannot initialize" <<
eom;
104 error() <<
"array size needs to be constant, got "
112 error() <<
"array size must not be negative" <<
eom;
128 if(!zero.has_value())
131 error() <<
"cannot zero-initialize array with subtype '"
167 error() <<
"array size needs to be constant, got "
175 error() <<
"array size must not be negative" <<
eom;
193 if(!zero.has_value())
196 error() <<
"cannot zero-initialize array with subtype '"
213 <<
"' cannot be initialized with '" <<
to_string(value) <<
"'"
222 <<
"' cannot be initialized with designated initializer" <<
eom;
277 c.type().id() !=
ID_code,
"struct member must not be of code type");
280 !
c.get_is_padding() &&
322 error() <<
"array has non-constant size '"
337 if(!vector_size.has_value())
340 error() <<
"vector has non-constant size '"
358 exprt::operandst::const_iterator
init_it,
372 designator.
front().type,
387 for(
size_t i=0; i<designator.
size(); i++)
389 size_t index=designator[i].index;
390 const typet &type=designator[i].type;
406 error() <<
"cannot zero-initialize array with element type '"
428 if(!zero.has_value())
431 error() <<
"cannot zero-initialize array with element type '"
441 error() <<
"array index designator " << index
442 <<
" out of bounds (" << dest->
operands().size()
458 error() <<
"structure member designator " << index
459 <<
" out of bounds (" << dest->
operands().size()
465 "member designator is bounded by components size");
467 components[index].type().
id() !=
ID_code,
468 "struct member must not be of code type");
470 !components[index].get_is_padding(),
471 "member designator points at non-padding member");
482 if(components.empty())
485 error() <<
"union member designator found for empty union" <<
eom;
493 error() <<
"too many initializers" <<
eom;
499 warning() <<
"excess elements in union initializer" <<
eom;
504 else if(index >= components.size())
507 error() <<
"union member designator " << index <<
" out of bounds ("
508 << components.size() <<
")" <<
eom;
532 if(!zero.has_value())
535 error() <<
"cannot zero-initialize union component of type '"
577 const typet &type=designator.
back().subtype;
612 if(!components.empty())
619 if(!zero.has_value())
622 error() <<
"cannot zero-initialize union component of type '"
669 "full type must be composite");
674 const bool vla_permitted=designator.
back().vla_permitted;
683 <<
" requires initializer list, found " << value.
id()
684 <<
" instead" <<
eom;
742 components.size() == entry.
size,
"matching component numbers");
747 (components[entry.
index].get_is_padding() ||
748 (components[entry.
index].get_anonymous() &&
761 if(designator.
size()==1)
767 INVARIANT(!designator.
empty(),
"designator had more than one entry");
790 error() <<
"expected array index designator" <<
eom;
802 error() <<
"expected constant array index designator" <<
eom;
815 error() <<
"expected constant array size" <<
eom;
832 error() <<
"expected member designator" <<
eom;
851 bool found=
false, repeat;
857 std::size_t number = 0;
861 for(
const auto &
c : components)
863 if(
c.get_name() == component_name)
867 entry.
size=components.size();
881 entry.
size=components.size();
898 error() <<
"failed to find struct component '" << component_name
908 error() <<
"designated initializers cannot initialize '"
944 warning() <<
"ignoring excess initializers" <<
eom;
958 if(!zero.has_value())
961 error() <<
"cannot zero-initialize '" <<
to_string(full_type) <<
"'"
979 if(!zero.has_value())
982 error() <<
"cannot zero-initialize '" <<
to_string(full_type) <<
"'"
1000 <<
"' with an initializer list" <<
eom;
1009 for(exprt::operandst::const_iterator it=operands.begin();
1010 it!=operands.end(); )
1027 !components.empty() &&
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.
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.
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.
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)
symbol_table_baset & symbol_table
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)
const irep_idt const irep_idt mode
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.
A struct tag type, i.e., struct_typet with an identifier.
Structure type, corresponds to C style structs.
Base type for structs and unions.
std::vector< componentt > componentst
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
typet type
Type of symbol.
irep_idt name
The unique identifier.
exprt value
Initial value of symbol.
Symbol table entry describing a data typeThis is a symbol generated as part of type checking.
The type of an expression, extends irept.
Union constructor from single element.
bool has_prefix(const std::string &s, const std::string &prefix)
#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 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,...
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
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 array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_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)
static std::string type2name(const typet &type, const namespacet &ns, symbol_numbert &symbol_number)
const type_with_subtypet & to_type_with_subtype(const typet &type)