Added regression test for pointers. Updated KLEE.

Author: S1eGa

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

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)

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