1/*******************************************************************\
5Author: Daniel Kroening, kroening@kroening.com
7\*******************************************************************/
25 const typet &target_type,
38 std::size_t lower_bound,
39 std::size_t upper_bound)
42 result.
lb = lower_bound;
43 result.
ub = upper_bound;
50 // big-endian bounds need swapping
51 if(result.
ub < result.
lb)
52 std::swap(result.
lb, result.
ub);
67 else if(src.
id() ==
ID_c_enum)
// we use the underlying type
87 operands.reserve(components.size());
89 for(
const auto &
comp : components)
135 if(components.empty())
149 components.front().get_name(),
158 : components.front().get_name();
161 : components.front().type();
196 "subtype width times array size should be total bitvector width");
242 "subtype width times vector size should be total bitvector width");
290 "subtype width should be half of the total bitvector width");
332 const typet &target_type,
368 result.
type() = target_type;
369 return std::move(result);
383 result.
type() = target_type;
404 false,
"bv_to_expr does not yet support ", target_type.
id_string());
412 const std::optional<mp_integer> &
max_bytes,
426 std::size_t lower_bound,
427 std::size_t upper_bound,
451 bytes.reserve(upper_bound - lower_bound);
452 for(std::size_t i = lower_bound; i < upper_bound; ++i)
479 // TODO we either need a symbol table here or make array comprehensions
484 "$array_comprehension_index_a_v" +
501 for(std::size_t i = 1; i <
el_bytes; ++i)
515 // The source array/vector has no statically known size (an incomplete
516 // type whose extent is genuinely unknown here, e.g. an extern array
517 // declared without a bound). Represent it as a zero-length comprehension;
518 // any byte access into it is then out of bounds and becomes nondet/fails,
519 // which is the behaviour the extern6 regression exercises.
552 const std::optional<mp_integer> &
src_size,
556 const std::optional<mp_integer> &
max_bytes,
567 "unpacking of arrays with non-byte-aligned elements is not supported");
575 // refine the number of elements to extract in case the element width is known
576 // and a multiple of bytes; otherwise we will expand the entire array/vector
582 // turn bytes into elements, rounding up
588 // compute offset as number of elements
590 // insert offset_bytes-many nil bytes into the output array
599 // the maximum number of bytes is an upper bound in case the size of the
600 // array/vector is unknown; if element_bits was usable above this will
601 // have been turned into a number of elements already
626 // recursively unpack each element so that we eventually just have an array
632 : std::optional<mp_integer>{};
671 const std::optional<mp_integer> &
max_bytes,
689 std::make_move_iterator(sub.
operands().begin()),
690 std::make_move_iterator(sub.
operands().end()));
707 const std::optional<mp_integer> &
max_bytes,
719 std::optional<std::pair<exprt::operandst, std::size_t>>
bit_fields;
723 for(
auto it = components.begin(); it != components.end(); ++it)
725 const auto &
comp = *it;
728 // We can only handle a member of unknown width when it is the last member
729 // and is byte-aligned. Members of unknown width in the middle would leave
730 // us with unknown alignment of subsequent members, and queuing them up as
731 // bit fields is not possible either as the total width of the concatenation
732 // could not be determined.
735 (std::next(it) == components.end() && !
bit_fields.has_value()),
736 "members of non-constant width should come last in a struct");
742 // Is it a byte-aligned member?
762 // if the offset is negative, offset_in_member remains unset, which has
763 // the same effect as setting it to zero
796 "all preceding members should have been processed");
802 // we won't actually need this component, fill in zeros instead of
803 // computing an unpacking
822 std::make_move_iterator(sub.
operands().begin()),
823 std::make_move_iterator(sub.
operands().end()));
830 // any remaining bit fields?
889 std::make_move_iterator(
sub_imag.operands().begin()),
890 std::make_move_iterator(
sub_imag.operands().end()));
914 const std::optional<mp_integer> &
max_bytes,
1049 // a basic type; we turn that into extractbits while considering
1071 // When the source width is not a multiple of the byte size, round up
1072 // to the next byte boundary and zero-extend the source so that all
1073 // byte-sized extractbits operations remain within bounds. The padding
1074 // bits (the high bits of the final partial byte) are unspecified and are
1075 // filled with zero.
1101 // endianness_mapt should be the point of reference for mapping out
1102 // endianness, but we need to work on elements here instead of
1132 const typet &subtype,
1155 tmp.type() = subtype;
1173 // TODO we either need a symbol table here or make array comprehensions
1174 // introduce a scope
1178 "$array_comprehension_index_a" +
1193 body.
type() = subtype;
1222 // offset remains unchanged
1224 real.type() = subtype;
1231 imag.type() = subtype;
1244 // General notes about endianness and the bit-vector conversion:
1245 // A single byte with value 0b10001000 is stored (in irept) as
1246 // exactly this string literal, and its bit-vector encoding will be
1247 // bvt bv={0,0,0,1,0,0,0,1}, i.e., bv[0]==0 and bv[7]==1
1249 // A multi-byte value like x=256 would be:
1250 // - little-endian storage: ((char*)&x)[0]==0, ((char*)&x)[1]==1
1251 // - big-endian storage: ((char*)&x)[0]==1, ((char*)&x)[1]==0
1252 // - irept representation: 0000000100000000
1253 // - bvt: {0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0}
1254 // <... 8bits ...> <... 8bits ...>
1256 // An array {0, 1} will be encoded as bvt bv={0,1}, i.e., bv[1]==1
1257 // concatenation(0, 1) will yield a bvt bv={1,0}, i.e., bv[1]==0
1259 // The semantics of byte_extract(endianness, op, offset, T) is:
1260 // interpret ((char*)&op)+offset as the endianness-ordered storage
1261 // of an object of type T at address ((char*)&op)+offset
1262 // For some T x, byte_extract(endianness, x, 0, T) must yield x.
1264 // byte_extract for a composite type T or an array will interpret
1265 // the individual subtypes with suitable endianness; the overall
1266 // order of components is not affected by endianness.
1269 // unsigned char A[4];
1270 // byte_extract_little_endian(A, 0, unsigned short) requests that
1271 // A[0],A[1] be interpreted as the storage of an unsigned short with
1272 // A[1] being the most-significant byte; byte_extract_big_endian for
1273 // the same operands will select A[0] as the most-significant byte.
1275 // int A[2] = {0x01020304,0xDEADBEEF}
1276 // byte_extract_big_endian(A, 0, short) should yield 0x0102
1277 // byte_extract_little_endian(A, 0, short) should yield 0x0304
1278 // To obtain this we first compute byte arrays while taking into
1279 // account endianness:
1280 // big-endian byte representation: {01,02,03,04,DE,AB,BE,EF}
1281 // little-endian byte representation: {04,03,02,01,EF,BE,AB,DE}
1282 // We extract the relevant bytes starting from ((char*)A)+0:
1283 // big-endian: {01,02}; little-endian: {04,03}
1284 // Finally we place them in the appropriate byte order as indicated
1286 // big-endian: (short)concatenation(01,02)=0x0102
1287 // little-endian: (short)concatenation(03,04)=0x0304
1294 // determine an upper bound of the last byte we might need
1328 // consider ways of dealing with arrays of unknown subtype size or with a
1329 // subtype size that does not fit byte boundaries; currently we fall back to
1330 // stitching together consecutive elements down below
1343 if(result.has_value())
1344 return std::move(*result);
1346 // else fall back to generic lowering that uses bit masks, below
1359 for(
const auto &
comp : components)
1363 // the next member would be misaligned, abort
1420 std::optional<typet> subtype;
1421 std::optional<typet> index_type;
1437 "offset bits are byte aligned");
1443 // all cases with non-constant width should have been handled above
1446 "the extracted width or the source width must be known");
1454 // get 'width'-many bytes, and concatenate
1461 // the most significant byte comes first in the concatenation!
1474 index < root.
operands().size() && index >= 0)
1476 // offset is constant and in range
1490 else // width_bytes>=2
1518 const typet &subtype,
1523 // TODO we either need a symbol table here or make array comprehensions
1524 // introduce a scope
1528 "$array_comprehension_index_u_a_v" +
1555 or_exprt{std::move(lower_bound), std::move(upper_bound)},
1587 const typet &subtype,
1601 // apply 'array-update-with' num_elements times
1614 // skip elements that wouldn't change (skip over typecasts as we might have
1615 // some signed/unsigned char conversions)
1660 const typet &subtype,
1673 // TODO we either need a symbol table here or make array comprehensions
1674 // introduce a scope
1678 "$array_comprehension_index_u_a_v_u" +
1682 // all arithmetic uses offset/index types
1688 // the bound from where updates start
1695 // The actual value of updates other than at the start or end
1713 // The number of target array/vector elements being replaced, not including
1714 // a possible partial update at the end of the updated range, which is handled
1715 // below: (non_const_update_bound + (subtype_size - 1)) / subtype_size to
1716 // round up to the nearest multiple of subtype_size.
1724 // The last element to be updated: first_index + updated_elements - 1
1730 // The size of a partial update at the end of the updated range, may be zero.
1740 // The bound where updates end, which is conditional on the partial update
1751 // The actual value of a partial update at the end.
1764 or_exprt{std::move(lower_bound), std::move(upper_bound)},
1800 const typet &subtype,
1805 // do all arithmetic below using index/offset types - the array theory
1806 // back-end is really picky about indices having the same type
1815 // compute the index of the first element of the array/vector that may be
1822 // compute the offset within that first element
1825 // compute the number of bytes (from the update value) that are going to be
1826 // consumed for updating the first element
1840 "value should be an array expression if the update bound is constant");
1849 // encode the first update: update the original element at first_index (the
1850 // actual update will only be initial_bytes-many bytes from
1851 // value_as_byte_array)
1875 // We will update one array/vector element at a time - compute the number of
1876 // update values that will be consumed in each step. If we cannot determine a
1877 // constant value at this time we assume it's at least one byte. The
1878 // byte_extract_exprt within the loop uses the symbolic value (subtype_size),
1879 // we just need to make sure we make progress for the loop to terminate.
1883 // Given the first update already encoded, keep track of the offset into the
1884 // update value. Again, the expressions within the loop use the symbolic
1885 // value, this is just an optimization in case we can determine a constant
1887 std::size_t offset = 0;
1900 &result](std::size_t i) ->
void {
1919 result =
with_exprt{result, std::move(where), std::move(element)};
1958 // We need to take one or more bytes from value_as_byte_array to modify the
1959 // target element. We need to compute:
1960 // - The position in value_as_byte_array to take bytes from: If subtype_bits
1961 // is less than the size of a byte, then multiple struct/array/vector elements
1962 // will need to be updated using the same byte.
1963 std::size_t first = 0;
1964 // - An upper bound on the number of bytes required from value_as_byte_array.
1967 // - The offset into the target element: If subtype_bits is greater or equal
1968 // to the size of a byte, then there may be an offset into the target element
1969 // that needs to be taken into account, and multiple bytes will be required.
1978 "indices past the update should be handled below");
1991 update_elements > 0,
"indices before the update should be handled above");
2004 // each case below will set "new_value" as appropriate
2071 // With an upper bound on the size of the update established, construct the
2072 // actual update expression. If the exact size of the update is unknown,
2073 // make the size expression conditional.
2086 // The size of the update is not constant, and thus is to be symbolically
2087 // bound; first see how many bytes we have left in the update:
2088 // non_const_update_bound > first ? non_const_update_bound - first: 0
2100 // Now take the minimum of update-bytes-left and the previously computed
2101 // size of the element to be updated:
2125 const typet &subtype,
2145 // fall back to bytewise updates in all non-constant or dubious cases
2164 // copy the prefix not affected by the update
2168 // the modified elements
2172 src.get_bits_per_byte();
2186 // copy the tail not affected by the update
2215 elements.reserve(
struct_type.components().size());
2222 // compute the update offset relative to this struct member - will be
2223 // negative if we are already in the middle of the update or beyond it
2234 // The offset to update is not constant, either because the original
2235 // offset in src never was, or because a struct member has an unknown
2236 // offset. Abort the attempt to update individual struct members and
2237 // instead turn the operand-to-be-updated into a byte array, which we know
2238 // how to update even if the offset is non-constant.
2255 bu.type() =
bu.op().type();
2270 // we don't need to update anything when
2271 // 1) the update offset is greater than the end of this member (thus the
2272 // relative offset is greater than this element) or
2273 // 2) the update offset plus the size of the update is less than the member
2281 elements.push_back(member);
2322 "lower_byte_update of union of unknown size is not supported");
2351 std::optional<typet> subtype;
2365 "constant update bound should yield an array expression");
2414 // mask out the bits to be updated, shift the value according to the
2415 // offset and bit-or
2507 // original_bits &= ~mask
2510 // concatenate and zero-extend the value
2513 std::reverse(value.operands().begin(), value.operands().end());
2522 // Big endian -- the zero is added as LSB.
2545 // original_bits |= newvalue
2568 false,
"lower_byte_update does not yet support ", src.
type().
id_string());
2577 "byte update expression should either be little or big endian");
2579 // An update of a void-typed object or update by a void-typed value is the
2580 // source operand (this is questionable, but may arise when dereferencing
2581 // invalid pointers).
2585 // byte_update lowering proceeds as follows:
2586 // 1) Determine the size of the update, with the size of the object to be
2587 // updated as an upper bound. We fail if neither can be determined.
2588 // 2) Turn the update value into a byte array of the size determined above.
2589 // 3) If the offset is not constant, turn the object into a byte array, and
2590 // use a "with" expression to encode the update; else update the values in
2592 // 4) Construct a new object.
2594 // update value, may require extension to full bytes
2610 // If the following invariant fails, then the type was only found to be
2611 // constant via simplification. Such instances should be fixed at the place
2612 // introducing these constant-but-not-constant_exprt type sizes.
2614 update_bits.has_value(),
"constant size-of should imply fixed bit width");
2621 "non-byte aligned type expected to be a bitvector type");
2669 // destroys any sharing, should use hash table
API to expression classes for bitvectors.
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
const concatenation_exprt & to_concatenation_expr(const exprt &expr)
Cast an exprt to a concatenation_exprt.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Expression classes for byte-level operators.
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_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...
Expression to define a mapping from an argument (index) to elements.
Array constructor from list of elements.
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Bit-wise AND Any number of operands that is greater or equal one.
Bit-wise negation of bit-vectors.
Bit-wise OR Any number of operands that is greater or equal one.
Base class of fixed-width bit-vector types.
constant_exprt all_zeros_expr() const
Fixed-width bit-vector without numerical interpretation.
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
const exprt & offset() const
std::size_t get_bits_per_byte() const
const exprt & value() const
Type for C bit fields These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (...
Complex constructor from a pair of numbers.
Imaginary part of the expression describing a complex number.
Real part of the expression describing a complex number.
Complex numbers made of pair of given subtype.
Concatenation of bit-vector operands.
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).
Maps a big-endian offset to a little-endian offset.
size_t number_of_bits() const
size_t map_bit(size_t bit) const
Base class for all expressions.
std::vector< exprt > operandst
bool is_constant() const
Return whether the expression is a constant.
typet & type()
Return the type of the expression.
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
The trinary if-then-else operator.
const std::string & id_string() const
const irep_idt & id() const
Extract member of struct or union.
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Binary multiplication Associativity is not specified.
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Boolean OR All operands must be boolean, and the result is always boolean.
The plus expression Associativity is not specified.
Fixed-width bit-vector with two's complement interpretation.
Struct constructor from list of elements.
Structure type, corresponds to C style structs.
std::vector< componentt > componentst
Expression to hold a symbol (variable)
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
The unary minus expression.
Union constructor from single element.
Fixed-width bit-vector with unsigned binary interpretation.
Vector constructor from list of elements.
Operator to update elements in structs and arrays.
zero extension The operand is converted to the given type by either a) truncating if the new type is ...
#define Forall_operands(it, expr)
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Deprecated expression utility functions.
static exprt lower_byte_update_union(const byte_update_exprt &src, const union_typet &union_type, const exprt &value_as_byte_array, const std::optional< exprt > &non_const_update_bound, const namespacet &ns)
Apply a byte update src to a union typed operand using the byte array value_as_byte_array as update v...
static exprt lower_byte_update_byte_array_vector(const byte_update_exprt &src, const typet &subtype, const array_exprt &value_as_byte_array, const std::optional< exprt > &non_const_update_bound, const namespacet &ns)
Apply a byte update src to an array/vector of bytes using the byte array value_as_byte_array as updat...
static exprt bv_to_expr(const exprt &bitvector_expr, const typet &target_type, const endianness_mapt &endianness_map, const namespacet &ns)
Convert a bitvector-typed expression bitvector_expr to an expression of type target_type.
static exprt bv_to_union_expr(const exprt &bitvector_expr, const union_typet &union_type, const endianness_mapt &endianness_map, const namespacet &ns)
Convert a bitvector-typed expression bitvector_expr to a union-typed expression.
static complex_exprt bv_to_complex_expr(const exprt &bitvector_expr, const complex_typet &complex_type, const endianness_mapt &endianness_map, const namespacet &ns)
Convert a bitvector-typed expression bitvector_expr to a complex-typed expression.
static array_exprt unpack_struct(const exprt &src, bool little_endian, const std::optional< mp_integer > &offset_bytes, const std::optional< mp_integer > &max_bytes, const std::size_t bits_per_byte, const namespacet &ns)
Rewrite a struct-typed expression into its individual bytes.
static exprt::operandst instantiate_byte_array(const exprt &src, std::size_t lower_bound, std::size_t upper_bound, const std::size_t bits_per_byte, const namespacet &ns)
Build the individual bytes to be used in an update.
exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
rewrite byte extraction from an array to byte extraction from a concatenation of array index expressi...
bitvector_typet adjust_width(const typet &src, std::size_t new_width)
changes the width of the given bitvector type
static vector_exprt bv_to_vector_expr(const exprt &bitvector_expr, const vector_typet &vector_type, const endianness_mapt &endianness_map, const namespacet &ns)
Convert a bitvector-typed expression bitvector_expr to a vector-typed expression.
static void process_bit_fields(exprt::operandst &&bit_fields, std::size_t total_bits, exprt::operandst &dest, bool little_endian, const std::optional< mp_integer > &offset_bytes, const std::optional< mp_integer > &max_bytes, const std::size_t bits_per_byte, const namespacet &ns)
Extract bytes from a sequence of bitvector-typed elements.
static struct_exprt bv_to_struct_expr(const exprt &bitvector_expr, const struct_typet &struct_type, const endianness_mapt &endianness_map, const namespacet &ns)
Convert a bitvector-typed expression bitvector_expr to a struct-typed expression.
static array_exprt unpack_complex(const exprt &src, bool little_endian, const std::size_t bits_per_byte, const namespacet &ns)
Rewrite a complex_exprt into its individual bytes.
static exprt unpack_array_vector_no_known_bounds(const exprt &src, std::size_t el_bytes, bool little_endian, const std::size_t bits_per_byte, const namespacet &ns)
Rewrite an array or vector into its individual bytes when no maximum number of bytes is known.
static exprt lower_byte_update_array_vector(const byte_update_exprt &src, const typet &subtype, const std::optional< mp_integer > &subtype_bits, const exprt &value_as_byte_array, const std::optional< exprt > &non_const_update_bound, const namespacet &ns)
Apply a byte update src to an array/vector typed operand using the byte array value_as_byte_array as ...
static exprt lower_byte_update_array_vector_non_const(const byte_update_exprt &src, const typet &subtype, const exprt &value_as_byte_array, const std::optional< exprt > &non_const_update_bound, const namespacet &ns)
Apply a byte update src to an array/vector typed operand, using the byte array value_as_byte_array as...
static array_exprt bv_to_array_expr(const exprt &bitvector_expr, const array_typet &array_type, const endianness_mapt &endianness_map, const namespacet &ns)
Convert a bitvector-typed expression bitvector_expr to an array-typed expression.
static boundst map_bounds(const endianness_mapt &endianness_map, std::size_t lower_bound, std::size_t upper_bound)
Map bit boundaries according to endianness.
exprt lower_byte_operators(const exprt &src, const namespacet &ns)
Rewrite an expression possibly containing byte-extract or -update expressions to more fundamental ope...
static exprt lower_byte_extract_array_vector(const byte_extract_exprt &src, const byte_extract_exprt &unpacked, const typet &subtype, const mp_integer &element_bits, const namespacet &ns)
Rewrite a byte extraction of an array/vector-typed result to byte extraction of the individual compon...
static exprt lower_byte_update(const byte_update_exprt &src, const exprt &value_as_byte_array, const std::optional< exprt > &non_const_update_bound, const namespacet &ns)
Apply a byte update src using the byte array value_as_byte_array as update value.
static exprt unpack_array_vector(const exprt &src, const std::optional< mp_integer > &src_size, const mp_integer &element_bits, bool little_endian, const std::optional< mp_integer > &offset_bytes, const std::optional< mp_integer > &max_bytes, const std::size_t bits_per_byte, const namespacet &ns)
Rewrite an array or vector into its individual bytes.
static exprt unpack_rec(const exprt &src, bool little_endian, const std::optional< mp_integer > &offset_bytes, const std::optional< mp_integer > &max_bytes, const std::size_t bits_per_byte, const namespacet &ns, bool unpack_byte_array=false)
Rewrite an object into its individual bytes.
static exprt lower_byte_update_struct(const byte_update_exprt &src, const struct_typet &struct_type, const exprt &value_as_byte_array, const std::optional< exprt > &non_const_update_bound, const namespacet &ns)
Apply a byte update src to a struct typed operand using the byte array value_as_byte_array as update ...
static std::optional< exprt > lower_byte_extract_complex(const byte_extract_exprt &src, const byte_extract_exprt &unpacked, const namespacet &ns)
Rewrite a byte extraction of a complex-typed result to byte extraction of the individual components t...
static exprt lower_byte_update_byte_array_vector_non_const(const byte_update_exprt &src, const typet &subtype, const exprt &value_as_byte_array, const exprt &non_const_update_bound, const namespacet &ns)
Apply a byte update src to an array/vector of bytes using the byte-array typed expression value_as_by...
static exprt lower_byte_update_single_element(const byte_update_exprt &src, const mp_integer &offset_bits, const exprt &element_to_update, const mp_integer &subtype_bits, const mp_integer &bits_already_set, const exprt &value_as_byte_array, const std::optional< exprt > &non_const_update_bound, const namespacet &ns)
Byte update a struct/array/vector element.
static exprt lower_byte_update_array_vector_unbounded(const byte_update_exprt &src, const typet &subtype, const exprt &subtype_size, const exprt &value_as_byte_array, const exprt &non_const_update_bound, const exprt &initial_bytes, const exprt &first_index, const exprt &first_update_value, const namespacet &ns)
Apply a byte update src to an array/vector typed operand, using the byte array value_as_byte_array as...
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
std::optional< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
std::optional< mp_integer > member_offset_bits(const struct_typet &type, const irep_idt &member, const namespacet &ns)
std::optional< exprt > size_of_expr(const typet &type, const namespacet &ns)
std::optional< exprt > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
bool simplify(exprt &expr, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
#define CHECK_RETURN(CONDITION)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
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.
const string_constantt & to_string_constant(const exprt &expr)
static bool failed(bool error_indicator)
const type_with_subtypet & to_type_with_subtype(const typet &type)