33 if(type.
id()==ID_array)
38 "any array must have a size");
43 result.id() != ID_compound_literal)
62 (type.
id() == ID_struct_tag &&
64 (type.
id() == ID_union_tag &&
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 type.
id() == ID_array &&
98 const auto array_size = numeric_cast<mp_integer>(array_type.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 && 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 '"
196 tmp2.
operands().resize(numeric_cast_v<std::size_t>(*array_size), *zero);
206 error() <<
"type '" <<
to_string(type) <<
"' cannot be initialized with '"
211 if(value.
id()==ID_designated_initializer)
215 <<
"' cannot be initialized with designated initializer" <<
eom;
256 if(
auto struct_tag_type = type_try_dynamic_cast<struct_tag_typet>(type))
268 c.type().id() != ID_code,
"struct member must not be of code type");
271 !c.get_is_padding() &&
272 (c.type().id() != ID_c_bit_field || !c.get_anonymous()))
281 else if(
auto union_tag_type = type_try_dynamic_cast<union_tag_typet>(type))
298 else if(type.
id() == ID_array)
309 const auto array_size = numeric_cast<mp_integer>(array_type.
size());
310 if(!array_size.has_value())
313 error() <<
"array has non-constant size '"
318 entry.
size = numeric_cast_v<std::size_t>(*array_size);
322 else if(type.
id() == ID_vector)
326 const auto vector_size = numeric_cast<mp_integer>(vector_type.
size());
328 if(!vector_size.has_value())
331 error() <<
"vector has non-constant size '"
336 entry.
size = numeric_cast_v<std::size_t>(*vector_size);
348 const exprt &initializer_list,
349 exprt::operandst::const_iterator init_it,
353 exprt value=*init_it;
357 if(value.
id()==ID_designated_initializer)
364 static_cast<const exprt &
>(value.
find(ID_designator)));
370 result, designator, value, value.
operands().begin(), force_constant);
378 for(
size_t i=0; i<designator.
size(); i++)
380 size_t index=designator[i].index;
381 const typet &type=designator[i].type;
383 if(type.
id() == ID_array || type.
id() == ID_vector)
388 if(dest->
id() == ID_array_of)
391 const auto array_size = numeric_cast<mp_integer>(array_type.
size());
392 if(!array_size.has_value())
395 error() <<
"cannot zero-initialize array with element type '"
402 dest->
operands().resize(numeric_cast_v<std::size_t>(*array_size), zero);
417 if(!zero.has_value())
420 error() <<
"cannot zero-initialize array with element type '"
425 numeric_cast_v<std::size_t>(index) + 1, *zero);
430 error() <<
"array index designator " << index
431 <<
" out of bounds (" << dest->
operands().size()
437 dest = &(dest->
operands()[numeric_cast_v<std::size_t>(index)]);
440 auto struct_tag_type = type_try_dynamic_cast<struct_tag_typet>(type))
448 error() <<
"structure member designator " << index
449 <<
" out of bounds (" << dest->
operands().size()
455 "member designator is bounded by components size");
457 components[index].type().
id() != ID_code,
458 "struct member must not be of code type");
460 !components[index].get_is_padding(),
461 "member designator points at non-padding member");
465 else if(
auto union_tag_type = type_try_dynamic_cast<union_tag_typet>(type))
472 if(components.empty())
475 error() <<
"union member designator found for empty union" <<
eom;
478 else if(init_it != initializer_list.
operands().begin())
483 error() <<
"too many initializers" <<
eom;
489 warning() <<
"excess elements in union initializer" <<
eom;
494 else if(index >= components.size())
497 error() <<
"union member designator " << index <<
" out of bounds ("
498 << components.size() <<
")" <<
eom;
505 dest->
id() == ID_union &&
512 else if(dest->
id() == ID_union)
522 if(!zero.has_value())
525 error() <<
"cannot zero-initialize union component of type '"
535 *dest = std::move(byte_update);
542 *dest = std::move(union_expr);
547 dest->
id() == ID_byte_update_big_endian ||
548 dest->
id() == ID_byte_update_little_endian)
553 dest = &byte_update.
op2();
571 type.
id() != ID_struct_tag && type.
id() != ID_union_tag &&
572 type.
id() != ID_array && type.
id() != ID_vector)
577 if(value.
id()==ID_initializer_list &&
593 if(
auto union_tag_type = type_try_dynamic_cast<union_tag_typet>(type))
600 if(!components.empty())
607 if(!zero.has_value())
610 error() <<
"cannot zero-initialize union component of type '"
621 if(value.
id()==ID_initializer_list)
626 else if(value.
id()==ID_string_constant)
632 type.
id() == ID_array &&
640 else if(value.
type() == type)
646 type.
id() == ID_struct_tag || type.
id() == ID_union_tag ||
647 type.
id() == ID_vector)
655 type.
id() == ID_struct_tag || type.
id() == ID_union_tag ||
656 type.
id() == ID_array || type.
id() == ID_vector,
657 "full type must be composite");
661 const typet dest_type = type;
670 warning() <<
"initialisation of " << dest_type.
id()
671 <<
" requires initializer list, found " << value.
id()
672 <<
" instead" <<
eom;
677 dest_type.
id()==ID_array &&
681 value.
id(ID_initializer_list);
683 for( ; init_it!=initializer_list.
operands().end(); ++init_it)
727 components.size() == entry.
size,
"matching component numbers");
732 (components[entry.
index].get_is_padding() ||
733 (components[entry.
index].get_anonymous() &&
734 components[entry.
index].type().id() == ID_c_bit_field)))
746 if(designator.
size()==1)
752 INVARIANT(!designator.
empty(),
"designator had more than one entry");
757 const typet &src_type,
765 for(
const auto &d_op : src.
operands())
769 if(entry.
type.
id() == ID_array)
771 if(d_op.id()!=ID_index)
774 error() <<
"expected array index designator" <<
eom;
786 error() <<
"expected constant array index designator" <<
eom;
793 const auto size_opt =
799 error() <<
"expected constant array size" <<
eom;
803 entry.
index = numeric_cast_v<std::size_t>(index);
804 entry.
size = numeric_cast_v<std::size_t>(size);
808 auto struct_union_tag_type =
809 type_try_dynamic_cast<struct_or_union_tag_typet>(entry.
type))
814 if(d_op.id()!=ID_member)
817 error() <<
"expected member designator" <<
eom;
821 const irep_idt &component_name=d_op.get(ID_component_name);
836 bool found=
false, repeat;
842 std::size_t number = 0;
846 for(
const auto &c : components)
848 if(c.get_name() == component_name)
852 entry.
size=components.size();
858 (c.type().id() == ID_struct_tag ||
859 c.type().id() == ID_union_tag) &&
868 entry.
size=components.size();
885 error() <<
"failed to find struct component '" << component_name
886 <<
"' in initialization of '" <<
to_string(struct_union_type)
895 error() <<
"designated initializers cannot initialize '"
919 type.
id() == ID_array && value.
operands().size() >= 1 &&
929 warning() <<
"ignoring excess initializers" <<
eom;
938 type.
id() == ID_struct_tag || type.
id() == ID_union_tag ||
939 type.
id() == ID_vector)
943 if(!zero.has_value())
951 else if(type.
id() == ID_array)
963 if(!zero.has_value())
972 else if(type.
id() == ID_complex)
981 else if(value.
operands().size() == 2)
984 auto &subtype = complex_type.subtype();
995 <<
"too many initializers for '" <<
to_string(type) <<
"'";
1009 <<
"' with an initializer list" <<
eom;
1018 for(exprt::operandst::const_iterator it=operands.begin();
1019 it!=operands.end(); )
1022 result, current_designator, value, it, force_constant);
1028 if(
auto struct_tag_type = type_try_dynamic_cast<struct_tag_typet>(type))
1036 !components.empty() &&
1037 components.back().type().get_bool(ID_C_flexible_array_member))
1039 const auto array_size = numeric_cast<mp_integer>(
1043 !array_size.has_value() ||
1044 (*array_size <= 1 && init_array.
operands().size() != *array_size))
1051 actual_array_type.
set(ID_C_flexible_array_member,
true);
1052 init_array.
type() = actual_array_type;
1055 actual_struct_type.
remove(ID_tag);
1056 std::string typestr =
type2name(actual_struct_type, *
this);
1057 irep_idt tag_identifier =
"tag-#anon#" + typestr;
1059 compound_symbol.base_name =
"#anon#" + typestr;
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_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Array constructor from list of elements.
const array_typet & type() const
typet index_type() const
The type of the index expressions into any instance of this type.
const typet & element_type() const
The type of the elements of the array.
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)
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)
virtual void make_constant_index(exprt &expr)
designatort make_designator(const typet &type, const exprt &src)
void designator_enter(const typet &type, designatort &designator)
Complex constructor from a pair of numbers.
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.
bool starts_with(const char *s) const
equivalent of as_string().starts_with(s)
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
exprt & with_source_location(source_locationt location) &
Add the source location from location, if it is non-nil.
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_idt &name) const
const irept & find(const irep_idt &name) const
void remove(const irep_idt &name)
void set(const irep_idt &name, const irep_idt &value)
const irep_idt & id() const
source_locationt source_location
mstreamt & warning() const
mstreamt & result() const
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
const array_typet & type() const
array_exprt to_array_expr() const
convert string into array constant
A struct tag type, i.e., struct_typet with an identifier.
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
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.
errort with_location(source_locationt _location) &&
The type of an expression, extends irept.
Union constructor from single element.
irep_idt get_component_name() const
const constant_exprt & size() const
const typet & element_type() const
The type of the elements of the vector.
#define Forall_operands(it, expr)
std::optional< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
Expression Initialization.
#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)
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 array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_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 binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_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 array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
const struct_or_union_tag_typet & to_struct_or_union_tag_type(const typet &type)
Cast a typet to a struct_or_union_tag_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)