From 046f8eb6c6aa311a256834ef37a9fe36dfd660d5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Marjam=C3=A4ki?= Date: Sun, 10 May 2020 22:50:23 +0200 Subject: [PATCH] ExprEngine: improved handling when lhs/rhs for && has unknown value --- lib/exprengine.cpp | 5 +++++ test/testexprengine.cpp | 11 ++++++++++- 2 files changed, 15 insertions(+), 1 deletion(-) diff --git a/lib/exprengine.cpp b/lib/exprengine.cpp index 5f496a542..4dfeb6557 100644 --- a/lib/exprengine.cpp +++ b/lib/exprengine.cpp @@ -1621,6 +1621,11 @@ static ExprEngine::ValuePtr executeBinaryOp(const Token *tok, Data &data) call(data.callbacks, tok, result, &data); return result; } + if (tok->str() == "&&" && (v1 || v2)) { + auto result = v1 ? v1 : v2; + call(data.callbacks, tok, result, &data); + return result; + } return ExprEngine::ValuePtr(); } diff --git a/test/testexprengine.cpp b/test/testexprengine.cpp index d3ad391b4..25ee4538a 100644 --- a/test/testexprengine.cpp +++ b/test/testexprengine.cpp @@ -53,6 +53,7 @@ private: TEST_CASE(if2); TEST_CASE(if3); TEST_CASE(if4); + TEST_CASE(if5); TEST_CASE(ifelse1); TEST_CASE(switch1); @@ -344,6 +345,15 @@ private: 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() { ASSERT_EQUALS("(<= $1 5)\n" "(and (>= $1 (- 32768)) (<= $1 32767))\n" @@ -523,7 +533,6 @@ private: ASSERT_EQUALS("1:2147483647", getRange("void f() { sizeof(data); }", "sizeof(data)")); } - void functionCallContract1() { const char code[] = "void foo(int x);\n" "void bar(unsigned short x) { foo(x); }";