diff --git a/lib/exprengine.cpp b/lib/exprengine.cpp index aa982da15..0d9530d52 100644 --- a/lib/exprengine.cpp +++ b/lib/exprengine.cpp @@ -891,8 +891,12 @@ ExprEngine::ArrayValue::ArrayValue(DataBase *data, const Variable *var) size.push_back(std::make_shared(data->getNewSymbolName(), 1, ExprEngine::ArrayValue::MAXSIZE)); } + const Token *initToken = var->nameToken(); + while (initToken && initToken->str() != "=") + initToken = initToken->astParent(); + ValuePtr val; - if (var && !var->isGlobal() && !var->isStatic() && !(var->isArgument() && var->isConst())) + if (var && !var->isGlobal() && !var->isStatic() && !(var->isArgument() && var->isConst()) && !initToken) val = std::make_shared(); else if (var && var->valueType()) { ::ValueType vt(*var->valueType()); diff --git a/test/testexprengine.cpp b/test/testexprengine.cpp index 948f99e5d..ecb88a37e 100644 --- a/test/testexprengine.cpp +++ b/test/testexprengine.cpp @@ -87,6 +87,7 @@ private: TEST_CASE(array6); TEST_CASE(arrayInit1); TEST_CASE(arrayInit2); + TEST_CASE(arrayInit3); TEST_CASE(arrayUninit); TEST_CASE(arrayInLoop); @@ -615,8 +616,8 @@ private: } void array2() { - ASSERT_EQUALS("(and (>= |$3:4| 0) (<= |$3:4| 255))\n" - "(= |$3:4| 365)\n" + ASSERT_EQUALS("(and (>= |$4:4| 0) (<= |$4:4| 255))\n" + "(= |$4:4| 365)\n" "z3::unsat\n", expr("void dostuff(unsigned char *); int f() { unsigned char arr[10] = \"\"; dostuff(arr); return arr[4] == 365; }", "==")); } @@ -672,6 +673,10 @@ private: ASSERT_EQUALS("66", getRange("void f() { char str[] = \"hello\"; str[0] = \'B\'; }", "str[0]=\'B\'")); } + void arrayInit3() { + ASSERT_EQUALS("-32768:32767", getRange("void f() { short buf[5] = {2, 1, 0, 3, 4}; ret = buf[2]; }", "buf[2]")); + } + void arrayUninit() { ASSERT_EQUALS("?", getRange("int f() { int arr[10]; return arr[4]; }", "arr[4]")); }