ExprEngine; copy Data => copy arrays

lib/exprengine.cpp

@@ -340,6 +340,26 @@ namespace {
             , startTime(std::time(nullptr))
             , mTrackExecution(trackExecution)
             , mDataIndex(trackExecution->getNewDataIndex()) {}
+
+        Data(const Data &old)
+            : DataBase(old.currentFunction, old.settings)
+            , symbolValueIndex(old.symbolValueIndex)
+            , errorLogger(old.errorLogger)
+            , tokenizer(old.tokenizer)
+            , callbacks(old.callbacks)
+            , recursion(old.recursion)
+            , startTime(old.startTime)
+            , mTrackExecution(old.mTrackExecution)
+            , mDataIndex(mTrackExecution->getNewDataIndex()) {
+            memory = old.memory;
+            for (auto &it: memory) {
+                if (!it.second)
+                    continue;
+                if (auto oldValue = std::dynamic_pointer_cast<ExprEngine::ArrayValue>(it.second))
+                    it.second = std::make_shared<ExprEngine::ArrayValue>(getNewSymbolName(), *oldValue);
+            }
+        }
+
         typedef std::map<nonneg int, ExprEngine::ValuePtr> Memory;
         Memory memory;
         int * const symbolValueIndex;
@@ -809,6 +829,15 @@ ExprEngine::ArrayValue::ArrayValue(DataBase *data, const Variable *var)
     assign(ExprEngine::ValuePtr(), val);
 }
 
+ExprEngine::ArrayValue::ArrayValue(const std::string &name, const ExprEngine::ArrayValue &arrayValue)
+    : Value(name, ExprEngine::ValueType::ArrayValue)
+    , pointer(arrayValue.pointer), nullPointer(arrayValue.nullPointer), uninitPointer(arrayValue.uninitPointer)
+{
+    size = arrayValue.size;
+    data = arrayValue.data;
+}
+
+
 std::string ExprEngine::ArrayValue::getRange() const
 {
     std::string r = getSymbolicExpression();

lib/exprengine.h

@@ -194,6 +194,7 @@ namespace ExprEngine {
 
         ArrayValue(const std::string &name, ValuePtr size, ValuePtr value, bool pointer, bool nullPointer, bool uninitPointer);
         ArrayValue(DataBase *data, const Variable *var);
+        ArrayValue(const std::string &name, const ArrayValue &arrayValue);
 
         std::string getRange() const OVERRIDE;
         std::string getSymbolicExpression() const OVERRIDE;

test/testbughuntingchecks.cpp

@@ -31,6 +31,7 @@ private:
     void run() OVERRIDE {
 #ifdef USE_Z3
         TEST_CASE(uninit);
+        TEST_CASE(uninit_array);
         TEST_CASE(uninit_function_par);
         TEST_CASE(ctu);
 #endif
@@ -57,6 +58,15 @@ private:
         ASSERT_EQUALS("[test.cpp:1]: (error) Cannot determine that 'x' is initialized\n", errout.str());
     }
 
+    void uninit_array() {
+        check("void foo(int x) {\n"
+              "  int a[10];\n"
+              "  if (x > 0) a[0] = 32;\n"
+              "  return a[0];\n"
+              "}");
+        ASSERT_EQUALS("[test.cpp:4]: (error) Cannot determine that 'a[0]' is initialized\n", errout.str());
+    }
+
     void uninit_function_par() {
         // non constant parameters may point at uninitialized data
         // constant parameters should point at initialized data