33 "upper end of extracted bits must be within the bitvector",
39 "lower end of extracted bits must be within the bitvector",
45 "upper bound must be greater or equal to lower bound");
51 "the difference between upper and lower end of the range must have the "
52 "same width as the resulting bitvector type",
API to expression classes for bitvectors.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
virtual bvt convert_extractbits(const extractbits_exprt &expr)
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width={})
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
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,...)