Added regression test for pointers. Updated KLEE.

Author: S1eGa

server/test/framework/Regression_Tests.cpp

@@ -340,6 +340,42 @@ namespace {
                 "f4");
     }
 
+    TEST_F(Regression_Test, Pointers_Alignment) {
+        static const size_t HEX = 16;
+        static const size_t NODE_ALIGNMENT = 8;
+        
+        fs::path source = getTestFilePath("issue-195.c");
+        auto [testGen, status] = createTestForFunction(source, NODE_ALIGNMENT);
+
+        ASSERT_TRUE(status.ok()) << status.error_message();
+
+        std::function<bool(const tests::Tests::TestCaseParamValue &)> checkAlignmentInNode =
+            [&checkAlignmentInNode](const tests::Tests::TestCaseParamValue &param) {
+                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;
+            };
+
+
+        checkTestCasePredicates(
+            testGen.tests.at(source).methods.begin().value().testCases,
+            std::vector<TestCasePredicate>(
+                { [&checkAlignmentInNode](const tests::Tests::MethodTestCase &testCase) {
+                    for (const auto &paramValue : testCase.paramValues) {
+                        if (!checkAlignmentInNode(paramValue)) {
+                            return false;
+                        }
+                    }
+                    return true;
+                } }),
+            "list_sum");
+    }
+
     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;
+}