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

ExprEngine; Avoid overspecified constraints

This commit is contained in:
Daniel Marjamäki 2020-12-22 11:10:01 +01:00
parent f4f3b1bc77
commit 347fccb207
2 changed files with 11 additions and 15 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
lib/exprengine.cpp
View File

@ -2565,8 +2565,10 @@ static std::string execute(const Token *start, const Token *end, Data &data)
Data &thenData(data); Data &thenData(data);
Data elseData(data); Data elseData(data);
thenData.addConstraint(condValue, true); if (canBeFalse && canBeTrue) { // Avoid that constraints are overspecified
elseData.addConstraint(condValue, false); thenData.addConstraint(condValue, true);
elseData.addConstraint(condValue, false);
}
Data::ifSplit(tok, thenData, elseData); Data::ifSplit(tok, thenData, elseData);

20
test/testexprengine.cpp
View File

@ -462,8 +462,7 @@ private:
" }\n" " }\n"
" return a == 0;\n" " return a == 0;\n"
"}"; "}";
const char expected[] = "(distinct 1 0)\n" const char expected[] = "(= 0 0)\n"
"(= 0 0)\n"
"z3::sat\n"; "z3::sat\n";
ASSERT_EQUALS(expected, expr(code, "==")); ASSERT_EQUALS(expected, expr(code, "=="));
} }
@ -476,8 +475,7 @@ private:
" }\n" " }\n"
" return a == 0;\n" " return a == 0;\n"
"}"; "}";
const char expected[] = "(distinct 12.3 0.0)\n" const char expected[] = "(= 0 0)\n"
"(= 0 0)\n"
"z3::sat\n"; "z3::sat\n";
ASSERT_EQUALS(expected, expr(code, "==")); ASSERT_EQUALS(expected, expr(code, "=="));
} }
@ -491,7 +489,9 @@ private:
" return a == 0;\n" " return a == 0;\n"
"}"; "}";
// String literals are always true. z3 will not be involved. // String literals are always true. z3 will not be involved.
ASSERT_EQUALS("", expr(code, "==")); ASSERT_EQUALS("(= 0 0)\n"
"z3::sat\n",
expr(code, "=="));
} }
void ifAlwaysFalse1() { void ifAlwaysFalse1() {
@ -502,8 +502,7 @@ private:
" }\n" " }\n"
" return a == 0;\n" " return a == 0;\n"
"}"; "}";
const char expected[] = "(= 0 0)\n" const char expected[] = "(= 42 0)\n"
"(= 42 0)\n"
"z3::unsat\n"; "z3::unsat\n";
ASSERT_EQUALS(expected, expr(code, "==")); ASSERT_EQUALS(expected, expr(code, "=="));
} }
@ -516,8 +515,7 @@ private:
" }\n" " }\n"
" return a == 0;\n" " return a == 0;\n"
"}"; "}";
const char expected[] = "(= 0.0 0.0)\n" const char expected[] = "(= 42 0)\n"
"(= 42 0)\n"
"z3::unsat\n"; "z3::unsat\n";
ASSERT_EQUALS(expected, expr(code, "==")); ASSERT_EQUALS(expected, expr(code, "=="));
} }
@ -539,12 +537,10 @@ private:
"}"; "}";
ASSERT_EQUALS("(> $1 5)\n" ASSERT_EQUALS("(> $1 5)\n"
"(> $1 5)\n"
"(and (>= $1 0) (<= $1 255))\n" "(and (>= $1 0) (<= $1 255))\n"
"(= $1 13)\n" "(= $1 13)\n"
"z3::sat\n" "z3::sat\n"
"(<= $1 5)\n" "(<= $1 5)\n"
"(<= $1 5)\n"
"(and (>= $1 0) (<= $1 255))\n" "(and (>= $1 0) (<= $1 255))\n"
"(= $1 13)\n" "(= $1 13)\n"
"z3::unsat\n", "z3::unsat\n",
@ -575,7 +571,6 @@ private:
" return x == 0;\n" // <- sat " return x == 0;\n" // <- sat
"}"; "}";
ASSERT_EQUALS("(<= $1 0)\n" ASSERT_EQUALS("(<= $1 0)\n"
"(= $1 0)\n"
"(and (>= $1 0) (<= $1 255))\n" "(and (>= $1 0) (<= $1 255))\n"
"(= $1 0)\n" "(= $1 0)\n"
"z3::sat\n", "z3::sat\n",
@ -592,7 +587,6 @@ private:
" return x == 0;\n" // <- unsat " return x == 0;\n" // <- unsat
"}"; "}";
ASSERT_EQUALS("(>= $1 1)\n" ASSERT_EQUALS("(>= $1 1)\n"
"(distinct $1 0)\n"
"(and (>= $1 0) (<= $1 255))\n" "(and (>= $1 0) (<= $1 255))\n"
"(= (+ $1 1) 0)\n" "(= (+ $1 1) 0)\n"
"z3::unsat\n", "z3::unsat\n",