25 template <
bool nondet>
52 template <
bool nondet>
59 if(type_id==ID_unsignedbv ||
60 type_id==ID_signedbv ||
61 type_id==ID_pointer ||
63 type_id==ID_incomplete_c_enum ||
64 type_id==ID_c_bit_field ||
67 type_id==ID_floatbv ||
79 else if(type_id==ID_rational ||
91 else if(type_id==ID_verilog_signedbv ||
92 type_id==ID_verilog_unsignedbv)
100 std::string value(width,
'0');
108 else if(type_id==ID_complex)
115 exprt sub_zero = expr_initializer_rec(type.
subtype(), source_location);
122 else if(type_id==ID_code)
125 error() <<
"cannot initialize code-type" << eom;
128 else if(type_id==ID_array)
137 value.
type().
id(ID_array);
145 expr_initializer_rec(array_type.
subtype(), source_location);
149 if(array_type.
size().
id()==ID_infinity)
172 error() <<
"failed to zero-initialize array of non-fixed size `" 178 array_size >= 0,
"array should not have negative size");
186 else if(type_id==ID_vector)
190 exprt tmpval = expr_initializer_rec(vector_type.
subtype(), source_location);
204 error() <<
"failed to zero-initialize vector of non-fixed size `" 210 vector_size >= 0,
"vector should not have negative size");
218 else if(type_id==ID_struct)
225 value.
operands().reserve(components.size());
227 for(struct_typet::componentst::const_iterator
228 it=components.begin();
229 it!=components.end();
232 if(it->type().id()==ID_code)
240 expr_initializer_rec(it->type(), source_location));
247 else if(type_id==ID_union)
260 for(struct_typet::componentst::const_iterator
261 it=components.begin();
262 it!=components.end();
266 if(it->type().id()==ID_code)
271 if(bits>component_size)
290 expr_initializer_rec(component.
type(), source_location);
295 else if(type_id==ID_symbol)
297 exprt result = expr_initializer_rec(ns.follow(type), source_location);
299 if(ns.follow(type).id()!=ID_array)
304 else if(type_id==ID_c_enum_tag)
307 expr_initializer_rec(
311 else if(type_id==ID_struct_tag)
314 expr_initializer_rec(
318 else if(type_id==ID_union_tag)
321 expr_initializer_rec(
325 else if(type_id==ID_string)
339 error() <<
"failed to initialize `" <<
format(type) <<
"'" << eom;
351 return z_i(type, source_location);
361 return z_i(type, source_location);
369 std::ostringstream oss;
375 return z_i(type, source_location);
388 std::ostringstream oss;
394 return z_i(type, source_location);
const irep_idt & get_name() const
The type of an expression.
exprt nondet_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns, message_handlert &message_handler)
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.
exprt expr_initializer_rec(const typet &type, const source_locationt &source_location)
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.
Expression Initialization.
const irep_idt & id() const
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a generic typet to a union_tag_typet.
A constant-size array type.
union constructor from single element
API to expression classes.
const exprt & size() const
A side effect that returns a non-deterministically chosen value.
const vector_typet & to_vector_type(const typet &type)
Cast a generic typet to a vector_typet.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a generic typet to a union_tag_typet.
const exprt & size() const
array constructor from single element
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
vector constructor from list of elements
exprt operator()(const typet &type, const source_locationt &source_location)
std::size_t get_width() const
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a generic typet to a c_enum_tag_typet.
exprt zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns, message_handlert &message_handler)
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Base class for all expressions.
expr_initializert(const namespacet &_ns, message_handlert &_message_handler)
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
const source_locationt & source_location() const
const complex_typet & to_complex_type(const typet &type)
Cast a generic typet to a complex_typet.
void set_component_name(const irep_idt &component_name)
source_locationt & add_source_location()
goto_programt coverage_criteriont message_handlert & message_handler
std::size_t integer2size_t(const mp_integer &n)
const typet & subtype() const
#define DATA_INVARIANT(CONDITION, REASON)
struct constructor from list of elements
array constructor from list of elements
complex constructor from a pair of numbers
void set(const irep_namet &name, const irep_idt &value)