68 dest.insert(dest.end(), src.begin(), src.end());
71 for(std::size_t i = src.size(); i <
dest_width; i++)
80 lower.assign(src.begin(), src.begin() + src.size() / 2);
81 upper.assign(src.begin() + src.size() / 2, src.end());
94 "lower result bitvector size plus upper result bitvector size shall "
95 "equal the destination bitvector size");
106 "destination type shall be of complex type when source type is of "
117 tmp_src.resize(src.size() / 2);
136 for(std::size_t i = 0; i < dest.size(); i++)
213 src_width == 1,
"bitvector of type boolean shall have width one");
314 src_width == 1,
"bitvector of type boolean shall have width one");
319 dest.push_back(src[0]);
378 bool sign_extension =
384 dest.push_back(src[i]);
385 else if(sign_extension)
419 dest.push_back(src.back());
441 src_width == 1,
"bitvector of type boolean shall have width one");
446 dest.push_back(src[0]);
462 for(std::size_t i = 0, j = 0; i <
dest_width; i += 2, j++)
465 dest.push_back(src[j]);
476 for(std::size_t i = 0, j = 0; i <
dest_width; i += 2, j++)
479 dest.push_back(src[j]);
481 dest.push_back(src.back());
562 typedef std::map<irep_idt, std::size_t>
op_mapt;
565 for(std::size_t i = 0; i <
op_comp.size(); i++)
569 for(std::size_t i = 0; i <
dest_comp.size(); i++)
622 else if(
from == 0 &&
to == 0)
Pre-defined bitvector types.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
bvtypet get_bvtype(const typet &type)
typet c_bit_field_replacement_type(const c_bit_field_typet &src, const namespacet &ns)
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
offset_mapt build_offset_map(const struct_typet &src)
virtual literalt convert_typecast(const typecast_exprt &expr)
conversion from bitvector types to boolean
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
virtual bvt convert_bv_typecast(const typecast_exprt &expr)
bool type_conversion(const typet &src_type, const bvt &src, const typet &dest_type, bvt &dest)
std::vector< std::size_t > offset_mapt
bvt add(const bvt &op0, const bvt &op1)
static bvt zero_extension(const bvt &bv, std::size_t new_size)
static bvt build_constant(const mp_integer &i, std::size_t width)
literalt is_zero(const bvt &op)
bvt incrementer(const bvt &op, literalt carry_in)
Base class for all expressions.
typet & type()
Return the type of the expression.
constant_exprt to_expr() const
void from_integer(const mp_integer &i)
virtual literalt convert_rest(const exprt &expr)
virtual literalt land(literalt a, literalt b)=0
virtual literalt new_variable()=0
virtual literalt lor(literalt a, literalt b)=0
Structure type, corresponds to C style structs.
std::vector< componentt > componentst
Semantic type conversion.
The type of an expression, extends irept.
std::vector< literalt > bvt
literalt const_literal(bool value)
const mp_integer string2integer(const std::string &n, unsigned base)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
const range_typet & to_range_type(const typet &type)
Cast a typet to a range_typet.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.