ExprEngine: << and >> are not handled well, throw exception for now.
This commit is contained in:
parent
c7a56529bb
commit
4e49b14721
|
@ -548,11 +548,7 @@ struct ExprData {
|
||||||
return bool_expr(op1) && bool_expr(op2);
|
return bool_expr(op1) && bool_expr(op2);
|
||||||
if (b->binop == "||")
|
if (b->binop == "||")
|
||||||
return bool_expr(op1) || bool_expr(op2);
|
return bool_expr(op1) || bool_expr(op2);
|
||||||
if (b->binop == "<<")
|
throw VerifyException(nullptr, "Internal error: Unhandled operator " + b->binop);
|
||||||
return z3::shl(op1, op2);
|
|
||||||
if (b->binop == ">>")
|
|
||||||
return z3::lshr(op1, op2);
|
|
||||||
throw VerifyException(nullptr, "Internal error: Unhandled operator");
|
|
||||||
}
|
}
|
||||||
|
|
||||||
z3::expr getExpr(ExprEngine::ValuePtr v) {
|
z3::expr getExpr(ExprEngine::ValuePtr v) {
|
||||||
|
|
Loading…
Reference in New Issue