Go to the documentation of this file.
22 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_c_bit_field ||
58 type_id==ID_floatbv ||
70 else if(type_id==ID_rational ||
82 else if(type_id==ID_verilog_signedbv ||
83 type_id==ID_verilog_unsignedbv)
91 std::string value(width,
'0');
99 else if(type_id==ID_complex)
107 expr_initializer_rec(
to_complex_type(type).subtype(), source_location);
108 if(!sub_zero.has_value())
117 else if(type_id==ID_array)
127 value.add_source_location()=source_location;
128 return std::move(value);
132 auto tmpval = expr_initializer_rec(array_type.
subtype(), source_location);
133 if(!tmpval.has_value())
136 const auto array_size = numeric_cast<mp_integer>(array_type.
size());
138 array_type.
size().
id() == ID_infinity || !array_size.has_value() ||
146 return std::move(value);
154 numeric_cast_v<std::size_t>(*array_size), *tmpval);
155 value.add_source_location()=source_location;
156 return std::move(value);
159 else if(type_id==ID_vector)
163 auto tmpval = expr_initializer_rec(vector_type.
subtype(), source_location);
164 if(!tmpval.has_value())
168 numeric_cast_v<mp_integer>(vector_type.
size());
174 value.
operands().resize(numeric_cast_v<std::size_t>(vector_size), *tmpval);
175 value.add_source_location()=source_location;
177 return std::move(value);
179 else if(type_id==ID_struct)
186 value.
operands().reserve(components.size());
188 for(
const auto &c : components)
190 if(c.type().id() == ID_code)
194 value.add_to_operands(std::move(code_value));
198 const auto member = expr_initializer_rec(c.type(), source_location);
199 if(!member.has_value())
202 value.add_to_operands(std::move(*member));
206 value.add_source_location()=source_location;
208 return std::move(value);
210 else if(type_id==ID_union)
221 for(
const auto &c : components)
224 if(c.type().id() == ID_code)
229 if(bits.has_value() && *bits > component_size)
233 component_size = *bits;
242 return std::move(value);
246 auto component_value =
247 expr_initializer_rec(
component.type(), source_location);
249 if(!component_value.has_value())
255 return std::move(value);
258 else if(type_id==ID_c_enum_tag)
260 auto result = expr_initializer_rec(
263 if(!result.has_value())
267 result->type() = type;
271 else if(type_id==ID_struct_tag)
273 auto result = expr_initializer_rec(
276 if(!result.has_value())
280 result->type() = type;
284 else if(type_id==ID_union_tag)
286 auto result = expr_initializer_rec(
289 if(!result.has_value())
293 result->type() = type;
297 else if(type_id==ID_string)
const componentst & components() const
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
const typet & subtype() const
optionalt< exprt > operator()(const typet &type, const source_locationt &source_location)
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
The type of an expression, extends irept.
const std::size_t MAX_FLATTENED_ARRAY_SIZE
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...
Union constructor from single element.
Base class for all expressions.
std::vector< componentt > componentst
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Vector constructor from list of elements.
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Magic numbers used throughout the codebase.
optionalt< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
Struct constructor from list of elements.
const exprt & size() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
const array_typet & type() const
Expression Initialization.
Array constructor from single element.
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
expr_initializert(const namespacet &_ns)
const irep_idt & id() const
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Complex constructor from a pair of numbers.
nonstd::optional< T > optionalt
const constant_exprt & size() const
std::size_t get_width() const
A side_effect_exprt that returns a non-deterministically chosen value.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
optionalt< exprt > expr_initializer_rec(const typet &type, const source_locationt &source_location)
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
source_locationt & add_source_location()
unsignedbv_typet size_type()
A constant literal expression.
API to expression classes.
Array constructor from list of elements.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.