68 if(type_id==ID_unsignedbv ||
69 type_id==ID_signedbv ||
70 type_id==ID_pointer ||
72 type_id==ID_incomplete_c_enum ||
73 type_id==ID_c_bit_field ||
76 type_id==ID_floatbv ||
80 result.add_source_location()=source_location;
83 else if(type_id==ID_rational ||
87 result.add_source_location()=source_location;
90 else if(type_id==ID_verilog_signedbv ||
91 type_id==ID_verilog_unsignedbv)
94 std::string value(width,
'0');
97 result.add_source_location()=source_location;
100 else if(type_id==ID_complex)
104 result.add_source_location()=source_location;
107 else if(type_id==ID_code)
110 error() <<
"cannot zero-initialize code-type" <<
eom;
113 else if(type_id==ID_array)
122 value.
type().
id(ID_array);
133 if(array_type.
size().
id()==ID_infinity)
135 exprt value(ID_array_of, type);
143 error() <<
"failed to zero-initialize array of non-fixed size `" 151 error() <<
"failed to zero-initialize array of with negative size" 162 else if(type_id==ID_vector)
173 error() <<
"failed to zero-initialize vector of non-fixed size `" 181 error() <<
"failed to zero-initialize vector of with negative size" 192 else if(type_id==ID_struct)
197 exprt value(ID_struct, type);
199 value.
operands().reserve(components.size());
201 for(struct_typet::componentst::const_iterator
202 it=components.begin();
203 it!=components.end();
206 if(it->type().id()==ID_code)
210 code_value.add_source_location()=source_location;
222 else if(type_id==ID_union)
235 for(struct_typet::componentst::const_iterator
236 it=components.begin();
237 it!=components.end();
241 if(it->type().id()==ID_code)
246 if(bits>component_size)
270 else if(type_id==ID_symbol)
279 else if(type_id==ID_c_enum_tag)
286 else if(type_id==ID_struct_tag)
293 else if(type_id==ID_union_tag)
300 else if(type_id==ID_string)
320 return z_i(type, source_location);
328 std::ostringstream oss;
334 return z_i(type, source_location);
const irep_idt & get_name() const
The type of an expression.
const typet & follow(const typet &src) const
Linking: Zero Initialization.
std::string to_string(const typet &src)
std::string to_string(const exprt &src)
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
void copy_to_operands(const exprt &expr)
std::vector< componentt > componentst
const componentst & components() const
mp_integer pointer_offset_bits(const typet &type, const namespacet &ns)
unsignedbv_typet size_type()
A constant literal expression.
static mstreamt & eom(mstreamt &m)
const typet & follow_tag(const union_tag_typet &src) const
const irep_idt & id() const
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
void set_value(const irep_idt &value)
exprt zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns, message_handlert &message_handler)
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a generic typet to a c_enum_tag_typet.
source_locationt source_location
A constant-size array type.
union constructor from single element
API to expression classes.
const exprt & size() const
zero_initializert(const namespacet &_ns, message_handlert &_message_handler)
std::string type2c(const typet &type, const namespacet &ns)
const exprt & size() const
vector constructor from list of elements
std::size_t get_width() const
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
unsigned integer2unsigned(const mp_integer &n)
exprt zero_initializer_rec(const typet &type, const source_locationt &source_location)
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a generic typet to a union_tag_typet.
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a generic typet to a union_tag_typet.
Base class for all expressions.
std::string expr2c(const exprt &expr, const namespacet &ns)
void set_component_name(const irep_idt &component_name)
source_locationt & add_source_location()
const complex_typet & to_complex_type(const typet &type)
Cast a generic typet to a complex_typet.
const typet & subtype() const
const vector_typet & to_vector_type(const typet &type)
Cast a generic typet to a vector_typet.
array constructor from list of elements
complex constructor from a pair of numbers
void set(const irep_namet &name, const irep_idt &value)
exprt operator()(const typet &type, const source_locationt &source_location)
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.