Go to the documentation of this file.
17 if(expr.
id()==ID_overflow_plus ||
18 expr.
id()==ID_overflow_minus)
25 if(bv0.size()!=bv1.size())
29 overflow_expr.lhs().type().id() == ID_signedbv
33 return expr.
id()==ID_overflow_minus?
37 else if(expr.
id()==ID_overflow_mult)
42 overflow_expr.lhs().type().id() != ID_unsignedbv &&
43 overflow_expr.lhs().type().id() != ID_signedbv)
50 overflow_expr.lhs().type().id() == ID_signedbv
55 overflow_expr.lhs().type() == overflow_expr.rhs().type(),
56 "operands of overflow_mult expression shall have same type");
58 std::size_t old_size=bv0.size();
59 std::size_t new_size=old_size*2;
70 bv_overflow.reserve(old_size);
73 for(std::size_t i=old_size; i<result.size(); i++)
74 bv_overflow.push_back(result[i]);
81 bv_overflow.reserve(old_size);
85 for(std::size_t i=old_size-1; i<result.size(); i++)
86 bv_overflow.push_back(result[i]);
91 return !
prop.
lor(all_one, all_zero);
94 else if(expr.
id() == ID_overflow_shl)
101 std::size_t old_size = bv0.size();
102 std::size_t new_size = old_size * 2;
105 overflow_expr.lhs().type().id() == ID_signedbv
114 literalt neg_shift = overflow_expr.lhs().type().id() == ID_unsignedbv
133 result.erase(result.begin(), result.begin() + old_size);
142 result.erase(result.begin(), result.begin() + old_size - 1);
159 else if(expr.
id()==ID_overflow_unary_minus)
virtual literalt convert_overflow(const exprt &expr)
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
std::vector< literalt > bvt
Base class for all expressions.
virtual literalt lor(literalt a, literalt b)=0
virtual literalt land(literalt a, literalt b)=0
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
bvt shift(const bvt &op, const shiftt shift, std::size_t distance)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
literalt overflow_sub(const bvt &op0, const bvt &op1, representationt rep)
literalt const_literal(bool value)
literalt overflow_add(const bvt &op0, const bvt &op1, representationt rep)
const irep_idt & id() 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...
virtual literalt convert_rest(const exprt &expr)
bvt build_constant(const mp_integer &i, std::size_t width)
virtual literalt lequal(literalt a, literalt b)=0
literalt rel(const bvt &bv0, irep_idt id, const bvt &bv1, representationt rep)
literalt overflow_negate(const bvt &op)
bvt extension(const bvt &bv, std::size_t new_size, representationt rep)
bvt multiplier(const bvt &op0, const bvt &op1, representationt rep)
virtual literalt lselect(literalt a, literalt b, literalt c)=0