100 std::string value(width,
'0');
140 value.add_source_location()=source_location;
141 return std::move(value);
160 return std::move(value);
169 value.add_source_location()=source_location;
170 return std::move(value);
190 value.add_source_location()=source_location;
192 return std::move(value);
201 value.
operands().reserve(components.size());
203 for(
const auto &
c : components)
206 c.type().id() !=
ID_code,
"struct member must not be of code type");
210 if(!member.has_value())
213 value.add_to_operands(std::move(*member));
216 value.add_source_location()=source_location;
218 return std::move(value);
228 return std::move(value);
244 return std::move(value);
251 if(!result.has_value())
255 result->type() = type;
264 if(!result.has_value())
268 result->type() = type;
277 if(!result.has_value())
281 result->type() = type;
444 for(
size_t i = 1; i < size; ++i)
451 values.size() == 1 ? values[0]
API to expression classes for bitvectors.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
byte_extract_exprt make_byte_extract(const exprt &_op, const exprt &_offset, const typet &_type)
Construct a byte_extract_exprt with endianness and byte width matching the current configuration.
Expression classes for byte-level operators.
bitvector_typet char_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.
Complex constructor from a pair of numbers.
struct configt::ansi_ct ansi_c
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).
std::optional< exprt > expr_initializer_rec(const typet &type, const source_locationt &source_location, const exprt &init_expr)
expr_initializert(const namespacet &_ns)
std::optional< exprt > operator()(const typet &type, const source_locationt &source_location, const exprt &init_expr)
Base class for all expressions.
std::vector< exprt > operandst
typet & type()
Return the type of the expression.
source_locationt & add_source_location()
const irep_idt & id() const
A base class for multi-ary expressions Associativity is not specified.
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.
std::vector< componentt > componentst
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
source_locationt & add_source_location()
Union constructor from single element.
Fixed-width bit-vector with unsigned binary interpretation.
Vector constructor from list of elements.
exprt duplicate_per_byte(const exprt &init_byte_expr, const typet &output_type, const namespacet &ns)
Builds an expression of the given output type with each of its bytes initialized to the given initial...
std::optional< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
static exprt cast_or_reinterpret(const exprt &expr, const typet &out_type)
Typecast the input to the output if this is a signed/unsigned bv.
std::optional< exprt > expr_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns, const exprt &init_byte_expr)
Create a value for type type, with all subtype bytes initialized to the given value.
std::optional< 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
exprt simplify_expr(exprt src, const namespacet &ns)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
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.