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

ExprEngine: Execute false execution path even if there is no else, upon Z3 exception assume that value is in range (safe option)

This commit is contained in:
Daniel Marjamäki 2019-10-06 18:26:40 +02:00
parent 6c0c9ba6d3
commit 05aae9569b
1 changed files with 13 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

19
lib/exprengine.cpp
View File

@ -594,12 +594,17 @@ bool ExprEngine::IntRange::isIntValueInRange(DataBase *dataBase, int value) cons
// Check the value against the constraints
ExprData exprData;
z3::solver solver(exprData.context);
z3::expr e = exprData.context.int_const(name.c_str());
exprData.valueExpr.emplace(name, e);
for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
solver.add(exprData.getConstraintExpr(constraint));
solver.add(e == value);
return solver.check() == z3::sat;
try {
z3::expr e = exprData.context.int_const(name.c_str());
exprData.valueExpr.emplace(name, e);
for (auto constraint : dynamic_cast<const Data *>(dataBase)->constraints)
solver.add(exprData.getConstraintExpr(constraint));
solver.add(e == value);
return solver.check() == z3::sat;
} catch (const z3::exception &exception) {
//std::cout << exception << std::endl;
return true; // Safe option is to return true
}
#else
// The value may or may not be in range
return false;
@ -1093,6 +1098,8 @@ static void execute(const Token *start, const Token *end, Data &data)
if (Token::simpleMatch(thenEnd, "} else {")) {
const Token *elseStart = thenEnd->tokAt(2);
execute(elseStart->next(), end, elseData);
} else {
execute(thenEnd, end, elseData);
}
return;
}