21 template <
bool nondet>
44 template <
bool nondet>
51 if(type_id==ID_unsignedbv ||
52 type_id==ID_signedbv ||
53 type_id==ID_pointer ||
55 type_id==ID_incomplete_c_enum ||
56 type_id==ID_c_bit_field ||
59 type_id==ID_floatbv ||
71 else if(type_id==ID_rational ||
83 else if(type_id==ID_verilog_signedbv ||
84 type_id==ID_verilog_unsignedbv)
92 std::string value(width,
'0');
100 else if(type_id==ID_complex)
108 expr_initializer_rec(
to_complex_type(type).subtype(), source_location);
118 else if(type_id==ID_array)
127 value.
type().
id(ID_array);
130 return std::move(value);
135 expr_initializer_rec(array_type.
subtype(), source_location);
139 if(array_type.
size().
id()==ID_infinity)
146 return std::move(value);
149 const auto array_size = numeric_cast<mp_integer>(array_type.
size());
150 if(!array_size.has_value())
162 value.
operands().resize(numeric_cast_v<std::size_t>(*array_size), tmpval);
164 return std::move(value);
167 else if(type_id==ID_vector)
171 exprt tmpval = expr_initializer_rec(vector_type.
subtype(), source_location);
176 numeric_cast_v<mp_integer>(vector_type.
size());
182 value.
operands().resize(numeric_cast_v<std::size_t>(vector_size), tmpval);
185 return std::move(value);
187 else if(type_id==ID_struct)
194 value.
operands().reserve(components.size());
196 for(
const auto &c : components)
198 if(c.type().id() == ID_code)
206 const exprt member = expr_initializer_rec(c.type(), source_location);
216 return std::move(value);
218 else if(type_id==ID_union)
231 for(
const auto &c : components)
234 if(c.type().id() == ID_code)
239 if(bits.has_value() && *bits > component_size)
243 component_size = *bits;
258 expr_initializer_rec(
component.type(), source_location);
263 return std::move(value);
265 else if(type_id == ID_symbol_type)
267 exprt result = expr_initializer_rec(ns.follow(type), source_location);
269 if(ns.follow(type).id()!=ID_array)
274 else if(type_id==ID_c_enum_tag)
277 expr_initializer_rec(
281 else if(type_id==ID_struct_tag)
283 exprt result = expr_initializer_rec(
287 result.
type() = type;
291 else if(type_id==ID_union_tag)
293 exprt result = expr_initializer_rec(
297 result.
type() = type;
301 else if(type_id==ID_string)
328 const exprt result = z_i(type, source_location);
348 const exprt result = z_i(type, source_location);
The type of an expression, extends irept.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
optionalt< exprt > nondet_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create a non-deterministic value for type type, with all subtypes independently expanded as non-deter...
exprt expr_initializer_rec(const typet &type, const source_locationt &source_location)
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
expr_initializert(const namespacet &_ns)
std::vector< componentt > componentst
const componentst & components() const
typet & type()
Return the type of the expression.
unsignedbv_typet size_type()
A constant literal expression.
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.
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
nonstd::optional< T > optionalt
Union constructor from single element.
API to expression classes.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
const exprt & size() const
A side_effect_exprt that returns a non-deterministically chosen value.
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 exprt & size() const
Array constructor from single element.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Vector constructor from list of elements.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
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 typet to a c_enum_tag_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Base class for all expressions.
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
void set_component_name(const irep_idt &component_name)
source_locationt & add_source_location()
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
const typet & subtype() const
Struct constructor from list of elements.
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Array constructor from list of elements.
Complex constructor from a pair of numbers.
void set(const irep_namet &name, const irep_idt &value)