diff --git a/lib/exprengine.cpp b/lib/exprengine.cpp index bd5edbb57..c8c8f08b3 100644 --- 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(structVal1); - if (!structVal) - throw ExprEngineException(tok2, "Unhandled assignment in loop"); + if (!structVal) { + // Handle pointer to a struct + if (auto structPtr = std::dynamic_pointer_cast(structVal1)) { + if (structPtr && structPtr->pointer && !structPtr->data.empty()) { + auto indexValue = std::make_shared("0", 0, 0); + for (auto val: structPtr->read(indexValue)) { + structVal = std::dynamic_pointer_cast(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 index b47acb5c6..ff1fd4895 100644 --- a/test/testexprengine.cpp +++ b/test/testexprengine.cpp @@ -114,6 +114,8 @@ private: TEST_CASE(structMember2); TEST_CASE(structMember3); + TEST_CASE(pointerToStructInLoop); + TEST_CASE(ternaryOperator1); #endif } @@ -816,6 +818,20 @@ private: 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"