From 144c3e944434afa20774783766e911ddd18dd8dc Mon Sep 17 00:00:00 2001
From: Pavel <operasfantom@gmail.com>
Date: Tue, 14 Jun 2022 18:34:32 +0400
Subject: [PATCH] Use klee_assume(s[N - 1] == '\0') call for the last element
 of string

---
 .../src/printers/KleeConstraintsPrinter.cpp   |  2 +-
 server/test/framework/Regression_Tests.cpp    | 30 +++++++++++++++++++
 server/test/suites/regression/CMakeLists.txt  |  4 ++-
 server/test/suites/regression/GH215.c         |  8 +++++
 4 files changed, 42 insertions(+), 2 deletions(-)
 create mode 100644 server/test/suites/regression/GH215.c

diff --git a/server/src/printers/KleeConstraintsPrinter.cpp b/server/src/printers/KleeConstraintsPrinter.cpp
index 990574b64..1161e1fd8 100644
--- a/server/src/printers/KleeConstraintsPrinter.cpp
+++ b/server/src/printers/KleeConstraintsPrinter.cpp
@@ -120,7 +120,7 @@ void KleeConstraintsPrinter::genConstraintsForMultiPointerOrArray(const Constrai
         std::vector<std::string> charSizes(indexes.begin(), indexes.end() - 1);
         const auto charElement = constrMultiIndex(state.curElement, charSizes);
         ss << TAB_N() << "if (" << indexes.back() << PrinterUtils::EQ_OPERATOR << sizes.back() - 1 << ")" << LB();
-        ss << TAB_N() << charElement << "[" << sizes.back() - 1 << "]" << PrinterUtils::ASSIGN_OPERATOR << "'\\0'" << SCNL;
+        ss << TAB_N() << PrinterUtils::KLEE_ASSUME << "(" << charElement << "[" << sizes.back() - 1 << "]" << PrinterUtils::EQ_OPERATOR << "'\\0'" << ")" << SCNL;
         ss << TAB_N() << "break" << SCNL;
         ss << RB();
     }
diff --git a/server/test/framework/Regression_Tests.cpp b/server/test/framework/Regression_Tests.cpp
index f036ea138..3379134c2 100644
--- a/server/test/framework/Regression_Tests.cpp
+++ b/server/test/framework/Regression_Tests.cpp
@@ -238,4 +238,34 @@ namespace {
 
         ASSERT_TRUE(status.ok()) << status.error_message();
     }
+
+    TEST_F(Regression_Test, Hash_Of_String) {
+        fs::path source = getTestFilePath("GH215.c");
+        auto [testGen, status] = createTestForFunction(source, 2);
+
+        ASSERT_TRUE(status.ok()) << status.error_message();
+
+        auto predicate = [](const tests::Tests::MethodTestCase &testCase) {
+            auto s = testCase.paramValues[0].view->getEntryValue(nullptr);
+            s = s.substr(1, s.length() - 2);
+            auto actual = testCase.returnValue.view->getEntryValue(nullptr);
+            auto expected = std::to_string(std::accumulate(s.begin(), s.end(), 0));
+            return actual == expected;
+        };
+
+        checkTestCasePredicates(
+            testGen.tests.at(source).methods.begin().value().testCases,
+            std::vector<TestCasePredicate>(
+                { [&predicate](const tests::Tests::MethodTestCase &testCase) {
+                     // empty string
+                     return testCase.paramValues[0].view->getEntryValue(nullptr).length() == 2 &&
+                            predicate(testCase);
+                 },
+                  [&predicate](const tests::Tests::MethodTestCase &testCase) {
+                      // non-empty string
+                      return testCase.paramValues[0].view->getEntryValue(nullptr).length() > 2 &&
+                             predicate(testCase);
+                  } }),
+            "hash");
+    }
 }
diff --git a/server/test/suites/regression/CMakeLists.txt b/server/test/suites/regression/CMakeLists.txt
index f5d81c594..48aa5b059 100644
--- a/server/test/suites/regression/CMakeLists.txt
+++ b/server/test/suites/regression/CMakeLists.txt
@@ -38,4 +38,6 @@ add_library(PR124 PR124.c)
 
 add_library(PR153 PR153.c)
 
-set_target_properties(regression PROPERTIES LINK_WHAT_YOU_USE TRUE)
\ No newline at end of file
+add_library(GH215 GH215.c)
+
+set_target_properties(regression PROPERTIES LINK_WHAT_YOU_USE TRUE)
diff --git a/server/test/suites/regression/GH215.c b/server/test/suites/regression/GH215.c
new file mode 100644
index 000000000..e0a32edd6
--- /dev/null
+++ b/server/test/suites/regression/GH215.c
@@ -0,0 +1,8 @@
+int hash(const char *s) {
+    int h = 0, i = 0;
+    while (s[i] != '\0') {
+        h = (h + s[i]);
+        i++;
+    }
+    return h;
+}