Bug hunting; Fixed array init

danmar · danmar · commit 82635417d264 · 2020-12-14T22:15:10.000+01:00
diff --git 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<ExprEngine::IntRange>(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<ExprEngine::UninitValue>();
     else if (var && var->valueType()) {
         ::ValueType vt(*var->valueType());
diff --git a/test/testexprengine.cpp b/test/testexprengine.cpp
@@ -87,6 +87,7 @@ class TestExprEngine : public TestFixture {
         TEST_CASE(array6);
         TEST_CASE(arrayInit1);
         TEST_CASE(arrayInit2);
+        TEST_CASE(arrayInit3);
         TEST_CASE(arrayUninit);
         TEST_CASE(arrayInLoop);
 
@@ -615,8 +616,8 @@ class TestExprEngine : public TestFixture {
     }
 
     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 @@ class TestExprEngine : public TestFixture {
         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]"));
     }
