Go to the documentation of this file.
24 op_bv.size() <= width,
25 "operand bitvector width shall not be larger than the width indicated by "
33 for(std::size_t i=0; i<op_bv.size(); i++)
37 for(std::size_t i=op_bv.size(); i<bv.size(); i++)
44 "endianness should be set to either little endian or big endian");
49 for(std::size_t i=0; i<op_bv.size(); i++)
53 for(std::size_t i=op_bv.size(); i<bv.size(); i++)
std::vector< literalt > bvt
Union constructor from single element.
virtual literalt new_variable()=0
virtual bvt convert_union(const union_exprt &expr)
struct configt::ansi_ct ansi_c
typet & type()
Return the type of the expression.
void conversion_failed(const exprt &expr, bvt &bv)
virtual std::size_t boolbv_width(const typet &type) const
size_t map_bit(size_t bit) const
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
Maps a big-endian offset to a little-endian offset.
virtual endianness_mapt endianness_map(const typet &type, bool little_endian) const
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.