20 if(expr.
id()==ID_overflow_plus ||
21 expr.
id()==ID_overflow_minus)
23 if(operands.size()!=2)
24 throw "operator "+expr.
id_string()+
" takes two operands";
29 if(bv0.size()!=bv1.size())
36 return expr.
id()==ID_overflow_minus?
40 else if(expr.
id()==ID_overflow_mult)
42 if(operands.size()!=2)
43 throw "operator "+expr.
id_string()+
" takes two operands";
45 if(operands[0].type().
id()!=ID_unsignedbv &&
46 operands[0].type().
id()!=ID_signedbv)
52 if(bv0.size()!=bv1.size())
53 throw "operand size mismatch on overflow-*";
59 if(operands[0].type()!=operands[1].type())
60 throw "operand type mismatch on overflow-*";
62 assert(bv0.size()==bv1.size());
63 std::size_t old_size=bv0.size();
64 std::size_t new_size=old_size*2;
75 bv_overflow.reserve(old_size);
78 for(std::size_t i=old_size; i<
result.size(); i++)
79 bv_overflow.push_back(
result[i]);
86 bv_overflow.reserve(old_size);
90 for(std::size_t i=old_size-1; i<
result.size(); i++)
91 bv_overflow.push_back(
result[i]);
96 return !
prop.
lor(all_one, all_zero);
99 else if(expr.
id()==ID_overflow_unary_minus)
101 if(operands.size()!=1)
102 throw "operator "+expr.
id_string()+
" takes one operand";
114 if(operands.size()!=1)
115 throw "operator "+expr.
id_string()+
" takes one operand";
117 const exprt &op=operands[0];
121 if(bits>=bv.size() || bits==0)
122 throw "overflow-typecast got wrong number of bits";
125 if(op.
type().
id()==ID_signedbv)
128 for(std::size_t i=bits; i<bv.size(); i++)
129 tmp_bv.push_back(
prop.
lxor(bv[bits-1], bv[i]));
136 for(std::size_t i=bits; i<bv.size(); i++)
137 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)
virtual literalt lxor(literalt a, literalt b)=0
bvt multiplier(const bvt &op0, const bvt &op1, representationt rep)
std::vector< exprt > operandst
bool has_prefix(const std::string &s, const std::string &prefix)
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)
literalt overflow_add(const bvt &op0, const bvt &op1, representationt rep)
std::vector< literalt > bvt