Bug hunting: Fixed handling of switch 'case %char%'

This commit is contained in:
Daniel Marjamäki 2020-05-01 15:15:24 +02:00
parent 2011a4dcbf
commit 34572a40ab
2 changed files with 32 additions and 2 deletions

View File

@ -1837,8 +1837,9 @@ static void execute(const Token *start, const Token *end, Data &data)
for (const Token *tok2 = bodyStart->next(); tok2 != bodyEnd; tok2 = tok2->next()) { for (const Token *tok2 = bodyStart->next(); tok2 != bodyEnd; tok2 = tok2->next()) {
if (tok2->str() == "{") if (tok2->str() == "{")
tok2 = tok2->link(); tok2 = tok2->link();
else if (Token::Match(tok2, "case %num% :")) { else if (Token::Match(tok2, "case %char%|%num% :")) {
auto caseValue = std::make_shared<ExprEngine::IntRange>(tok2->strAt(1), MathLib::toLongNumber(tok2->strAt(1)), MathLib::toLongNumber(tok2->strAt(1))); const MathLib::bigint caseValue1 = tok2->next()->getKnownIntValue();
auto caseValue = std::make_shared<ExprEngine::IntRange>(MathLib::toString(caseValue1), caseValue1, caseValue1);
Data caseData(data); Data caseData(data);
caseData.addConstraint(condValue, caseValue, true); caseData.addConstraint(condValue, caseValue, true);
defaultData.addConstraint(condValue, caseValue, false); defaultData.addConstraint(condValue, caseValue, false);

View File

@ -56,6 +56,7 @@ private:
TEST_CASE(ifelse1); TEST_CASE(ifelse1);
TEST_CASE(switch1); TEST_CASE(switch1);
TEST_CASE(switch2);
TEST_CASE(while1); TEST_CASE(while1);
TEST_CASE(while2); TEST_CASE(while2);
@ -356,6 +357,34 @@ private:
expr(code, "==")); expr(code, "=="));
} }
void switch2() {
const char code[] = "void foo(char type, int mcc) {\n"
" switch (type) {\n"
" case '1':\n"
" case '3':\n"
" break;\n"
" default:\n"
" return false;\n"
" }\n"
" p[0] = mcc == 0;\n"
"}";
ASSERT_EQUALS("(declare-fun $1 () Int)\n" // case '1'
"(declare-fun $2 () Int)\n"
"(assert (= $1 49))\n"
"(assert (and (>= $2 (- 2147483648)) (<= $2 2147483647)))\n"
"(assert (and (>= $1 (- 128)) (<= $1 127)))\n"
"(assert (= $2 0))\n"
"z3::sat\n"
"(declare-fun $1 () Int)\n" // case '3'
"(declare-fun $2 () Int)\n"
"(assert (= $1 51))\n"
"(assert (and (>= $2 (- 2147483648)) (<= $2 2147483647)))\n"
"(assert (and (>= $1 (- 128)) (<= $1 127)))\n"
"(assert (= $2 0))\n"
"z3::sat",
expr(code, "=="));
}
void while1() { void while1() {
const char code[] = "void f(int y) {\n" const char code[] = "void f(int y) {\n"
" int x = 0;\n" " int x = 0;\n"