Go to the documentation of this file.
21 template <
bool nondet>
43 template <
bool nondet>
50 if(type_id==ID_unsignedbv ||
51 type_id==ID_signedbv ||
52 type_id==ID_pointer ||
54 type_id==ID_c_bit_field ||
57 type_id==ID_floatbv ||
69 else if(type_id==ID_rational ||
81 else if(type_id==ID_verilog_signedbv ||
82 type_id==ID_verilog_unsignedbv)
90 std::string value(width,
'0');
98 else if(type_id==ID_complex)
106 expr_initializer_rec(
to_complex_type(type).subtype(), source_location);
107 if(!sub_zero.has_value())
116 else if(type_id==ID_array)
126 value.add_source_location()=source_location;
127 return std::move(value);
131 auto tmpval = expr_initializer_rec(array_type.
subtype(), source_location);
132 if(!tmpval.has_value())
135 const auto array_size = numeric_cast<mp_integer>(array_type.
size());
137 array_type.
size().
id() == ID_infinity || !array_size.has_value() ||
145 return std::move(value);
153 numeric_cast_v<std::size_t>(*array_size), *tmpval);
154 value.add_source_location()=source_location;
155 return std::move(value);
158 else if(type_id==ID_vector)
162 auto tmpval = expr_initializer_rec(vector_type.
subtype(), source_location);
163 if(!tmpval.has_value())
167 numeric_cast_v<mp_integer>(vector_type.
size());
173 value.
operands().resize(numeric_cast_v<std::size_t>(vector_size), *tmpval);
174 value.add_source_location()=source_location;
176 return std::move(value);
178 else if(type_id==ID_struct)
185 value.
operands().reserve(components.size());
187 for(
const auto &c : components)
189 if(c.type().id() == ID_code)
193 value.add_to_operands(std::move(code_value));
197 const auto member = expr_initializer_rec(c.type(), source_location);
198 if(!member.has_value())
201 value.add_to_operands(std::move(*member));
205 value.add_source_location()=source_location;
207 return std::move(value);
209 else if(type_id==ID_union)
220 for(
const auto &c : components)
223 if(c.type().id() == ID_code)
228 if(bits.has_value() && *bits > component_size)
232 component_size = *bits;
241 return std::move(value);
245 auto component_value =
246 expr_initializer_rec(
component.type(), source_location);
248 if(!component_value.has_value())
254 return std::move(value);
257 else if(type_id==ID_c_enum_tag)
259 auto result = expr_initializer_rec(
262 if(!result.has_value())
266 result->type() = type;
270 else if(type_id==ID_struct_tag)
272 auto result = expr_initializer_rec(
275 if(!result.has_value())
279 result->type() = type;
283 else if(type_id==ID_union_tag)
285 auto result = expr_initializer_rec(
288 if(!result.has_value())
292 result->type() = type;
296 else if(type_id==ID_string)
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
const componentst & components() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_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 bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
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.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
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)
source_locationt & add_source_location()
unsignedbv_typet size_type()
A constant literal expression.
Array constructor from list of elements.