20 auto const maybe_upper_as_int = numeric_cast<mp_integer>(expr.
upper());
21 auto const maybe_lower_as_int = numeric_cast<mp_integer>(expr.
lower());
25 if(!maybe_upper_as_int.has_value() || !maybe_lower_as_int.has_value())
28 auto upper_as_int = maybe_upper_as_int.value();
29 auto lower_as_int = maybe_lower_as_int.value();
32 upper_as_int >= 0 && upper_as_int < src_bv.size(),
33 "upper end of extracted bits must be within the bitvector",
38 lower_as_int >= 0 && lower_as_int < src_bv.size(),
39 "lower end of extracted bits must be within the bitvector",
44 lower_as_int <= upper_as_int,
45 "upper bound must be greater or equal to lower bound");
50 (upper_as_int - lower_as_int + 1) ==
bv_width,
51 "the difference between upper and lower end of the range must have the "
52 "same width as the resulting bitvector type",
56 const std::size_t offset = numeric_cast_v<std::size_t>(lower_as_int);
58 bvt result_bv(src_bv.begin() + offset, src_bv.begin() + offset +
bv_width);
API to expression classes for bitvectors.
virtual const bvt & convert_bv(const exprt &expr, const std::optional< std::size_t > expected_width={})
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
virtual bvt convert_extractbits(const extractbits_exprt &expr)
bvt conversion_failed(const exprt &expr)
Print that the expression of x has failed conversion, then return a vector of x's width.
virtual std::size_t boolbv_width(const typet &type) const
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
typet & type()
Return the type of the expression.
std::vector< literalt > bvt
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)