Typecasting value-set of pointers needs to propagate down

Author: jezhiggins

regression/goto-analyzer/heap-allocation-write-2/test-value-set-pointers.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--variable-sensitivity --vsd-pointers value-set --vsd-arrays every-element --verify
+^EXIT=0$
+^SIGNAL=0$
+\[main.assertion.1\] .*p\[.*0\] == 10: SUCCESS
+\[main.assertion.2\] .*p\[.*1\] == 20: SUCCESS
+\[main.assertion.3\] .*q\[.*0\] == 100: SUCCESS
+\[main.assertion.4\] .*q\[.*99\] == 101: SUCCESS
+--

regression/goto-analyzer/heap-allocation-write/test-value-set-pointers.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--variable-sensitivity --vsd-pointers value-set --vsd-arrays every-element --verify
+^EXIT=0$
+^SIGNAL=0$
+\[main.assertion.1\] .*alias == 99: SUCCESS
+\[main.assertion.2\] .*alias == 100: SUCCESS
+\[main.assertion.3\] .*i_was_malloced\[.*0\] == 101: SUCCESS
+\[main.assertion.4\] .*alias\[.*1\] == 102: SUCCESS
+--

regression/goto-analyzer/heap-allocation/test-value-set-pointers.desc

@@ -3,6 +3,6 @@ main.c
 --variable-sensitivity --vsd-pointers value-set --show
 ^EXIT=0$
 ^SIGNAL=0$
-main::1::p \(\) -> value-set-begin: ptr ->\(heap-allocation-0\) :value-set-end
-main::1::q \(\) -> value-set-begin: ptr ->\(heap-allocation-1\) :value-set-end
+main::1::p \(\) -> value-set-begin: ptr ->\(heap-allocation-0\[0\]\) :value-set-end
+main::1::q \(\) -> value-set-begin: ptr ->\(heap-allocation-1\[0\]\) :value-set-end
 --

src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp

@@ -34,9 +34,10 @@ value_set_pointer_abstract_objectt::value_set_pointer_abstract_objectt(
 
 value_set_pointer_abstract_objectt::value_set_pointer_abstract_objectt(
   const typet &new_type,
-  const value_set_pointer_abstract_objectt &old)
-  : abstract_pointer_objectt(new_type, old.is_top(), old.is_bottom()),
-    values(old.values)
+  bool top,
+  bool bottom,
+  const abstract_object_sett &new_values)
+  : abstract_pointer_objectt(new_type, top, bottom), values(new_values)
 {
 }
 
@@ -111,7 +112,15 @@ abstract_object_pointert value_set_pointer_abstract_objectt::typecast(
   const namespacet &ns) const
 {
   INVARIANT(is_void_pointer(type()), "Only allow pointer casting from void*");
-  return std::make_shared<value_set_pointer_abstract_objectt>(new_type, *this);
+  abstract_object_sett new_values;
+  for(auto value : values)
+  {
+    auto pointer =
+      std::dynamic_pointer_cast<const abstract_pointer_objectt>(value);
+    new_values.insert(pointer->typecast(new_type, environment, ns));
+  }
+  return std::make_shared<value_set_pointer_abstract_objectt>(
+    new_type, is_top(), is_bottom(), new_values);
 }
 
 abstract_object_pointert value_set_pointer_abstract_objectt::resolve_values(

src/analyses/variable-sensitivity/value_set_pointer_abstract_object.h

@@ -24,7 +24,9 @@ class value_set_pointer_abstract_objectt : public abstract_pointer_objectt,
 
   value_set_pointer_abstract_objectt(
     const typet &new_type,
-    const value_set_pointer_abstract_objectt &old);
+    bool top,
+    bool bottom,
+    const abstract_object_sett &new_values);
 
   /// \copydoc abstract_objectt::abstract_objectt(const typet &, bool, bool)
   value_set_pointer_abstract_objectt(const typet &type, bool top, bool bottom);