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;
130 if(value.
id()==ID_string_constant &&
131 full_type.
id()==ID_array &&
132 (full_type.
subtype().
id()==ID_signedbv ||
133 full_type.
subtype().
id()==ID_unsignedbv) &&
144 if(full_type.
id()==ID_array &&
152 error() <<
"array size needs to be constant, got " 160 error() <<
"array size must not be negative" <<
eom;
187 if(full_type.
id()==ID_array &&
192 <<
"' cannot be initialized with `" <<
to_string(value)
197 if(value.
id()==ID_designated_initializer)
201 <<
"' cannot be initialized with designated initializer" 262 if(full_type.
id()==ID_struct)
271 for(struct_typet::componentst::const_iterator
276 if(it->type().id()!=ID_code &&
277 !it->get_is_padding())
286 else if(full_type.
id()==ID_union)
303 else if(full_type.
id()==ID_array)
319 error() <<
"array has non-constant size `" 328 else if(full_type.
id()==ID_vector)
337 error() <<
"vector has non-constant 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 &&
415 error() <<
"array index designator " << index
416 <<
" out of bounds (" << dest->
operands().size()
424 else if(full_type.
id()==ID_struct)
432 error() <<
"structure member designator " << index
433 <<
" out of bounds (" << dest->
operands().size()
439 "member designator is bounded by components size");
441 !components[index].get_is_padding(),
442 "member designator points at data member");
446 else if(full_type.
id()==ID_union)
454 "member designator is bounded by components size");
458 if(dest->
id()==ID_union &&
459 dest->
get(ID_component_name)==component.get_name())
495 assert(full_type.
id()!=ID_symbol);
498 if(full_type.
id()!=ID_struct &&
499 full_type.
id()!=ID_union &&
500 full_type.
id()!=ID_array &&
501 full_type.
id()!=ID_vector)
506 if(value.
id()==ID_initializer_list &&
519 if(full_type.
id()==ID_union)
526 if(!components.empty())
545 if(value.
id()==ID_initializer_list)
550 else if(value.
id()==ID_string_constant)
555 if(full_type.
id()==ID_array &&
568 if(full_type.
id()==ID_struct ||
569 full_type.
id()==ID_union ||
570 full_type.
id()==ID_vector)
577 assert(full_type.
id()==ID_struct ||
578 full_type.
id()==ID_union ||
579 full_type.
id()==ID_array ||
580 full_type.
id()==ID_vector);
584 const typet dest_type=full_type;
593 warning() <<
"initialisation of " << dest_type.id()
594 <<
" requires initializer list, found " << value.
id()
595 <<
" instead" <<
eom;
600 dest_type.id()==ID_array &&
604 value.
id(ID_initializer_list);
606 for( ; init_it!=initializer_list.
operands().end(); ++init_it)
615 error() <<
"cannot initialize type `" 616 <<
to_string(dest_type) <<
"' using value `" 632 assert(!designator.
empty());
641 if(full_type.
id()==ID_array &&
645 if(full_type.
id()==ID_struct &&
653 assert(components.size()==entry.
size);
657 (components[entry.
index].get_is_padding() ||
658 components[entry.
index].type().id()==ID_code))
668 if(designator.
size()==1)
674 assert(!designator.
empty());
679 const typet &src_type,
689 const exprt &d_op=*it;
693 if(full_type.
id()==ID_array)
695 if(d_op.
id()!=ID_index)
698 error() <<
"expected array index designator" <<
eom;
711 error() <<
"expected constant array index designator" <<
eom;
720 error() <<
"expected constant array size" <<
eom;
728 else if(full_type.
id()==ID_struct ||
729 full_type.
id()==ID_union)
734 if(d_op.
id()!=ID_member)
737 error() <<
"expected member designator" <<
eom;
741 const irep_idt &component_name=d_op.
get(ID_component_name);
755 bool found=
false, repeat;
765 for(struct_union_typet::componentst::const_iterator
766 c_it=components.begin();
767 c_it!=components.end();
770 if(c_it->get_name()==component_name)
774 entry.
size=components.size();
778 else if(c_it->get_anonymous() &&
779 (
follow(c_it->type()).
id()==ID_struct ||
780 follow(c_it->type()).
id()==ID_union) &&
782 c_it->type(), component_name, *
this))
785 entry.
size=components.size();
800 error() <<
"failed to find struct component `" 801 << component_name <<
"' in initialization of `" 810 error() <<
"designated initializers cannot initialize `" 819 assert(!designator.
empty());
829 assert(value.
id()==ID_initializer_list);
834 if(full_type.id()==ID_struct ||
835 full_type.id()==ID_union ||
836 full_type.id()==ID_vector)
843 else if(full_type.id()==ID_array)
862 value.
op0().
id()==ID_string_constant &&
863 (full_type.subtype().id()==ID_signedbv ||
864 full_type.subtype().id()==ID_unsignedbv) &&
865 full_type.subtype().get(ID_width)==
char_type().
get(ID_width))
870 warning() <<
"ignoring excess initializers" <<
eom;
886 <<
"' with an initializer list" <<
eom;
895 for(exprt::operandst::const_iterator it=operands.begin();
896 it!=operands.end(); )
899 result, current_designator, value, it, force_constant);
906 if(full_type.id()==ID_struct)
908 assert(
result.operands().size()==
912 if(full_type.id()==ID_array &&
916 size_t size=
result.operands().size();
917 result.type().id(ID_array);
const irep_idt & get_name() const
The type of an expression.
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)
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)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
static mstreamt & eom(mstreamt &m)
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
ANSI-C Language Type Checking.
const entryt & back() const
const source_locationt & find_source_location() const
source_locationt source_location
A constant-size array type.
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 generic 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)
void err_location(const source_locationt &loc)
array_exprt to_array_expr() const
convert string into array constant
const typet & follow(const typet &) const
bitvector_typet index_type()
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
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
exprt zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns, message_handlert &message_handler)
std::vector< exprt > operandst
virtual void implicit_typecast(exprt &expr, const typet &type)
typet type
Type of symbol.
message_handlert & get_message_handler()
Base type of C structs and unions, and C++ classes.
mstreamt & result() const
const string_constantt & to_string_constant(const exprt &expr)
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Base class for all expressions.
std::size_t component_number(const irep_idt &component_name) const
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
const source_locationt & source_location() const
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)
void set_component_name(const irep_idt &component_name)
source_locationt & add_source_location()
virtual void do_initializer(exprt &initializer, const typet &type, bool force_constant)
std::size_t integer2size_t(const mp_integer &n)
const typet & subtype() const
#define DATA_INVARIANT(CONDITION, REASON)
const irept & find(const irep_namet &name) const
bitvector_typet char_type()
C Language Type Checking.