23 auto const maybe_upper_as_int = numeric_cast<mp_integer>(expr.
upper());
24 auto const maybe_lower_as_int = numeric_cast<mp_integer>(expr.
lower());
28 if(!maybe_upper_as_int.has_value() || !maybe_lower_as_int.has_value())
31 auto upper_as_int = maybe_upper_as_int.value();
32 auto lower_as_int = maybe_lower_as_int.value();
35 upper_as_int >= 0 && upper_as_int < src_bv.size(),
36 "upper end of extracted bits must be within the bitvector",
41 lower_as_int >= 0 && lower_as_int < src_bv.size(),
42 "lower end of extracted bits must be within the bitvector",
47 lower_as_int <= upper_as_int,
48 "upper bound must be greater or equal to lower bound");
53 (upper_as_int - lower_as_int + 1) ==
bv_width,
54 "the difference between upper and lower end of the range must have the "
55 "same width as the resulting bitvector type",
59 const std::size_t offset = numeric_cast_v<std::size_t>(lower_as_int);
61 bvt result_bv(src_bv.begin() + offset, src_bv.begin() + offset +
bv_width);