ExprEngine: Handle pointers to struct as function argument (danmar#2945)

jubnzv · web-flow · commit 36ab23f1f741 · 2020-12-13T16:02:35.000+01:00
diff --git a/lib/exprengine.cpp b/lib/exprengine.cpp
@@ -2625,8 +2625,19 @@ static std::string execute(const Token *start, const Token *end, Data &data)
                         if (!structVal1)
                             structVal1 = createVariableValue(*structToken->variable(), data);
                         auto structVal = std::dynamic_pointer_cast<ExprEngine::StructValue>(structVal1);
-                        if (!structVal)
-                            throw ExprEngineException(tok2, "Unhandled assignment in loop");
+                        if (!structVal) {
+                            // Handle pointer to a struct
+                            if (auto structPtr = std::dynamic_pointer_cast<ExprEngine::ArrayValue>(structVal1)) {
+                                if (structPtr && structPtr->pointer && !structPtr->data.empty()) {
+                                    auto indexValue = std::make_shared<ExprEngine::IntRange>("0", 0, 0);
+                                    for (auto val: structPtr->read(indexValue)) {
+                                        structVal = std::dynamic_pointer_cast<ExprEngine::StructValue>(val.second);
+                                    }
+                                }
+                            }
+                            if (!structVal)
+                                throw ExprEngineException(tok2, "Unhandled assignment in loop");
+                        }
 
                         data.assignStructMember(tok2, &*structVal, memberName, memberValue);
                         continue;
diff --git a/test/testexprengine.cpp b/test/testexprengine.cpp
@@ -114,6 +114,8 @@ class TestExprEngine : public TestFixture {
         TEST_CASE(structMember2);
         TEST_CASE(structMember3);
 
+        TEST_CASE(pointerToStructInLoop);
+
         TEST_CASE(ternaryOperator1);
 #endif
     }
@@ -816,6 +818,20 @@ class TestExprEngine : public TestFixture {
         ASSERT_EQUALS(expected, expr(code, "=="));
     }
 
+    void pointerToStructInLoop() {
+        const char code[] = "struct S { int x; };\n"
+                            "void foo(struct S *s) {\n"
+                            "  while (1)\n"
+                            "    s->x = 42; \n"
+                            "}";
+
+        const char expected[] = "(and (>= $3 (- 2147483648)) (<= $3 2147483647))\n"
+                                "(= $3 42)\n"
+                                "z3::sat\n";
+
+        ASSERT_EQUALS(expected, expr(code, "=="));
+    }
+
 
     void ternaryOperator1() {
         const char code[] = "void foo(signed char x) {\n"
