walkero
/
cppcheck
1
0
Fork 0
Code Issues Pull Requests Projects Releases 1 Wiki Activity

ExprEngine: Quick hacks for old Z3 compatibility

This commit is contained in:
Daniel Marjamäki 2020-01-15 19:46:00 +01:00
parent 52d72b6ffc
commit 9507fccfc1
1 changed files with 12 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
lib/exprengine.cpp
View File

@ -599,7 +599,11 @@ struct ExprData {
} }
z3::expr addFloat(const std::string &name) { z3::expr addFloat(const std::string &name) {
#ifdef OLD_Z3
z3::expr e = context.real_val(name.c_str());
#else
z3::expr e = context.fpa_const(name.c_str(), 11, 53); z3::expr e = context.fpa_const(name.c_str(), 11, 53);
#endif
valueExpr.emplace(name, e); valueExpr.emplace(name, e);
return e; return e;
} }
@ -617,7 +621,11 @@ struct ExprData {
if (b->binop == "/") if (b->binop == "/")
return op1 / op2; return op1 / op2;
if (b->binop == "%") if (b->binop == "%")
#ifdef OLD_Z3
return op1;
#else
return op1 % op2; return op1 % op2;
#endif
if (b->binop == "==") if (b->binop == "==")
return int_expr(op1) == int_expr(op2); return int_expr(op1) == int_expr(op2);
if (b->binop == "!=") if (b->binop == "!=")
@ -646,7 +654,11 @@ struct ExprData {
throw VerifyException(nullptr, "Can not solve expressions, operand value is null"); throw VerifyException(nullptr, "Can not solve expressions, operand value is null");
if (auto intRange = std::dynamic_pointer_cast<ExprEngine::IntRange>(v)) { if (auto intRange = std::dynamic_pointer_cast<ExprEngine::IntRange>(v)) {
if (intRange->name[0] != '$') if (intRange->name[0] != '$')
#ifdef OLD_z3
return context.int_val((long long)(intRange->minValue));
#else
return context.int_val(int64_t(intRange->minValue)); return context.int_val(int64_t(intRange->minValue));
#endif
auto it = valueExpr.find(v->name); auto it = valueExpr.find(v->name);
if (it != valueExpr.end()) if (it != valueExpr.end())
return it->second; return it->second;