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

ExprEngine: Catch z3::exception and print message

This commit is contained in:
Daniel Marjamäki 2019-10-09 09:42:00 +02:00
parent 1df97ac5c8
commit ab6354754f
1 changed files with 27 additions and 17 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

44
lib/exprengine.cpp
View File

@ -623,7 +623,7 @@ bool ExprEngine::IntRange::isEqual(DataBase *dataBase, int value) const
solver.add(e == value); solver.add(e == value);
return solver.check() == z3::sat; return solver.check() == z3::sat;
} catch (const z3::exception &exception) { } catch (const z3::exception &exception) {
//std::cout << exception << std::endl; std::cerr << "z3: " << exception << std::endl;
return true; // Safe option is to return true return true; // Safe option is to return true
} }
#else #else
@ -653,14 +653,19 @@ bool ExprEngine::BinOpResult::isEqual(ExprEngine::DataBase *dataBase, int value)
bool ExprEngine::BinOpResult::isGreaterThan(ExprEngine::DataBase *dataBase, int value) const bool ExprEngine::BinOpResult::isGreaterThan(ExprEngine::DataBase *dataBase, int value) const
{ {
#ifdef USE_Z3 #ifdef USE_Z3
ExprData exprData; try {
z3::solver solver(exprData.context); ExprData exprData;
z3::expr e = exprData.getExpr(this); z3::solver solver(exprData.context);
exprData.addAssertions(solver); z3::expr e = exprData.getExpr(this);
for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints) exprData.addAssertions(solver);
solver.add(exprData.getConstraintExpr(constraint)); for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
solver.add(e > value); solver.add(exprData.getConstraintExpr(constraint));
return solver.check() == z3::sat; solver.add(e > value);
return solver.check() == z3::sat;
} catch (const z3::exception &exception) {
std::cerr << "z3:" << exception << std::endl;
return true; // Safe option is to return true
}
#else #else
(void)dataBase; (void)dataBase;
(void)value; (void)value;
@ -671,14 +676,19 @@ bool ExprEngine::BinOpResult::isGreaterThan(ExprEngine::DataBase *dataBase, int
bool ExprEngine::BinOpResult::isLessThan(ExprEngine::DataBase *dataBase, int value) const bool ExprEngine::BinOpResult::isLessThan(ExprEngine::DataBase *dataBase, int value) const
{ {
#ifdef USE_Z3 #ifdef USE_Z3
ExprData exprData; try {
z3::solver solver(exprData.context); ExprData exprData;
z3::expr e = exprData.getExpr(this); z3::solver solver(exprData.context);
exprData.addAssertions(solver); z3::expr e = exprData.getExpr(this);
for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints) exprData.addAssertions(solver);
solver.add(exprData.getConstraintExpr(constraint)); for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
solver.add(e < value); solver.add(exprData.getConstraintExpr(constraint));
return solver.check() == z3::sat; solver.add(e < value);
return solver.check() == z3::sat;
} catch (const z3::exception &exception) {
std::cerr << "z3:" << exception << std::endl;
return true; // Safe option is to return true
}
#else #else
(void)dataBase; (void)dataBase;
(void)value; (void)value;