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

ExprEngine: improved handling when lhs/rhs for && has unknown value

This commit is contained in:
Daniel Marjamäki 2020-05-10 22:50:23 +02:00
parent e0e50139cb
commit 046f8eb6c6
2 changed files with 15 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
lib/exprengine.cpp
View File

@ -1621,6 +1621,11 @@ static ExprEngine::ValuePtr executeBinaryOp(const Token *tok, Data &data)
call(data.callbacks, tok, result, &data); call(data.callbacks, tok, result, &data);
return result; return result;
} }
if (tok->str() == "&&" && (v1 || v2)) {
auto result = v1 ? v1 : v2;
call(data.callbacks, tok, result, &data);
return result;
}
return ExprEngine::ValuePtr(); return ExprEngine::ValuePtr();
} }

11
test/testexprengine.cpp
View File

@ -53,6 +53,7 @@ private:
TEST_CASE(if2); TEST_CASE(if2);
TEST_CASE(if3); TEST_CASE(if3);
TEST_CASE(if4); TEST_CASE(if4);
TEST_CASE(if5);
TEST_CASE(ifelse1); TEST_CASE(ifelse1);
TEST_CASE(switch1); TEST_CASE(switch1);
@ -344,6 +345,15 @@ private:
ASSERT_EQUALS(expected, expr(code, "==")); ASSERT_EQUALS(expected, expr(code, "=="));
} }
void if5() {
ASSERT_EQUALS("(> |$2:0| 12)\n"
"(and (>= |$2:0| (- 2147483648)) (<= |$2:0| 2147483647))\n"
"(= |$2:0| 5)\n"
"z3::unsat\n",
expr("void foo(const int *x) { if (f1() && *x > 12) dostuff(*x == 5); }", "=="));
}
void ifelse1() { void ifelse1() {
ASSERT_EQUALS("(<= $1 5)\n" ASSERT_EQUALS("(<= $1 5)\n"
"(and (>= $1 (- 32768)) (<= $1 32767))\n" "(and (>= $1 (- 32768)) (<= $1 32767))\n"
@ -523,7 +533,6 @@ private:
ASSERT_EQUALS("1:2147483647", getRange("void f() { sizeof(data); }", "sizeof(data)")); ASSERT_EQUALS("1:2147483647", getRange("void f() { sizeof(data); }", "sizeof(data)"));
} }
void functionCallContract1() { void functionCallContract1() {
const char code[] = "void foo(int x);\n" const char code[] = "void foo(int x);\n"
"void bar(unsigned short x) { foo(x); }"; "void bar(unsigned short x) { foo(x); }";