Use klee_assume(s[N - 1] == '\0') call for the last element of string

Author: operasfantom

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();
     }

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");
+    }
 }

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)
+add_library(GH215 GH215.c)
+
+set_target_properties(regression PROPERTIES LINK_WHAT_YOU_USE TRUE)

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;
+}