From be422355f0200d03fc5e677bbdef9d5f7dd1346a Mon Sep 17 00:00:00 2001
From: Sergey Morozov <morozov.serg901@gmail.com>
Date: Wed, 7 Sep 2022 19:13:51 +0300
Subject: [PATCH] Added regression test for pointers. Updated KLEE.

---
 server/test/framework/Regression_Tests.cpp   | 28 ++++++++++++++++++++
 server/test/suites/regression/CMakeLists.txt |  2 ++
 server/test/suites/regression/issue-195.c    | 15 +++++++++++
 submodules/klee                              |  2 +-
 4 files changed, 46 insertions(+), 1 deletion(-)
 create mode 100644 server/test/suites/regression/issue-195.c

diff --git a/server/test/framework/Regression_Tests.cpp b/server/test/framework/Regression_Tests.cpp
index 0df4c355..8a157aaf 100644
--- a/server/test/framework/Regression_Tests.cpp
+++ b/server/test/framework/Regression_Tests.cpp
@@ -340,6 +340,34 @@ namespace {
                 "f4");
     }
 
+    static bool checkAlignmentInNode(const tests::Tests::TestCaseParamValue &param) {
+        static const size_t HEX = 16;
+        static const size_t NODE_ALIGNMENT = 8;
+
+        const auto stringPointer = param.view->getSubViews().at(1)->getEntryValue(nullptr);
+        const size_t address = strtoull(stringPointer.c_str(), nullptr, HEX);
+        bool result = (address % NODE_ALIGNMENT == 0);
+
+        for (const auto &innerLazyValueParam : param.lazyValues) {
+            result &= checkAlignmentInNode(innerLazyValueParam);
+        }
+        return result;
+    }
+
+    TEST_F(Regression_Test, Pointers_Alignment) {
+        fs::path source = getTestFilePath("issue-195.c");
+        auto [testGen, status] = createTestForFunction(source, 8);
+
+        ASSERT_TRUE(status.ok()) << status.error_message();
+
+        for (const tests::Tests::MethodTestCase &testCase :
+             testGen.tests.at(source).methods.begin().value().testCases) {
+            for (const auto &paramValue : testCase.paramValues) {
+                EXPECT_TRUE(checkAlignmentInNode(paramValue));
+            }
+        }
+    }
+
     TEST_F(Regression_Test, Generate_Folder) {
         fs::path folderPath = getTestFilePath("ISSUE-140");
         auto [testGen, status] = createTestForFolder(folderPath, true, true);
diff --git a/server/test/suites/regression/CMakeLists.txt b/server/test/suites/regression/CMakeLists.txt
index b5b76213..ce641223 100644
--- a/server/test/suites/regression/CMakeLists.txt
+++ b/server/test/suites/regression/CMakeLists.txt
@@ -49,4 +49,6 @@ target_compile_definitions(issue-276 PUBLIC EXPORT2="")
 target_compile_definitions(issue-276 PUBLIC EXPORT3=4)
 target_compile_definitions(issue-276 PUBLIC EXPORT4="4")
 
+add_library(issue-195 issue-195.c)
+
 set_target_properties(regression PROPERTIES LINK_WHAT_YOU_USE TRUE)
diff --git a/server/test/suites/regression/issue-195.c b/server/test/suites/regression/issue-195.c
new file mode 100644
index 00000000..336bcbf8
--- /dev/null
+++ b/server/test/suites/regression/issue-195.c
@@ -0,0 +1,15 @@
+#include <stdlib.h>
+
+typedef struct Node {
+    int value;
+    struct Node *next;
+} Node;
+
+int list_sum(Node *head) {
+    int sum = 0;
+    while (head != NULL) {
+        sum += head->value;
+        head = head->next;
+    }
+    return sum;
+}
diff --git a/submodules/klee b/submodules/klee
index 40e004cd..5bc03123 160000
--- a/submodules/klee
+++ b/submodules/klee
@@ -1 +1 @@
-Subproject commit 40e004cd67da3ab56d48e705c24afe01be0c80ba
+Subproject commit 5bc03123155ed2adee6fa52ebad0c51c1c1e907e