From 05aae9569bc7896f035442963973d616c7260812 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Marjam=C3=A4ki?= Date: Sun, 6 Oct 2019 18:26:40 +0200 Subject: [PATCH] ExprEngine: Execute false execution path even if there is no else, upon Z3 exception assume that value is in range (safe option) --- lib/exprengine.cpp | 19 +++++++++++++------ 1 file changed, 13 insertions(+), 6 deletions(-) diff --git a/lib/exprengine.cpp b/lib/exprengine.cpp index 71b074fbd..48bf50ea7 100644 --- a/lib/exprengine.cpp +++ b/lib/exprengine.cpp @@ -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(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(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; }