19 if(expr.
id()==ID_overflow_plus ||
20 expr.
id()==ID_overflow_minus)
24 "expression " + expr.
id_string() +
" should have two operands");
29 if(bv0.size()!=bv1.size())
36 return expr.
id()==ID_overflow_minus?
40 else if(expr.
id()==ID_overflow_mult)
44 "overflow_mult expression should have two operands");
46 if(operands[0].type().id()!=ID_unsignedbv &&
47 operands[0].type().id()!=ID_signedbv)
58 operands[0].type() == operands[1].type(),
59 "operands of overflow_mult expression shall have same type");
61 std::size_t old_size=bv0.size();
62 std::size_t new_size=old_size*2;
73 bv_overflow.reserve(old_size);
76 for(std::size_t i=old_size; i<
result.size(); i++)
77 bv_overflow.push_back(
result[i]);
84 bv_overflow.reserve(old_size);
88 for(std::size_t i=old_size-1; i<
result.size(); i++)
89 bv_overflow.push_back(
result[i]);
94 return !
prop.
lor(all_one, all_zero);
97 else if(expr.
id() == ID_overflow_shl)
100 operands.size() == 2,
"overflow_shl expression should have two operands");
105 std::size_t old_size = bv0.size();
106 std::size_t new_size = old_size * 2;
118 operands[1].type().id() == ID_unsignedbv ?
163 else if(expr.
id()==ID_overflow_unary_minus)
166 operands.size() == 1,
167 "overflow_unary_minus expression should have one operand");
bvt extension(const bvt &bv, std::size_t new_size, representationt rep)
virtual literalt convert_overflow(const exprt &expr)
virtual literalt lor(literalt a, literalt b)=0
typet & type()
Return the type of the expression.
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
virtual literalt land(literalt a, literalt b)=0
const irep_idt & id() const
literalt overflow_negate(const bvt &op)
literalt rel(const bvt &bv0, irep_idt id, const bvt &bv1, representationt rep)
bvt multiplier(const bvt &op0, const bvt &op1, representationt rep)
std::vector< exprt > operandst
virtual literalt lequal(literalt a, literalt b)=0
bvt shift(const bvt &op, const shiftt shift, std::size_t distance)
literalt const_literal(bool value)
mstreamt & result() const
Base class for all expressions.
virtual literalt convert_rest(const exprt &expr)
const std::string & id_string() const
literalt overflow_sub(const bvt &op0, const bvt &op1, representationt rep)
virtual literalt lselect(literalt a, literalt b, literalt c)=0
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions, goto_programs, exprts, etc.
literalt overflow_add(const bvt &op0, const bvt &op1, representationt rep)
std::vector< literalt > bvt
bvt build_constant(const mp_integer &i, std::size_t width)