38 "any array must have a size");
69 <<
"' is still incomplete -- cannot initialize" <<
eom;
102 error() <<
"array size needs to be constant, got "
110 error() <<
"array size must not be negative" <<
eom;
126 if(!zero.has_value())
129 error() <<
"cannot zero-initialize array with subtype '"
164 error() <<
"array size needs to be constant, got "
172 error() <<
"array size must not be negative" <<
eom;
188 if(!zero.has_value())
191 error() <<
"cannot zero-initialize array with subtype '"
206 error() <<
"type '" <<
to_string(type) <<
"' cannot be initialized with '"
215 <<
"' cannot be initialized with designated initializer" <<
eom;
268 c.type().id() !=
ID_code,
"struct member must not be of code type");
271 !
c.get_is_padding() &&
313 error() <<
"array has non-constant size '"
328 if(!vector_size.has_value())
331 error() <<
"vector has non-constant size '"
349 exprt::operandst::const_iterator
init_it,
363 designator.
front().type,
378 for(
size_t i=0; i<designator.
size(); i++)
380 size_t index=designator[i].index;
381 const typet &type=designator[i].type;
395 error() <<
"cannot zero-initialize array with element type '"
417 if(!zero.has_value())
420 error() <<
"cannot zero-initialize array with element type '"
430 error() <<
"array index designator " << index
431 <<
" out of bounds (" << dest->
operands().size()
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");
472 if(components.empty())
475 error() <<
"union member designator found for empty union" <<
eom;
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;
522 if(!zero.has_value())
525 error() <<
"cannot zero-initialize union component of type '"
567 const typet &type=designator.
back().subtype;
600 if(!components.empty())
607 if(!zero.has_value())
610 error() <<
"cannot zero-initialize union component of type '"
640 else if(value.
type() == type)
657 "full type must be composite");
662 const bool vla_permitted=designator.
back().vla_permitted;
671 <<
" requires initializer list, found " << value.
id()
672 <<
" instead" <<
eom;
727 components.size() == entry.
size,
"matching component numbers");
732 (components[entry.
index].get_is_padding() ||
733 (components[entry.
index].get_anonymous() &&
746 if(designator.
size()==1)
752 INVARIANT(!designator.
empty(),
"designator had more than one entry");
774 error() <<
"expected array index designator" <<
eom;
786 error() <<
"expected constant array index designator" <<
eom;
799 error() <<
"expected constant array size" <<
eom;
817 error() <<
"expected member designator" <<
eom;
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();
868 entry.
size=components.size();
885 error() <<
"failed to find struct component '" << component_name
895 error() <<
"designated initializers cannot initialize '"
929 warning() <<
"ignoring excess initializers" <<
eom;
943 if(!zero.has_value())
963 if(!zero.has_value())
981 else if(value.
operands().size() == 2)
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(); )
1036 !components.empty() &&
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.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Array constructor from list of elements.
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)
const irep_idt const irep_idt mode
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
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
typet & type()
Return the type of the expression.
const source_locationt & source_location() const
exprt & with_source_location(source_locationt location) &
Add the source location from location, if it is non-nil.
bool get_bool(const irep_idt &name) const
const irept & find(const irep_idt &name) const
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.
A struct tag type, i.e., struct_typet with an identifier.
Structure type, corresponds to C style structs.
Base type for structs and unions.
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.
#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)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_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 array_typet & to_array_type(const typet &type)
Cast a typet to an array_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)