19 if(expr.
id()==ID_overflow_plus ||
20 expr.
id()==ID_overflow_minus)
22 if(operands.size()!=2)
23 throw "operator "+expr.
id_string()+
" takes two operands";
28 if(bv0.size()!=bv1.size())
35 return expr.
id()==ID_overflow_minus?
39 else if(expr.
id()==ID_overflow_mult)
41 if(operands.size()!=2)
42 throw "operator "+expr.
id_string()+
" takes two operands";
44 if(operands[0].type().
id()!=ID_unsignedbv &&
45 operands[0].type().
id()!=ID_signedbv)
51 if(bv0.size()!=bv1.size())
52 throw "operand size mismatch on overflow-*";
58 if(operands[0].type()!=operands[1].type())
59 throw "operand type mismatch on overflow-*";
62 std::size_t old_size=bv0.size();
63 std::size_t new_size=old_size*2;
74 bv_overflow.reserve(old_size);
77 for(std::size_t i=old_size; i<
result.size(); i++)
78 bv_overflow.push_back(
result[i]);
85 bv_overflow.reserve(old_size);
89 for(std::size_t i=old_size-1; i<
result.size(); i++)
90 bv_overflow.push_back(
result[i]);
95 return !
prop.
lor(all_one, all_zero);
98 else if(expr.
id() == ID_overflow_shl)
100 if(operands.size() != 2)
101 throw "operator " + expr.
id_string() +
" takes two operands";
106 std::size_t old_size = bv0.size();
107 std::size_t new_size = old_size * 2;
119 operands[1].type().id() == ID_unsignedbv ?
164 else if(expr.
id()==ID_overflow_unary_minus)
166 if(operands.size()!=1)
167 throw "operator "+expr.
id_string()+
" takes one operand";
179 if(operands.size()!=1)
180 throw "operator "+expr.
id_string()+
" takes one operand";
182 const exprt &op=operands[0];
186 if(bits>=bv.size() || bits==0)
187 throw "overflow-typecast got wrong number of bits";
190 if(op.
type().
id()==ID_signedbv)
193 for(std::size_t i=bits; i<bv.size(); i++)
194 tmp_bv.push_back(
prop.
lxor(bv[bits-1], bv[i]));
201 for(std::size_t i=bits; i<bv.size(); i++)
202 tmp_bv.push_back(bv[i]);
bvt extension(const bvt &bv, std::size_t new_size, representationt rep)
const std::string & id2string(const irep_idt &d)
virtual literalt convert_overflow(const exprt &expr)
unsigned unsafe_string2unsigned(const std::string &str, int base)
virtual literalt lor(literalt a, literalt b)=0
virtual literalt land(literalt a, literalt b)=0
const irep_idt & id() const
literalt overflow_negate(const bvt &op)
virtual const bvt & convert_bv(const exprt &expr)
literalt rel(const bvt &bv0, irep_idt id, const bvt &bv1, representationt rep)
virtual literalt lxor(literalt a, literalt b)=0
bvt multiplier(const bvt &op0, const bvt &op1, representationt rep)
bool has_prefix(const std::string &s, const std::string &prefix)
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)
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)