33 const std::size_t new_width = numeric_cast_v<std::size_t>(
power(2, bits));
35 const bool need_typecast =
36 new_width > *x_width || x.
type().
id() != ID_unsignedbv;
42 for(std::size_t shift = 1; shift < new_width; shift <<= 1)
49 std::string bitstring;
50 bitstring.reserve(new_width);
51 for(std::size_t i = 0; i < new_width / (2 * shift); ++i)
52 bitstring += std::string(shift,
'0') + std::string(shift,
'1');
API to expression classes for bitvectors.
A constant literal expression.
Base class for all expressions.
typet & type()
Return the type of the expression.
const irep_idt & id() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
The plus expression Associativity is not specified.
The popcount (counting the number of bits set to 1) expression.
Semantic type conversion.
Fixed-width bit-vector with unsigned binary interpretation.
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
exprt lower_popcount(const popcount_exprt &expr, const namespacet &ns)
Lower a popcount_exprt to arithmetic and logic expressions.
#define CHECK_RETURN(CONDITION)
API to expression classes.