33 if(type.
id()==ID_array)
38 "any array must have a size");
43 result.id() != ID_compound_literal)
64 (full_type.
id() == ID_struct || full_type.
id() == ID_union) &&
69 <<
"' is still incomplete -- cannot initialize" <<
eom;
73 if(value.
id()==ID_initializer_list)
77 value.
id() == ID_array && value.
get_bool(ID_C_string_constant) &&
78 full_type.
id() == ID_array &&
79 (full_type.
subtype().
id() == ID_signedbv ||
80 full_type.
subtype().
id() == ID_unsignedbv) &&
92 if(full_type.
id()==ID_array &&
96 const auto array_size =
98 if(!array_size.has_value())
101 error() <<
"array size needs to be constant, got "
109 error() <<
"array size must not be negative" <<
eom;
116 tmp.
operands().resize(numeric_cast_v<std::size_t>(*array_size));
125 if(!zero.has_value())
128 error() <<
"cannot zero-initialize array with subtype '"
132 tmp.
operands().resize(numeric_cast_v<std::size_t>(*array_size), *zero);
140 value.
id() == ID_string_constant && full_type.
id() == ID_array &&
141 (full_type.
subtype().
id() == ID_signedbv ||
142 full_type.
subtype().
id() == ID_unsignedbv) &&
154 if(full_type.
id()==ID_array &&
158 const auto array_size =
160 if(!array_size.has_value())
163 error() <<
"array size needs to be constant, got "
171 error() <<
"array size must not be negative" <<
eom;
178 tmp2.
operands().resize(numeric_cast_v<std::size_t>(*array_size));
187 if(!zero.has_value())
190 error() <<
"cannot zero-initialize array with subtype '"
194 tmp2.
operands().resize(numeric_cast_v<std::size_t>(*array_size), *zero);
201 if(full_type.
id()==ID_array &&
206 <<
"' cannot be initialized with '" <<
to_string(value) <<
"'"
211 if(value.
id()==ID_designated_initializer)
215 <<
"' cannot be initialized with designated initializer" <<
eom;
239 symbol.
type.
id() == ID_array &&
262 symbol.
type.
id() == ID_array &&
277 if(full_type.
id()==ID_struct)
288 if(c.type().id() != ID_code && !c.get_is_padding())
297 else if(full_type.
id()==ID_union)
314 else if(full_type.
id()==ID_array)
325 const auto array_size = numeric_cast<mp_integer>(array_type.
size());
326 if(!array_size.has_value())
329 error() <<
"array has non-constant size '"
334 entry.
size = numeric_cast_v<std::size_t>(*array_size);
338 else if(full_type.
id()==ID_vector)
342 const auto vector_size = numeric_cast<mp_integer>(vector_type.
size());
344 if(!vector_size.has_value())
347 error() <<
"vector has non-constant size '"
352 entry.
size = numeric_cast_v<std::size_t>(*vector_size);
364 const exprt &initializer_list,
365 exprt::operandst::const_iterator init_it,
369 exprt value=*init_it;
371 assert(!designator.
empty());
373 if(value.
id()==ID_designated_initializer)
380 static_cast<const exprt &
>(value.
find(ID_designator)));
382 assert(!designator.
empty());
386 result, designator, value, value.
operands().begin(), force_constant);
394 for(
size_t i=0; i<designator.
size(); i++)
396 size_t index=designator[i].index;
397 const typet &type=designator[i].type;
400 if(full_type.
id()==ID_array ||
401 full_type.
id()==ID_vector)
406 if(dest->
id() == ID_array_of)
409 const auto array_size = numeric_cast<mp_integer>(array_type.
size());
410 if(!array_size.has_value())
413 error() <<
"cannot zero-initialize array with subtype '"
419 dest->
operands().resize(numeric_cast_v<std::size_t>(*array_size), zero);
424 if(full_type.
id()==ID_array &&
431 if(!zero.has_value())
434 error() <<
"cannot zero-initialize array with subtype '"
439 numeric_cast_v<std::size_t>(index) + 1, *zero);
446 error() <<
"array index designator " << index
447 <<
" out of bounds (" << dest->
operands().size()
453 dest = &(dest->
operands()[numeric_cast_v<std::size_t>(index)]);
455 else if(full_type.
id()==ID_struct)
463 error() <<
"structure member designator " << index
464 <<
" out of bounds (" << dest->
operands().size()
470 "member designator is bounded by components size");
472 !components[index].get_is_padding(),
473 "member designator points at data member");
477 else if(full_type.
id()==ID_union)
484 if(components.empty())
487 error() <<
"union member designator found for empty union" <<
eom;
490 else if(init_it != initializer_list.
operands().begin())
495 error() <<
"too many initializers" <<
eom;
501 warning() <<
"excess elements in union initializer" <<
eom;
506 else if(index >= components.size())
509 error() <<
"union member designator " << index <<
" out of bounds ("
510 << components.size() <<
")" <<
eom;
517 dest->
id() == ID_union &&
524 else if(dest->
id() == ID_union)
534 if(!zero.has_value())
537 error() <<
"cannot zero-initialize union component of type '"
547 *dest = std::move(byte_update);
554 *dest = std::move(union_expr);
559 dest->
id() == ID_byte_update_big_endian ||
560 dest->
id() == ID_byte_update_little_endian)
565 dest = &byte_update.
op2();
583 if(full_type.
id()!=ID_struct &&
584 full_type.
id()!=ID_union &&
585 full_type.
id()!=ID_array &&
586 full_type.
id()!=ID_vector)
591 if(value.
id()==ID_initializer_list &&
607 if(full_type.
id()==ID_union)
614 if(!components.empty())
621 if(!zero.has_value())
624 error() <<
"cannot zero-initialize union component of type '"
635 if(value.
id()==ID_initializer_list)
640 else if(value.
id()==ID_string_constant)
646 full_type.
id() == ID_array &&
647 (full_type.
subtype().
id() == ID_signedbv ||
648 full_type.
subtype().
id() == ID_unsignedbv))
659 if(full_type.
id()==ID_struct ||
660 full_type.
id()==ID_union ||
661 full_type.
id()==ID_vector)
668 assert(full_type.
id()==ID_struct ||
669 full_type.
id()==ID_union ||
670 full_type.
id()==ID_array ||
671 full_type.
id()==ID_vector);
675 const typet dest_type=full_type;
684 warning() <<
"initialisation of " << dest_type.
id()
685 <<
" requires initializer list, found " << value.
id()
686 <<
" instead" <<
eom;
691 dest_type.
id()==ID_array &&
695 value.
id(ID_initializer_list);
697 for( ; init_it!=initializer_list.
operands().end(); ++init_it)
722 assert(!designator.
empty());
731 if(full_type.
id()==ID_array &&
735 if(full_type.
id()==ID_struct &&
743 assert(components.size()==entry.
size);
748 (components[entry.
index].get_is_padding() ||
749 (components[entry.
index].get_anonymous() &&
750 components[entry.
index].type().id() != ID_struct_tag &&
751 components[entry.
index].type().id() != ID_union_tag) ||
752 components[entry.
index].type().id() == ID_code))
764 if(designator.
size()==1)
770 assert(!designator.
empty());
775 const typet &src_type,
785 const exprt &d_op=*it;
789 if(full_type.
id()==ID_array)
791 if(d_op.
id()!=ID_index)
794 error() <<
"expected array index designator" <<
eom;
806 error() <<
"expected constant array index designator" <<
eom;
813 const auto size_opt =
819 error() <<
"expected constant array size" <<
eom;
823 entry.
index = numeric_cast_v<std::size_t>(index);
824 entry.
size = numeric_cast_v<std::size_t>(size);
827 else if(full_type.
id()==ID_struct ||
828 full_type.
id()==ID_union)
833 if(d_op.
id()!=ID_member)
836 error() <<
"expected member designator" <<
eom;
840 const irep_idt &component_name=d_op.
get(ID_component_name);
854 bool found=
false, repeat;
860 std::size_t number = 0;
864 for(
const auto &c : components)
866 if(c.get_name() == component_name)
870 entry.
size=components.size();
876 (c.type().id() == ID_struct_tag ||
877 c.type().id() == ID_union_tag) &&
881 entry.
size=components.size();
898 error() <<
"failed to find struct component '" << component_name
899 <<
"' in initialization of '" <<
to_string(struct_union_type)
908 error() <<
"designated initializers cannot initialize '"
917 assert(!designator.
empty());
927 assert(value.
id()==ID_initializer_list);
934 full_type.
id() == ID_array && value.
operands().size() >= 1 &&
936 (full_type.
subtype().
id() == ID_signedbv ||
937 full_type.
subtype().
id() == ID_unsignedbv) &&
944 warning() <<
"ignoring excess initializers" <<
eom;
952 if(full_type.
id()==ID_struct ||
953 full_type.
id()==ID_union ||
954 full_type.
id()==ID_vector)
958 if(!zero.has_value())
961 error() <<
"cannot zero-initialize '" <<
to_string(full_type) <<
"'"
967 else if(full_type.
id()==ID_array)
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(); )
1013 result, current_designator, value, it, force_constant);
1020 if(full_type.
id()==ID_struct)
1022 assert(
result.operands().size()==
1026 if(full_type.
id()==ID_array &&
1030 size_t size=
result.operands().size();
1031 result.type().id(ID_array);
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 index_type()
bitvector_typet char_type()
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Array constructor from list of elements.
const exprt & size() const
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.
source_locationt & add_source_location()
const source_locationt & source_location() const
typet & type()
Return the type of the expression.
bool get_bool(const irep_namet &name) const
const irept & find(const irep_namet &name) const
const irep_idt & id() const
const irep_idt & get(const irep_namet &name) 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.
array_exprt to_array_expr() const
convert string into array constant
Structure type, corresponds to C style structs.
Base type for structs and unions.
bool has_component(const irep_idt &component_name) const
const componentst & components() const
std::size_t component_number(const irep_idt &component_name) const
Return the sequence number of the component with given name.
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.
const typet & subtype() const
Union constructor from single element.
irep_idt get_component_name() const
const constant_exprt & size() 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 constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
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 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)
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.