69 dest.insert(
dest.end(), src.begin(), src.end());
81 lower.assign(src.begin(), src.begin()+src.size()/2);
82 upper.assign(src.begin()+src.size()/2, src.end());
95 "lower result bitvector size plus upper result bitvector size shall "
96 "equal the destination bitvector size");
107 "destination type shall be of complex type when source type is of "
139 for(std::size_t
i=0;
i<
dest.size();
i++)
196 "source bitvector size shall equal the destination bitvector size");
217 src_width == 1,
"bitvector of type boolean shall have width one");
274 "source bitvector width shall equal the destination bitvector width");
317 src_width == 1,
"bitvector of type boolean shall have width one");
322 dest.push_back(src[0]);
387 dest.push_back(src[
i]);
388 else if(sign_extension)
422 dest.push_back(src.back());
432 "source bitvector width shall equal the destination bitvector width");
444 src_width == 1,
"bitvector of type boolean shall have width one");
449 dest.push_back(src[0]);
467 dest.push_back(src[
j]);
481 dest.push_back(src[
j]);
483 dest.push_back(src.back());
513 "source bitvector width shall equal the destination bitvector width");
566 typedef std::map<irep_idt, std::size_t>
op_mapt;
582 op_mapt::const_iterator it=
629 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.
virtual void clear()
Reset the abstract state.
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=nullopt)
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)
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.
std::size_t get_fraction_bits() const
constant_exprt to_expr() const
void from_integer(const mp_integer &i)
const irep_idt & id() const
const std::string & get_string(const irep_idt &name) const
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
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
mp_integer get_from() const
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.