Merge branch 'main' of https://github.com/danmar/cppcheck into main
This commit is contained in:
commit
ff7e99fd42
|
@ -1213,6 +1213,10 @@ bool ExprEngine::IntRange::isEqual(DataBase *dataBase, int value) const
|
||||||
} catch (const z3::exception &exception) {
|
} catch (const z3::exception &exception) {
|
||||||
std::cerr << "z3: " << 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
|
||||||
|
} catch (const ExprData::BailoutValueException &) {
|
||||||
|
return true; // Safe option is to return true
|
||||||
|
} catch (const ExprEngineException &) {
|
||||||
|
return true; // Safe option is to return true
|
||||||
}
|
}
|
||||||
#else
|
#else
|
||||||
// The value may or may not be in range
|
// The value may or may not be in range
|
||||||
|
@ -1241,6 +1245,10 @@ bool ExprEngine::IntRange::isGreaterThan(DataBase *dataBase, int value) const
|
||||||
} catch (const z3::exception &exception) {
|
} catch (const z3::exception &exception) {
|
||||||
std::cerr << "z3: " << 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
|
||||||
|
} catch (const ExprData::BailoutValueException &) {
|
||||||
|
return true; // Safe option is to return true
|
||||||
|
} catch (const ExprEngineException &) {
|
||||||
|
return true; // Safe option is to return true
|
||||||
}
|
}
|
||||||
#else
|
#else
|
||||||
// The value may or may not be in range
|
// The value may or may not be in range
|
||||||
|
@ -1269,6 +1277,10 @@ bool ExprEngine::IntRange::isLessThan(DataBase *dataBase, int value) const
|
||||||
} catch (const z3::exception &exception) {
|
} catch (const z3::exception &exception) {
|
||||||
std::cerr << "z3: " << 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
|
||||||
|
} catch (const ExprData::BailoutValueException &) {
|
||||||
|
return true; // Safe option is to return true
|
||||||
|
} catch (const ExprEngineException &) {
|
||||||
|
return true; // Safe option is to return true
|
||||||
}
|
}
|
||||||
#else
|
#else
|
||||||
// The value may or may not be in range
|
// The value may or may not be in range
|
||||||
|
@ -1298,6 +1310,10 @@ bool ExprEngine::FloatRange::isEqual(DataBase *dataBase, int value) const
|
||||||
} catch (const z3::exception &exception) {
|
} catch (const z3::exception &exception) {
|
||||||
std::cerr << "z3: " << 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
|
||||||
|
} catch (const ExprData::BailoutValueException &) {
|
||||||
|
return true; // Safe option is to return true
|
||||||
|
} catch (const ExprEngineException &) {
|
||||||
|
return true; // Safe option is to return true
|
||||||
}
|
}
|
||||||
#else
|
#else
|
||||||
// The value may or may not be in range
|
// The value may or may not be in range
|
||||||
|
@ -1328,6 +1344,10 @@ bool ExprEngine::FloatRange::isGreaterThan(DataBase *dataBase, int value) const
|
||||||
} catch (const z3::exception &exception) {
|
} catch (const z3::exception &exception) {
|
||||||
std::cerr << "z3: " << 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
|
||||||
|
} catch (const ExprData::BailoutValueException &) {
|
||||||
|
return true; // Safe option is to return true
|
||||||
|
} catch (const ExprEngineException &) {
|
||||||
|
return true; // Safe option is to return true
|
||||||
}
|
}
|
||||||
#else
|
#else
|
||||||
// The value may or may not be in range
|
// The value may or may not be in range
|
||||||
|
@ -1358,6 +1378,10 @@ bool ExprEngine::FloatRange::isLessThan(DataBase *dataBase, int value) const
|
||||||
} catch (const z3::exception &exception) {
|
} catch (const z3::exception &exception) {
|
||||||
std::cerr << "z3: " << 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
|
||||||
|
} catch (const ExprData::BailoutValueException &) {
|
||||||
|
return true; // Safe option is to return true
|
||||||
|
} catch (const ExprEngineException &) {
|
||||||
|
return true; // Safe option is to return true
|
||||||
}
|
}
|
||||||
#else
|
#else
|
||||||
// The value may or may not be in range
|
// The value may or may not be in range
|
||||||
|
@ -1369,13 +1393,22 @@ bool ExprEngine::FloatRange::isLessThan(DataBase *dataBase, int value) const
|
||||||
bool ExprEngine::BinOpResult::isEqual(ExprEngine::DataBase *dataBase, int value) const
|
bool ExprEngine::BinOpResult::isEqual(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.addConstraints(solver, dynamic_cast<const Data *>(dataBase));
|
z3::expr e = exprData.getExpr(this);
|
||||||
exprData.addAssertions(solver);
|
exprData.addConstraints(solver, dynamic_cast<const Data *>(dataBase));
|
||||||
solver.add(exprData.int_expr(e) == value);
|
exprData.addAssertions(solver);
|
||||||
return solver.check() == z3::sat;
|
solver.add(exprData.int_expr(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
|
||||||
|
} catch (const ExprData::BailoutValueException &) {
|
||||||
|
return true; // Safe option is to return true
|
||||||
|
} catch (const ExprEngineException &) {
|
||||||
|
return true; // Safe option is to return true
|
||||||
|
}
|
||||||
#else
|
#else
|
||||||
(void)dataBase;
|
(void)dataBase;
|
||||||
(void)value;
|
(void)value;
|
||||||
|
@ -1397,6 +1430,10 @@ bool ExprEngine::BinOpResult::isGreaterThan(ExprEngine::DataBase *dataBase, int
|
||||||
} catch (const z3::exception &exception) {
|
} catch (const z3::exception &exception) {
|
||||||
std::cerr << "z3:" << 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
|
||||||
|
} catch (const ExprData::BailoutValueException &) {
|
||||||
|
return true; // Safe option is to return true
|
||||||
|
} catch (const ExprEngineException &) {
|
||||||
|
return true; // Safe option is to return true
|
||||||
}
|
}
|
||||||
#else
|
#else
|
||||||
(void)dataBase;
|
(void)dataBase;
|
||||||
|
@ -1419,6 +1456,10 @@ bool ExprEngine::BinOpResult::isLessThan(ExprEngine::DataBase *dataBase, int val
|
||||||
} catch (const z3::exception &exception) {
|
} catch (const z3::exception &exception) {
|
||||||
std::cerr << "z3:" << 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
|
||||||
|
} catch (const ExprData::BailoutValueException &) {
|
||||||
|
return true; // Safe option is to return true
|
||||||
|
} catch (const ExprEngineException &) {
|
||||||
|
return true; // Safe option is to return true
|
||||||
}
|
}
|
||||||
#else
|
#else
|
||||||
(void)dataBase;
|
(void)dataBase;
|
||||||
|
@ -1441,6 +1482,10 @@ bool ExprEngine::BinOpResult::isTrue(ExprEngine::DataBase *dataBase) const
|
||||||
} catch (const z3::exception &exception) {
|
} catch (const z3::exception &exception) {
|
||||||
std::cerr << "z3:" << 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
|
||||||
|
} catch (const ExprData::BailoutValueException &) {
|
||||||
|
return true; // Safe option is to return true
|
||||||
|
} catch (const ExprEngineException &) {
|
||||||
|
return true; // Safe option is to return true
|
||||||
}
|
}
|
||||||
#else
|
#else
|
||||||
(void)dataBase;
|
(void)dataBase;
|
||||||
|
@ -2688,7 +2733,7 @@ void ExprEngine::executeFunction(const Scope *functionScope, ErrorLogger *errorL
|
||||||
|
|
||||||
try {
|
try {
|
||||||
execute(functionScope->bodyStart, functionScope->bodyEnd, data);
|
execute(functionScope->bodyStart, functionScope->bodyEnd, data);
|
||||||
} catch (ExprEngineException &e) {
|
} catch (const ExprEngineException &e) {
|
||||||
if (settings->debugBugHunting)
|
if (settings->debugBugHunting)
|
||||||
report << "ExprEngineException tok.line:" << e.tok->linenr() << " what:" << e.what << "\n";
|
report << "ExprEngineException tok.line:" << e.tok->linenr() << " what:" << e.what << "\n";
|
||||||
trackExecution.setAbortLine(e.tok->linenr());
|
trackExecution.setAbortLine(e.tok->linenr());
|
||||||
|
|
Loading…
Reference in New Issue