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

Fixed #9402 (ExprEngine: && and || in condition)

This commit is contained in:
Daniel Marjamäki 2019-12-24 15:51:45 +01:00
parent 81bea120fc
commit 755e2d261c
2 changed files with 36 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
lib/exprengine.cpp
View File

@ -1092,7 +1092,14 @@ static ExprEngine::ValuePtr executeDot(const Token *tok, Data &data)
static ExprEngine::ValuePtr executeBinaryOp(const Token *tok, Data &data)
{
ExprEngine::ValuePtr v1 = executeExpression(tok->astOperand1(), data);
ExprEngine::ValuePtr v2 = executeExpression(tok->astOperand2(), data);
ExprEngine::ValuePtr v2;
if (tok->str() == "&&" || tok->str() == "||") {
Data data2(data);
data2.addConstraint(v1, tok->str() == "&&");
v2 = executeExpression(tok->astOperand2(), data2);
} else {
v2 = executeExpression(tok->astOperand2(), data);
}
if (v1 && v2) {
auto result = simplifyValue(std::make_shared<ExprEngine::BinOpResult>(tok->str(), v1, v2));
call(data.callbacks, tok, result, &data);

28
test/testexprengine.cpp
View File

@ -44,6 +44,8 @@ private:
TEST_CASE(exprAssign2); // Truncation
TEST_CASE(if1);
TEST_CASE(if2);
TEST_CASE(if3);
TEST_CASE(ifelse1);
TEST_CASE(switch1);
@ -218,6 +220,32 @@ private:
expr("void f(int x, int y) { if (x < y) return x == y; }", "=="));
}
void if2() {
const char code[] = "void foo(int x) {\n"
" if (x > 0 && x == 20) {}\n"
"}";
// In expression "x + x < 20", "x" is greater than 0
const char expected[] = "(declare-fun $1 () Int)\n"
"(assert (and (>= $1 (- 2147483648)) (<= $1 2147483647)))\n"
"(assert (> $1 0))\n"
"(assert (= $1 20))\n"
"z3::sat";
ASSERT_EQUALS(expected, expr(code, "=="));
}
void if3() {
const char code[] = "void foo(int x) {\n"
" if (x > 0 || x == 20) {}\n"
"}";
// In expression "x + x < 20", "x" is greater than 0
const char expected[] = "(declare-fun $1 () Int)\n"
"(assert (and (>= $1 (- 2147483648)) (<= $1 2147483647)))\n"
"(assert (<= $1 0))\n"
"(assert (= $1 20))\n"
"z3::unsat"; // "x == 20" is unsat
ASSERT_EQUALS(expected, expr(code, "=="));
}
void ifelse1() {
ASSERT_EQUALS("(declare-fun $1 () Int)\n"
"(assert (and (>= $1 (- 32768)) (<= $1 32767)))\n"