15 if(expr.
id()==ID_overflow_plus ||
16 expr.
id()==ID_overflow_minus)
23 if(bv0.size()!=bv1.size())
27 overflow_expr.lhs().type().id() == ID_signedbv
31 return expr.
id()==ID_overflow_minus?
35 else if(expr.
id()==ID_overflow_mult)
40 overflow_expr.lhs().type().id() != ID_unsignedbv &&
41 overflow_expr.lhs().type().id() != ID_signedbv)
48 overflow_expr.lhs().type().id() == ID_signedbv
53 overflow_expr.lhs().type() == overflow_expr.rhs().type(),
54 "operands of overflow_mult expression shall have same type");
56 std::size_t old_size=bv0.size();
57 std::size_t new_size=old_size*2;
68 bv_overflow.reserve(old_size);
71 for(std::size_t i=old_size; i<result.size(); i++)
72 bv_overflow.push_back(result[i]);
79 bv_overflow.reserve(old_size);
83 for(std::size_t i=old_size-1; i<result.size(); i++)
84 bv_overflow.push_back(result[i]);
89 return !
prop.
lor(all_one, all_zero);
92 else if(expr.
id() == ID_overflow_shl)
99 std::size_t old_size = bv0.size();
100 std::size_t new_size = old_size * 2;
103 overflow_expr.lhs().type().id() == ID_signedbv
112 literalt neg_shift = overflow_expr.lhs().type().id() == ID_unsignedbv
131 result.erase(result.begin(), result.begin() + old_size);
140 result.erase(result.begin(), result.begin() + old_size - 1);
157 else if(expr.
id()==ID_overflow_unary_minus)
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...
virtual literalt convert_overflow(const exprt &expr)
static bvt build_constant(const mp_integer &i, std::size_t width)
literalt overflow_add(const bvt &op0, const bvt &op1, representationt rep)
literalt overflow_sub(const bvt &op0, const bvt &op1, representationt rep)
static bvt shift(const bvt &op, const shiftt shift, std::size_t distance)
literalt overflow_negate(const bvt &op)
bvt multiplier(const bvt &op0, const bvt &op1, representationt rep)
static bvt extension(const bvt &bv, std::size_t new_size, representationt rep)
literalt rel(const bvt &bv0, irep_idt id, const bvt &bv1, representationt rep)
Base class for all expressions.
const irep_idt & id() const
virtual literalt convert_rest(const exprt &expr)
virtual literalt land(literalt a, literalt b)=0
virtual literalt lselect(literalt a, literalt b, literalt c)=0
virtual literalt lequal(literalt a, literalt b)=0
virtual literalt lor(literalt a, literalt b)=0
std::vector< literalt > bvt
literalt const_literal(bool value)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.