From 34572a40ab5b4046c77ba9abc50b0afac4a90954 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Daniel=20Marjam=C3=A4ki?= <daniel.marjamaki@gmail.com>
Date: Fri, 1 May 2020 15:15:24 +0200
Subject: [PATCH] Bug hunting: Fixed handling of switch 'case %char%'

---
 lib/exprengine.cpp      |  5 +++--
 test/testexprengine.cpp | 29 +++++++++++++++++++++++++++++
 2 files changed, 32 insertions(+), 2 deletions(-)

diff --git a/lib/exprengine.cpp b/lib/exprengine.cpp
index 49987f67c..76b5e8dea 100644
--- a/lib/exprengine.cpp
+++ b/lib/exprengine.cpp
@@ -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()) {
                 if (tok2->str() == "{")
                     tok2 = tok2->link();
-                else if (Token::Match(tok2, "case %num% :")) {
-                    auto caseValue = std::make_shared<ExprEngine::IntRange>(tok2->strAt(1), MathLib::toLongNumber(tok2->strAt(1)), MathLib::toLongNumber(tok2->strAt(1)));
+                else if (Token::Match(tok2, "case %char%|%num% :")) {
+                    const MathLib::bigint caseValue1 = tok2->next()->getKnownIntValue();
+                    auto caseValue = std::make_shared<ExprEngine::IntRange>(MathLib::toString(caseValue1), caseValue1, caseValue1);
                     Data caseData(data);
                     caseData.addConstraint(condValue, caseValue, true);
                     defaultData.addConstraint(condValue, caseValue, false);
diff --git a/test/testexprengine.cpp b/test/testexprengine.cpp
index 0e694e2e5..e345defa1 100644
--- a/test/testexprengine.cpp
+++ b/test/testexprengine.cpp
@@ -56,6 +56,7 @@ private:
         TEST_CASE(ifelse1);
 
         TEST_CASE(switch1);
+        TEST_CASE(switch2);
 
         TEST_CASE(while1);
         TEST_CASE(while2);
@@ -356,6 +357,34 @@ private:
                       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() {
         const char code[] = "void f(int y) {\n"
                             "  int x = 0;\n"