33 if(type.
id()==ID_array)
38 "any array must have a size");
61 if(full_type.
id()==ID_incomplete_struct)
65 <<
"' is still incomplete -- cannot initialize" <<
eom;
69 if(value.
id()==ID_initializer_list)
72 if(value.
id()==ID_array &&
73 value.
get_bool(ID_C_string_constant) &&
74 full_type.
id()==ID_array &&
76 full_type.
subtype().
id()==ID_unsignedbv) &&
87 if(full_type.
id()==ID_array &&
95 error() <<
"array size needs to be constant, got " 103 error() <<
"array size must not be negative" <<
eom;
110 tmp.
operands().resize(numeric_cast_v<std::size_t>(array_size));
119 if(!zero.has_value())
122 error() <<
"cannot zero-initialize array with subtype `" 126 tmp.
operands().resize(numeric_cast_v<std::size_t>(array_size), *zero);
133 if(value.
id()==ID_string_constant &&
134 full_type.
id()==ID_array &&
135 (full_type.
subtype().
id()==ID_signedbv ||
136 full_type.
subtype().
id()==ID_unsignedbv) &&
147 if(full_type.
id()==ID_array &&
155 error() <<
"array size needs to be constant, got " 163 error() <<
"array size must not be negative" <<
eom;
170 tmp2.
operands().resize(numeric_cast_v<std::size_t>(array_size));
179 if(!zero.has_value())
182 error() <<
"cannot zero-initialize array with subtype `" 186 tmp2.
operands().resize(numeric_cast_v<std::size_t>(array_size), *zero);
193 if(full_type.
id()==ID_array &&
198 <<
"' cannot be initialized with `" <<
to_string(value)
203 if(value.
id()==ID_designated_initializer)
207 <<
"' cannot be initialized with designated initializer" 268 if(full_type.
id()==ID_struct)
279 if(c.type().id() != ID_code && !c.get_is_padding())
288 else if(full_type.
id()==ID_union)
305 else if(full_type.
id()==ID_array)
321 error() <<
"array has non-constant size `" 326 entry.
size = numeric_cast_v<std::size_t>(array_size);
330 else if(full_type.
id()==ID_vector)
339 error() <<
"vector has non-constant size `" 344 entry.
size = numeric_cast_v<std::size_t>(vector_size);
356 const exprt &initializer_list,
357 exprt::operandst::const_iterator init_it,
361 exprt value=*init_it;
363 assert(!designator.
empty());
365 if(value.
id()==ID_designated_initializer)
371 designator.front().type,
372 static_cast<const exprt &
>(value.
find(ID_designator)));
374 assert(!designator.empty());
378 result, designator, value, value.
operands().begin(), force_constant);
386 for(
size_t i=0; i<designator.
size(); i++)
388 size_t index=designator[i].index;
389 const typet &type=designator[i].type;
392 if(full_type.
id()==ID_array ||
393 full_type.
id()==ID_vector)
397 if(full_type.
id()==ID_array &&
404 if(!zero.has_value())
407 error() <<
"cannot zero-initialize array with subtype `" 412 numeric_cast_v<std::size_t>(index) + 1, *zero);
419 error() <<
"array index designator " << index
420 <<
" out of bounds (" << dest->
operands().size()
426 dest = &(dest->
operands()[numeric_cast_v<std::size_t>(index)]);
428 else if(full_type.
id()==ID_struct)
436 error() <<
"structure member designator " << index
437 <<
" out of bounds (" << dest->
operands().size()
443 "member designator is bounded by components size");
445 !components[index].get_is_padding(),
446 "member designator points at data member");
450 else if(full_type.
id()==ID_union)
458 "member designator is bounded by components size");
462 if(dest->
id()==ID_union &&
474 if(!zero.has_value())
477 error() <<
"cannot zero-initialize union component of type `" 504 if(full_type.
id()!=ID_struct &&
505 full_type.
id()!=ID_union &&
506 full_type.
id()!=ID_array &&
507 full_type.
id()!=ID_vector)
512 if(value.
id()==ID_initializer_list &&
525 if(full_type.
id()==ID_union)
532 if(!components.empty())
539 if(!zero.has_value())
542 error() <<
"cannot zero-initialize union component of type `" 553 if(value.
id()==ID_initializer_list)
558 else if(value.
id()==ID_string_constant)
563 if(full_type.
id()==ID_array &&
576 if(full_type.
id()==ID_struct ||
577 full_type.
id()==ID_union ||
578 full_type.
id()==ID_vector)
585 assert(full_type.
id()==ID_struct ||
586 full_type.
id()==ID_union ||
587 full_type.
id()==ID_array ||
588 full_type.
id()==ID_vector);
592 const typet dest_type=full_type;
601 warning() <<
"initialisation of " << dest_type.id()
602 <<
" requires initializer list, found " << value.
id()
603 <<
" instead" <<
eom;
608 dest_type.id()==ID_array &&
612 value.
id(ID_initializer_list);
614 for( ; init_it!=initializer_list.
operands().end(); ++init_it)
623 error() <<
"cannot initialize type `" 624 <<
to_string(dest_type) <<
"' using value `" 640 assert(!designator.
empty());
649 if(full_type.
id()==ID_array &&
653 if(full_type.
id()==ID_struct &&
661 assert(components.size()==entry.
size);
665 (components[entry.
index].get_is_padding() ||
666 components[entry.
index].type().id()==ID_code))
676 if(designator.
size()==1)
682 assert(!designator.
empty());
687 const typet &src_type,
697 const exprt &d_op=*it;
701 if(full_type.
id()==ID_array)
703 if(d_op.
id()!=ID_index)
706 error() <<
"expected array index designator" <<
eom;
719 error() <<
"expected constant array index designator" <<
eom;
728 error() <<
"expected constant array size" <<
eom;
732 entry.
index = numeric_cast_v<std::size_t>(index);
733 entry.
size = numeric_cast_v<std::size_t>(size);
736 else if(full_type.
id()==ID_struct ||
737 full_type.
id()==ID_union)
742 if(d_op.
id()!=ID_member)
745 error() <<
"expected member designator" <<
eom;
749 const irep_idt &component_name=d_op.
get(ID_component_name);
763 bool found=
false, repeat;
769 std::size_t number = 0;
773 for(
const auto &c : components)
775 if(c.get_name() == component_name)
779 entry.
size=components.size();
784 c.get_anonymous() && (
follow(c.type()).
id() == ID_struct ||
785 follow(c.type()).
id() == ID_union) &&
789 entry.
size=components.size();
806 error() <<
"failed to find struct component `" 807 << component_name <<
"' in initialization of `" 816 error() <<
"designated initializers cannot initialize `" 825 assert(!designator.
empty());
835 assert(value.
id()==ID_initializer_list);
840 if(full_type.id()==ID_struct ||
841 full_type.id()==ID_union ||
842 full_type.id()==ID_vector)
846 if(!zero.has_value())
849 error() <<
"cannot zero-initialize `" <<
to_string(full_type) <<
"'" 855 else if(full_type.id()==ID_array)
867 if(!zero.has_value())
870 error() <<
"cannot zero-initialize `" <<
to_string(full_type) <<
"'" 880 value.
op0().
id()==ID_string_constant &&
881 (full_type.subtype().id()==ID_signedbv ||
882 full_type.subtype().id()==ID_unsignedbv) &&
883 full_type.subtype().get(ID_width)==
char_type().
get(ID_width))
888 warning() <<
"ignoring excess initializers" <<
eom;
904 <<
"' with an initializer list" <<
eom;
913 for(exprt::operandst::const_iterator it=operands.begin();
914 it!=operands.end(); )
917 result, current_designator, value, it, force_constant);
924 if(full_type.id()==ID_struct)
926 assert(
result.operands().size()==
930 if(full_type.id()==ID_array &&
934 size_t size=
result.operands().size();
935 result.type().id(ID_array);
The type of an expression, extends irept.
irep_idt name
The unique identifier.
const std::string & id2string(const irep_idt &d)
virtual void make_constant(exprt &expr)
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
std::vector< componentt > componentst
void push_entry(const entryt &entry)
exprt value
Initial value of symbol.
const componentst & components() const
bool has_component_rec(const typet &type, const irep_idt &component_name, const namespacet &ns)
typet & type()
Return the type of the expression.
#define CHECK_RETURN(CONDITION)
Structure type, corresponds to C style structs.
bool get_bool(const irep_namet &name) const
virtual std::string to_string(const exprt &expr)
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)
mstreamt & warning() const
Expression Initialization.
const irep_idt & id() const
optionalt< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
ANSI-C Language Type Checking.
const entryt & back() const
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
source_locationt source_location
Union constructor from single element.
const irep_idt & get(const irep_namet &name) const
void increment_designator(designatort &designator)
const exprt & size() const
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
bool has_prefix(const std::string &s, const std::string &prefix)
const exprt & size() const
virtual void typecheck_expr(exprt &expr)
#define forall_operands(it, expr)
array_exprt to_array_expr() const
convert string into array constant
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
bitvector_typet index_type()
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
void designator_enter(const typet &type, designatort &designator)
virtual exprt do_initializer_rec(const exprt &value, const typet &type, bool force_constant)
initialize something of type ‘type’ with given value ‘value’
bool has_component(const irep_idt &component_name) const
std::vector< exprt > operandst
virtual void implicit_typecast(exprt &expr, const typet &type)
typet type
Type of symbol.
Base type for structs and unions.
mstreamt & result() const
const string_constantt & to_string_constant(const exprt &expr)
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Base class for all expressions.
std::size_t component_number(const irep_idt &component_name) const
Return the sequence number of the component with given name.
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
const source_locationt & source_location() const
#define UNREACHABLE
This should be used to mark dead code.
virtual void make_constant_index(exprt &expr)
designatort make_designator(const typet &type, const exprt &src)
virtual exprt do_initializer_list(const exprt &value, const typet &type, bool force_constant)
#define Forall_operands(it, expr)
bool is_zero() const
Return whether the expression is a constant representing 0.
source_locationt & add_source_location()
virtual void do_initializer(exprt &initializer, const typet &type, bool force_constant)
const typet & subtype() const
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions, goto_programs, exprts, etc.
const irept & find(const irep_namet &name) const
bitvector_typet char_type()
C Language Type Checking.