Propagate merge location context down to array elements

Author: jezhiggins

regression/goto-analyzer/liveness-array/main.c

@@ -0,0 +1,10 @@
+int main()
+{
+  int non_det;
+  int x[2] = {0, 1};
+
+  if(non_det)
+    x[0] = 2;
+  else
+    x[0] = 3;
+}

regression/goto-analyzer/liveness-array/test-liveness.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--variable-sensitivity --vsd-arrays every-element --vsd-values intervals --vsd-liveness --show
+^EXIT=0$
+^SIGNAL=0$
+^main::1::x .* TOP @ \[1\]
+^main::1::x .* \{\[0\] = \[0, 0\] @ \[2\]
+^main::1::x .* \{\[0\] = \[2, 3\] @ \[7\]
+--

regression/goto-analyzer/liveness-array/test-write-location.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--variable-sensitivity --vsd-arrays every-element --vsd-values intervals --show
+^EXIT=0$
+^SIGNAL=0$
+^main::1::x .* TOP @ \[1\]
+^main::1::x .* \{\[0\] = \[0, 0\] @ \[2\]
+^main::1::x .* \{\[0\] = \[2, 3\] @ \[4, 6\]
+--

src/analyses/variable-sensitivity/full_array_abstract_object.cpp

@@ -383,6 +383,12 @@ abstract_object_pointert full_array_abstract_objectt::write_location_context(
   return visit_sub_elements(location_update_visitort(location));
 }
 
+abstract_object_pointert full_array_abstract_objectt::merge_location_context(
+  const locationt &location) const
+{
+  return visit_sub_elements(merge_location_update_visitort(location));
+}
+
 abstract_object_pointert full_array_abstract_objectt::visit_sub_elements(
   const abstract_object_visitort &visitor) const
 {

src/analyses/variable-sensitivity/full_array_abstract_object.h

@@ -70,6 +70,8 @@ class full_array_abstract_objectt : public abstract_aggregate_objectt<
    */
   abstract_object_pointert
   write_location_context(const locationt &location) const override;
+  abstract_object_pointert
+  merge_location_context(const locationt &location) const override;
 
   /**
    * Apply a visitor operation to all sub elements of this abstract_object.