90 std::string value(width,
'0');
106 expr_initializer_rec(
to_complex_type(type).subtype(), source_location);
126 value.add_source_location()=source_location;
127 return std::move(value);
132 expr_initializer_rec(
array_type.element_type(), source_location);
146 return std::move(value);
155 value.add_source_location()=source_location;
156 return std::move(value);
164 expr_initializer_rec(
vector_type.element_type(), source_location);
176 value.add_source_location()=source_location;
178 return std::move(value);
187 value.
operands().reserve(components.size());
189 for(
const auto &
c : components)
194 code_value.add_source_location()=source_location;
199 const auto member = expr_initializer_rec(
c.type(), source_location);
200 if(!member.has_value())
203 value.add_to_operands(std::move(*member));
207 value.add_source_location()=source_location;
209 return std::move(value);
219 return std::move(value);
227 expr_initializer_rec(
widest_member->first.type(), source_location);
235 return std::move(value);
239 auto result = expr_initializer_rec(
242 if(!result.has_value())
246 result->type() = type;
252 auto result = expr_initializer_rec(
255 if(!result.has_value())
259 result->type() = type;
265 auto result = expr_initializer_rec(
268 if(!result.has_value())
272 result->type() = type;
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
unsignedbv_typet size_type()
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Array constructor from list of elements.
const array_typet & type() const
Array constructor from single element.
const exprt & size() const
std::size_t get_width() const
Complex constructor from a pair of numbers.
A constant literal expression.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Union constructor to support unions without any member (a GCC/Clang feature).
optionalt< exprt > expr_initializer_rec(const typet &type, const source_locationt &source_location)
optionalt< exprt > operator()(const typet &type, const source_locationt &source_location)
expr_initializert(const namespacet &_ns)
Base class for all expressions.
source_locationt & add_source_location()
const irep_idt & id() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
A side_effect_exprt that returns a non-deterministically chosen value.
Struct constructor from list of elements.
const componentst & components() const
std::vector< componentt > componentst
The type of an expression, extends irept.
source_locationt & add_source_location()
Union constructor from single element.
Vector constructor from list of elements.
optionalt< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
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...
Expression Initialization.
Magic numbers used throughout the codebase.
const std::size_t MAX_FLATTENED_ARRAY_SIZE
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.