Go to the documentation of this file.
34 if(type.
id()==ID_array)
39 "any array must have a size");
44 result.id() != ID_compound_literal)
65 (full_type.
id() == ID_struct || full_type.
id() == ID_union) &&
70 <<
"' is still incomplete -- cannot initialize" <<
eom;
74 if(value.
id()==ID_initializer_list)
78 value.
id() == ID_array && value.
get_bool(ID_C_string_constant) &&
79 full_type.
id() == ID_array &&
80 (full_type.
subtype().
id() == ID_signedbv ||
81 full_type.
subtype().
id() == ID_unsignedbv) &&
93 if(full_type.
id()==ID_array &&
97 const auto array_size =
99 if(!array_size.has_value())
102 error() <<
"array size needs to be constant, got "
110 error() <<
"array size must not be negative" <<
eom;
117 tmp.
operands().resize(numeric_cast_v<std::size_t>(*array_size));
126 if(!zero.has_value())
129 error() <<
"cannot zero-initialize array with subtype '"
133 tmp.
operands().resize(numeric_cast_v<std::size_t>(*array_size), *zero);
141 value.
id() == ID_string_constant && full_type.
id() == ID_array &&
142 (full_type.
subtype().
id() == ID_signedbv ||
143 full_type.
subtype().
id() == ID_unsignedbv) &&
155 if(full_type.
id()==ID_array &&
159 const auto array_size =
161 if(!array_size.has_value())
164 error() <<
"array size needs to be constant, got "
172 error() <<
"array size must not be negative" <<
eom;
179 tmp2.
operands().resize(numeric_cast_v<std::size_t>(*array_size));
188 if(!zero.has_value())
191 error() <<
"cannot zero-initialize array with subtype '"
195 tmp2.
operands().resize(numeric_cast_v<std::size_t>(*array_size), *zero);
202 if(full_type.
id()==ID_array &&
207 <<
"' cannot be initialized with '" <<
to_string(value) <<
"'"
212 if(value.
id()==ID_designated_initializer)
216 <<
"' cannot be initialized with designated initializer" <<
eom;
240 symbol.
type.
id() == ID_array &&
263 symbol.
type.
id() == ID_array &&
278 if(full_type.
id()==ID_struct)
289 if(c.type().id() != ID_code && !c.get_is_padding())
298 else if(full_type.
id()==ID_union)
315 else if(full_type.
id()==ID_array)
326 const auto array_size = numeric_cast<mp_integer>(array_type.
size());
327 if(!array_size.has_value())
330 error() <<
"array has non-constant size '"
335 entry.
size = numeric_cast_v<std::size_t>(*array_size);
339 else if(full_type.
id()==ID_vector)
343 const auto vector_size = numeric_cast<mp_integer>(vector_type.
size());
345 if(!vector_size.has_value())
348 error() <<
"vector has non-constant size '"
353 entry.
size = numeric_cast_v<std::size_t>(*vector_size);
365 const exprt &initializer_list,
366 exprt::operandst::const_iterator init_it,
370 exprt value=*init_it;
372 assert(!designator.
empty());
374 if(value.
id()==ID_designated_initializer)
381 static_cast<const exprt &
>(value.
find(ID_designator)));
383 assert(!designator.
empty());
387 result, designator, value, value.
operands().begin(), force_constant);
395 for(
size_t i=0; i<designator.
size(); i++)
397 size_t index=designator[i].index;
398 const typet &type=designator[i].type;
401 if(full_type.
id()==ID_array ||
402 full_type.
id()==ID_vector)
407 if(dest->
id() == ID_array_of)
410 const auto array_size = numeric_cast<mp_integer>(array_type.
size());
411 if(!array_size.has_value())
414 error() <<
"cannot zero-initialize array with subtype '"
420 dest->
operands().resize(numeric_cast_v<std::size_t>(*array_size), zero);
425 if(full_type.
id()==ID_array &&
432 if(!zero.has_value())
435 error() <<
"cannot zero-initialize array with subtype '"
440 numeric_cast_v<std::size_t>(index) + 1, *zero);
447 error() <<
"array index designator " << index
448 <<
" out of bounds (" << dest->
operands().size()
454 dest = &(dest->
operands()[numeric_cast_v<std::size_t>(index)]);
456 else if(full_type.
id()==ID_struct)
464 error() <<
"structure member designator " << index
465 <<
" out of bounds (" << dest->
operands().size()
471 "member designator is bounded by components size");
473 !components[index].get_is_padding(),
474 "member designator points at data member");
478 else if(full_type.
id()==ID_union)
485 if(components.empty())
488 error() <<
"union member designator found for empty union" <<
eom;
491 else if(init_it != initializer_list.
operands().begin())
496 error() <<
"too many initializers" <<
eom;
502 warning() <<
"excess elements in union initializer" <<
eom;
507 else if(index >= components.size())
510 error() <<
"union member designator " << index <<
" out of bounds ("
511 << components.size() <<
")" <<
eom;
518 dest->
id() == ID_union &&
525 else if(dest->
id() == ID_union)
535 if(!zero.has_value())
538 error() <<
"cannot zero-initialize union component of type '"
548 *dest = std::move(byte_update);
555 *dest = std::move(union_expr);
560 dest->
id() == ID_byte_update_big_endian ||
561 dest->
id() == ID_byte_update_little_endian)
566 dest = &byte_update.
op2();
584 if(full_type.
id()!=ID_struct &&
585 full_type.
id()!=ID_union &&
586 full_type.
id()!=ID_array &&
587 full_type.
id()!=ID_vector)
592 if(value.
id()==ID_initializer_list &&
608 if(full_type.
id()==ID_union)
615 if(!components.empty())
622 if(!zero.has_value())
625 error() <<
"cannot zero-initialize union component of type '"
636 if(value.
id()==ID_initializer_list)
641 else if(value.
id()==ID_string_constant)
647 full_type.
id() == ID_array &&
648 (full_type.
subtype().
id() == ID_signedbv ||
649 full_type.
subtype().
id() == ID_unsignedbv))
660 if(full_type.
id()==ID_struct ||
661 full_type.
id()==ID_union ||
662 full_type.
id()==ID_vector)
669 assert(full_type.
id()==ID_struct ||
670 full_type.
id()==ID_union ||
671 full_type.
id()==ID_array ||
672 full_type.
id()==ID_vector);
676 const typet dest_type=full_type;
685 warning() <<
"initialisation of " << dest_type.
id()
686 <<
" requires initializer list, found " << value.
id()
687 <<
" instead" <<
eom;
692 dest_type.
id()==ID_array &&
696 value.
id(ID_initializer_list);
698 for( ; init_it!=initializer_list.
operands().end(); ++init_it)
723 assert(!designator.
empty());
732 if(full_type.
id()==ID_array &&
736 if(full_type.
id()==ID_struct &&
744 assert(components.size()==entry.
size);
749 (components[entry.
index].get_is_padding() ||
750 (components[entry.
index].get_anonymous() &&
751 components[entry.
index].type().id() != ID_struct_tag &&
752 components[entry.
index].type().id() != ID_union_tag) ||
753 components[entry.
index].type().id() == ID_code))
765 if(designator.
size()==1)
771 assert(!designator.
empty());
776 const typet &src_type,
786 const exprt &d_op=*it;
790 if(full_type.
id()==ID_array)
792 if(d_op.
id()!=ID_index)
795 error() <<
"expected array index designator" <<
eom;
807 error() <<
"expected constant array index designator" <<
eom;
814 const auto size_opt =
820 error() <<
"expected constant array size" <<
eom;
824 entry.
index = numeric_cast_v<std::size_t>(index);
825 entry.
size = numeric_cast_v<std::size_t>(size);
828 else if(full_type.
id()==ID_struct ||
829 full_type.
id()==ID_union)
834 if(d_op.
id()!=ID_member)
837 error() <<
"expected member designator" <<
eom;
841 const irep_idt &component_name=d_op.
get(ID_component_name);
855 bool found=
false, repeat;
861 std::size_t number = 0;
865 for(
const auto &c : components)
867 if(c.get_name() == component_name)
871 entry.
size=components.size();
877 (c.type().id() == ID_struct_tag ||
878 c.type().id() == ID_union_tag) &&
882 entry.
size=components.size();
899 error() <<
"failed to find struct component '" << component_name
900 <<
"' in initialization of '" <<
to_string(struct_union_type)
909 error() <<
"designated initializers cannot initialize '"
918 assert(!designator.
empty());
928 assert(value.
id()==ID_initializer_list);
935 full_type.
id() == ID_array && value.
operands().size() >= 1 &&
937 (full_type.
subtype().
id() == ID_signedbv ||
938 full_type.
subtype().
id() == ID_unsignedbv) &&
945 warning() <<
"ignoring excess initializers" <<
eom;
953 if(full_type.
id()==ID_struct ||
954 full_type.
id()==ID_union ||
955 full_type.
id()==ID_vector)
959 if(!zero.has_value())
962 error() <<
"cannot zero-initialize '" <<
to_string(full_type) <<
"'"
968 else if(full_type.
id()==ID_array)
980 if(!zero.has_value())
983 error() <<
"cannot zero-initialize '" <<
to_string(full_type) <<
"'"
1001 <<
"' with an initializer list" <<
eom;
1010 for(exprt::operandst::const_iterator it=operands.begin();
1011 it!=operands.end(); )
1014 result, current_designator, value, it, force_constant);
1021 if(full_type.
id()==ID_struct)
1023 assert(
result.operands().size()==
1027 if(full_type.
id()==ID_array &&
1031 size_t size=
result.operands().size();
1032 result.type().id(ID_array);
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 componentst & components() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const typet & subtype() const
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)
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
#define Forall_operands(it, expr)
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
The type of an expression, extends irept.
ANSI-C Language Type Checking.
virtual std::string to_string(const exprt &expr)
Base type for structs and unions.
typet type
Type of symbol.
const irept & find(const irep_namet &name) const
Union constructor from single element.
const string_constantt & to_string_constant(const exprt &expr)
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
Base class for all expressions.
std::vector< componentt > componentst
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
void push_entry(const entryt &entry)
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
struct configt::ansi_ct ansi_c
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
irep_idt byte_update_id()
std::size_t component_number(const irep_idt &component_name) const
Return the sequence number of the component with given name.
bitvector_typet index_type()
optionalt< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
virtual void make_constant(exprt &expr)
virtual exprt do_initializer_list(const exprt &value, const typet &type, bool force_constant)
const exprt & size() const
typet & type()
Return the type of the expression.
bool has_component_rec(const typet &type, const irep_idt &component_name, const namespacet &ns)
bool get_bool(const irep_namet &name) const
Expression classes for byte-level operators.
Expression Initialization.
mstreamt & result() const
bool has_prefix(const std::string &s, const std::string &prefix)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
const std::string & id2string(const irep_idt &d)
source_locationt source_location
#define forall_operands(it, expr)
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
const entryt & front() const
bool has_component(const irep_idt &component_name) const
virtual void make_constant_index(exprt &expr)
const irep_idt & id() const
std::vector< exprt > operandst
const entryt & back() const
const constant_exprt & size() const
void designator_enter(const typet &type, designatort &designator)
virtual void typecheck_expr(exprt &expr)
bitvector_typet char_type()
std::size_t get_width() const
irep_idt get_component_name() const
exprt value
Initial value of symbol.
array_exprt to_array_expr() const
convert string into array constant
Structure type, corresponds to C style structs.
virtual exprt do_initializer_rec(const exprt &value, const typet &type, bool force_constant)
initialize something of type ‘type’ with given value ‘value’
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
const irep_idt & get(const irep_namet &name) const
designatort make_designator(const typet &type, const exprt &src)
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
C Language Type Checking.
void increment_designator(designatort &designator)
source_locationt & add_source_location()
mstreamt & warning() const
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
const source_locationt & source_location() const
Array constructor from list of elements.
irep_idt name
The unique identifier.
virtual void implicit_typecast(exprt &expr, const typet &type)
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.