From 913f1752d871b8f6eaacd26a612f3bf6e3a9d6f4 Mon Sep 17 00:00:00 2001
From: Jez Higgins <jez@jezuk.co.uk>
Date: Thu, 8 Jul 2021 14:55:12 +0100
Subject: [PATCH 01/12] Capture heap allocations

Create a special 'heap allocation' placeholder expression. Extend
write_stack to be able to store that expression.
---
 .../variable-sensitivity/abstract_environment.cpp     | 11 +++++++++++
 src/analyses/variable-sensitivity/write_stack.cpp     |  2 +-
 .../variable-sensitivity/write_stack_entry.cpp        |  4 +++-
 3 files changed, 15 insertions(+), 2 deletions(-)

diff --git a/src/analyses/variable-sensitivity/abstract_environment.cpp b/src/analyses/variable-sensitivity/abstract_environment.cpp
index b473730c36e..abb0c03010f 100644
--- a/src/analyses/variable-sensitivity/abstract_environment.cpp
+++ b/src/analyses/variable-sensitivity/abstract_environment.cpp
@@ -84,6 +84,17 @@ abstract_environmentt::eval(const exprt &expr, const namespacet &ns) const
     return abstract_object_factory(simplified_expr.type(), simplified_expr, ns);
   }
 
+  if(
+    simplified_id == ID_side_effect &&
+    (simplified_expr.get(ID_statement) == ID_allocate))
+  {
+    auto heap_symbol = unary_exprt(
+      ID_address_of, exprt(ID_dynamic_object), simplified_expr.type());
+    auto heap_pointer =
+      abstract_object_factory(simplified_expr.type(), heap_symbol, ns);
+    return heap_pointer;
+  }
+
   // No special handling required by the abstract environment
   // delegate to the abstract object
   if(!simplified_expr.operands().empty())
diff --git a/src/analyses/variable-sensitivity/write_stack.cpp b/src/analyses/variable-sensitivity/write_stack.cpp
index 05a33c578b2..f632d5d7f5d 100644
--- a/src/analyses/variable-sensitivity/write_stack.cpp
+++ b/src/analyses/variable-sensitivity/write_stack.cpp
@@ -138,7 +138,7 @@ void write_stackt::construct_stack_to_lvalue(
       construct_stack_to_lvalue(
         to_member_expr(expr).struct_op(), environment, ns);
     }
-    else if(expr.id() == ID_symbol)
+    else if(expr.id() == ID_symbol || expr.id() == ID_dynamic_object)
     {
       add_to_stack(std::make_shared<simple_entryt>(expr), environment, ns);
     }
diff --git a/src/analyses/variable-sensitivity/write_stack_entry.cpp b/src/analyses/variable-sensitivity/write_stack_entry.cpp
index 74d7deca398..24e06815bc1 100644
--- a/src/analyses/variable-sensitivity/write_stack_entry.cpp
+++ b/src/analyses/variable-sensitivity/write_stack_entry.cpp
@@ -32,7 +32,9 @@ bool write_stack_entryt::try_squash_in(
 simple_entryt::simple_entryt(exprt expr) : simple_entry(expr)
 {
   // Invalid simple expression added to the stack
-  PRECONDITION(expr.id() == ID_member || expr.id() == ID_symbol);
+  PRECONDITION(
+    expr.id() == ID_member || expr.id() == ID_symbol ||
+    expr.id() == ID_dynamic_object);
 }
 
 /// Get the expression part needed to read this stack entry. For simple

From 2023081d375141ab8337c8b0326f754c69607299 Mon Sep 17 00:00:00 2001
From: Jez Higgins <jez@jezuk.co.uk>
Date: Thu, 8 Jul 2021 15:28:19 +0100
Subject: [PATCH 02/12] Allow void* pointers cast to another pointer type

That's the expr.type() rather than the representation class.
---
 .../goto-analyzer/heap-allocation/main.c      |  7 +++++++
 .../test-constant-pointers.desc               |  7 +++++++
 .../test-two-value-pointers.desc              |  7 +++++++
 .../test-value-set-pointers.desc              |  7 +++++++
 .../abstract_pointer_object.cpp               | 21 +++++++++++++++++++
 .../abstract_pointer_object.h                 |  2 ++
 .../constant_pointer_abstract_object.cpp      | 15 ++++++++++++-
 .../constant_pointer_abstract_object.h        |  4 +++-
 .../value_set_pointer_abstract_object.cpp     | 16 ++++++++++++++
 .../value_set_pointer_abstract_object.h       |  6 ++++++
 10 files changed, 90 insertions(+), 2 deletions(-)
 create mode 100644 regression/goto-analyzer/heap-allocation/main.c
 create mode 100644 regression/goto-analyzer/heap-allocation/test-constant-pointers.desc
 create mode 100644 regression/goto-analyzer/heap-allocation/test-two-value-pointers.desc
 create mode 100644 regression/goto-analyzer/heap-allocation/test-value-set-pointers.desc

diff --git a/regression/goto-analyzer/heap-allocation/main.c b/regression/goto-analyzer/heap-allocation/main.c
new file mode 100644
index 00000000000..6b4a712b016
--- /dev/null
+++ b/regression/goto-analyzer/heap-allocation/main.c
@@ -0,0 +1,7 @@
+
+int main()
+{
+  int *i_was_malloced = malloc(sizeof(int) * 10);
+
+  // q[0] = 99;
+}
diff --git a/regression/goto-analyzer/heap-allocation/test-constant-pointers.desc b/regression/goto-analyzer/heap-allocation/test-constant-pointers.desc
new file mode 100644
index 00000000000..7f155c6696d
--- /dev/null
+++ b/regression/goto-analyzer/heap-allocation/test-constant-pointers.desc
@@ -0,0 +1,7 @@
+CORE
+main.c
+--variable-sensitivity --vsd-pointers constants --show
+^EXIT=0$
+^SIGNAL=0$
+main::1::i_was_malloced \(\) -> ptr ->\(heap allocation\)
+--
diff --git a/regression/goto-analyzer/heap-allocation/test-two-value-pointers.desc b/regression/goto-analyzer/heap-allocation/test-two-value-pointers.desc
new file mode 100644
index 00000000000..7de42fea4c0
--- /dev/null
+++ b/regression/goto-analyzer/heap-allocation/test-two-value-pointers.desc
@@ -0,0 +1,7 @@
+CORE
+main.c
+--variable-sensitivity --vsd-pointers top-bottom --show
+^EXIT=0$
+^SIGNAL=0$
+main::1::i_was_malloced \(\) -> TOP
+--
diff --git a/regression/goto-analyzer/heap-allocation/test-value-set-pointers.desc b/regression/goto-analyzer/heap-allocation/test-value-set-pointers.desc
new file mode 100644
index 00000000000..4cd2205b362
--- /dev/null
+++ b/regression/goto-analyzer/heap-allocation/test-value-set-pointers.desc
@@ -0,0 +1,7 @@
+CORE
+main.c
+--variable-sensitivity --vsd-pointers value-set --show
+^EXIT=0$
+^SIGNAL=0$
+main::1::i_was_malloced \(\) -> value-set-begin: ptr ->\(heap allocation\) :value-set-end
+--
diff --git a/src/analyses/variable-sensitivity/abstract_pointer_object.cpp b/src/analyses/variable-sensitivity/abstract_pointer_object.cpp
index dbad74720f1..3dbcd8cf166 100644
--- a/src/analyses/variable-sensitivity/abstract_pointer_object.cpp
+++ b/src/analyses/variable-sensitivity/abstract_pointer_object.cpp
@@ -46,6 +46,19 @@ abstract_object_pointert abstract_pointer_objectt::expression_transform(
   if(expr.id() == ID_dereference)
     return read_dereference(environment, ns);
 
+  if(expr.id() == ID_typecast)
+  {
+    const typecast_exprt &tce = to_typecast_expr(expr);
+    if(tce.op().id() == ID_symbol && is_void_pointer(tce.op().type()))
+    {
+      auto obj = environment.eval(tce.op(), ns);
+      auto pointer = std::dynamic_pointer_cast<const abstract_pointer_objectt>(
+        obj->unwrap_context());
+      if(pointer)
+        return pointer->typecast(tce.type());
+    }
+  }
+
   return abstract_objectt::expression_transform(
     expr, operands, environment, ns);
 }
@@ -87,6 +100,14 @@ abstract_object_pointert abstract_pointer_objectt::write_dereference(
   return std::make_shared<abstract_pointer_objectt>(type(), true, false);
 }
 
+abstract_object_pointert
+abstract_pointer_objectt::typecast(const typet &new_type) const
+{
+  INVARIANT(is_void_pointer(type()), "Only allow pointer casting from void*");
+  return std::make_shared<abstract_pointer_objectt>(
+    new_type, is_top(), is_bottom());
+}
+
 void abstract_pointer_objectt::get_statistics(
   abstract_object_statisticst &statistics,
   abstract_object_visitedt &visited,
diff --git a/src/analyses/variable-sensitivity/abstract_pointer_object.h b/src/analyses/variable-sensitivity/abstract_pointer_object.h
index 365cf710deb..0af41cf1a43 100644
--- a/src/analyses/variable-sensitivity/abstract_pointer_object.h
+++ b/src/analyses/variable-sensitivity/abstract_pointer_object.h
@@ -95,6 +95,8 @@ class abstract_pointer_objectt : public abstract_objectt,
     const std::stack<exprt> &stack,
     const abstract_object_pointert &value,
     bool merging_write) const;
+
+  virtual abstract_object_pointert typecast(const typet &new_type) const;
 };
 
 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_ABSTRACT_POINTER_OBJECT_H
diff --git a/src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp b/src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp
index 6cbd1eaba3e..fac7c692eb4 100644
--- a/src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp
+++ b/src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp
@@ -33,8 +33,10 @@ constant_pointer_abstract_objectt::constant_pointer_abstract_objectt(
 }
 
 constant_pointer_abstract_objectt::constant_pointer_abstract_objectt(
+  const typet &new_type,
   const constant_pointer_abstract_objectt &old)
-  : abstract_pointer_objectt(old), value_stack(old.value_stack)
+  : abstract_pointer_objectt(new_type, old.is_top(), old.is_bottom()),
+    value_stack(old.value_stack)
 {
 }
 
@@ -121,6 +123,10 @@ void constant_pointer_abstract_objectt::output(
 
         out << symbol_pointed_to.get_identifier();
       }
+      else if(addressee.id() == ID_dynamic_object)
+      {
+        out << "heap allocation";
+      }
       else if(addressee.id() == ID_index)
       {
         auto const &array_index = to_index_expr(addressee);
@@ -209,6 +215,13 @@ abstract_object_pointert constant_pointer_abstract_objectt::write_dereference(
   }
 }
 
+abstract_object_pointert
+constant_pointer_abstract_objectt::typecast(const typet &new_type) const
+{
+  INVARIANT(is_void_pointer(type()), "Only allow pointer casting from void*");
+  return std::make_shared<constant_pointer_abstract_objectt>(new_type, *this);
+}
+
 void constant_pointer_abstract_objectt::get_statistics(
   abstract_object_statisticst &statistics,
   abstract_object_visitedt &visited,
diff --git a/src/analyses/variable-sensitivity/constant_pointer_abstract_object.h b/src/analyses/variable-sensitivity/constant_pointer_abstract_object.h
index baf09eba2bc..34645ac075a 100644
--- a/src/analyses/variable-sensitivity/constant_pointer_abstract_object.h
+++ b/src/analyses/variable-sensitivity/constant_pointer_abstract_object.h
@@ -34,8 +34,8 @@ class constant_pointer_abstract_objectt : public abstract_pointer_objectt
   /// Asserts if both top and bottom are true
   constant_pointer_abstract_objectt(const typet &type, bool top, bool bottom);
 
-  /// \param old: the abstract object to copy from
   constant_pointer_abstract_objectt(
+    const typet &type,
     const constant_pointer_abstract_objectt &old);
 
   /// \param expr: the expression to use as the starting pointer for
@@ -106,6 +106,8 @@ class constant_pointer_abstract_objectt : public abstract_pointer_objectt
     const abstract_object_pointert &value,
     bool merging_write) const override;
 
+  abstract_object_pointert typecast(const typet &new_type) const override;
+
   void get_statistics(
     abstract_object_statisticst &statistics,
     abstract_object_visitedt &visited,
diff --git a/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp b/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp
index 07fc3fab966..14f2d5a00de 100644
--- a/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp
+++ b/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp
@@ -12,6 +12,7 @@
 #include <analyses/variable-sensitivity/constant_pointer_abstract_object.h>
 #include <analyses/variable-sensitivity/context_abstract_object.h>
 #include <analyses/variable-sensitivity/value_set_pointer_abstract_object.h>
+#include <util/pointer_expr.h>
 
 #include "abstract_environment.h"
 
@@ -68,6 +69,14 @@ value_set_pointer_abstract_objectt::value_set_pointer_abstract_objectt(
   values.insert(std::make_shared<constant_pointer_abstract_objectt>(type));
 }
 
+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)
+{
+}
+
 value_set_pointer_abstract_objectt::value_set_pointer_abstract_objectt(
   const typet &type,
   bool top,
@@ -133,6 +142,13 @@ abstract_object_pointert value_set_pointer_abstract_objectt::write_dereference(
   return shared_from_this();
 }
 
+abstract_object_pointert
+value_set_pointer_abstract_objectt::typecast(const typet &new_type) 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_pointert value_set_pointer_abstract_objectt::resolve_values(
   const abstract_object_sett &new_values) const
 {
diff --git a/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.h b/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.h
index bce89cafbed..c54fb4c9e6a 100644
--- a/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.h
+++ b/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.h
@@ -22,6 +22,10 @@ class value_set_pointer_abstract_objectt : public abstract_pointer_objectt,
   /// \copydoc abstract_objectt::abstract_objectt(const typet&)
   explicit value_set_pointer_abstract_objectt(const typet &type);
 
+  value_set_pointer_abstract_objectt(
+    const typet &new_type,
+    const value_set_pointer_abstract_objectt &old);
+
   /// \copydoc abstract_objectt::abstract_objectt(const typet &, bool, bool)
   value_set_pointer_abstract_objectt(const typet &type, bool top, bool bottom);
 
@@ -64,6 +68,8 @@ class value_set_pointer_abstract_objectt : public abstract_pointer_objectt,
     const abstract_object_pointert &new_value,
     bool merging_write) const override;
 
+  abstract_object_pointert typecast(const typet &new_type) const override;
+
   void output(std::ostream &out, const ai_baset &ai, const namespacet &ns)
     const override;
 

From f018cf94d4e761315028853155000cf41ffc4696 Mon Sep 17 00:00:00 2001
From: Jez Higgins <jez@jezuk.co.uk>
Date: Fri, 9 Jul 2021 10:11:18 +0100
Subject: [PATCH 03/12] Create heap allocation abstract object on pointer
 typecast

We can't ensure the modified pointer object will be properly assigned
back to its symbol if we wait until first write.

If we defer then modified pointer may, or may not, be assigned depending
on how the write is expressed

 *p = 1;   // good :)
 p[0] = 1; // bad :(
---
 .../heap-allocation-write/main.c              | 14 ++++++++
 .../test-constant-pointers.desc               |  9 ++++++
 .../test-two-value-pointers.desc              |  9 ++++++
 .../test-constant-pointers.desc               |  2 +-
 .../abstract_pointer_object.cpp               |  8 +++--
 .../abstract_pointer_object.h                 |  5 ++-
 .../constant_pointer_abstract_object.cpp      | 32 ++++++++++++++++---
 .../constant_pointer_abstract_object.h        |  5 ++-
 .../value_set_pointer_abstract_object.cpp     |  6 ++--
 .../value_set_pointer_abstract_object.h       |  5 ++-
 10 files changed, 81 insertions(+), 14 deletions(-)
 create mode 100644 regression/goto-analyzer/heap-allocation-write/main.c
 create mode 100644 regression/goto-analyzer/heap-allocation-write/test-constant-pointers.desc
 create mode 100644 regression/goto-analyzer/heap-allocation-write/test-two-value-pointers.desc

diff --git a/regression/goto-analyzer/heap-allocation-write/main.c b/regression/goto-analyzer/heap-allocation-write/main.c
new file mode 100644
index 00000000000..45d67e58415
--- /dev/null
+++ b/regression/goto-analyzer/heap-allocation-write/main.c
@@ -0,0 +1,14 @@
+
+int main() {
+  int* i_was_malloced = malloc(sizeof(int) * 10);
+  int* alias = i_was_malloced;
+
+  *i_was_malloced = 99;
+  assert(*alias == 99);
+
+  i_was_malloced[0] = 100;
+  assert(*alias == 100);
+
+  *alias += 1;
+  assert(i_was_malloced[0] == 101);
+}
diff --git a/regression/goto-analyzer/heap-allocation-write/test-constant-pointers.desc b/regression/goto-analyzer/heap-allocation-write/test-constant-pointers.desc
new file mode 100644
index 00000000000..2596b4ecffc
--- /dev/null
+++ b/regression/goto-analyzer/heap-allocation-write/test-constant-pointers.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+--variable-sensitivity --vsd-pointers constants --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.* == 101: SUCCESS
+--
diff --git a/regression/goto-analyzer/heap-allocation-write/test-two-value-pointers.desc b/regression/goto-analyzer/heap-allocation-write/test-two-value-pointers.desc
new file mode 100644
index 00000000000..f1a6ce1bc8d
--- /dev/null
+++ b/regression/goto-analyzer/heap-allocation-write/test-two-value-pointers.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+--variable-sensitivity --vsd-pointers top-bottom --vsd-arrays every-element --verify
+^EXIT=0$
+^SIGNAL=0$
+\[main.assertion.1\] .*alias == 99: UNKNOWN
+\[main.assertion.2\] .*alias == 100: UNKNOWN
+\[main.assertion.3\] .*i_was_malloced.* == 101: UNKNOWN
+--
diff --git a/regression/goto-analyzer/heap-allocation/test-constant-pointers.desc b/regression/goto-analyzer/heap-allocation/test-constant-pointers.desc
index 7f155c6696d..dc7180016df 100644
--- a/regression/goto-analyzer/heap-allocation/test-constant-pointers.desc
+++ b/regression/goto-analyzer/heap-allocation/test-constant-pointers.desc
@@ -3,5 +3,5 @@ main.c
 --variable-sensitivity --vsd-pointers constants --show
 ^EXIT=0$
 ^SIGNAL=0$
-main::1::i_was_malloced \(\) -> ptr ->\(heap allocation\)
+main::1::i_was_malloced \(\) -> ptr ->\(heap-object\[0\]\)
 --
diff --git a/src/analyses/variable-sensitivity/abstract_pointer_object.cpp b/src/analyses/variable-sensitivity/abstract_pointer_object.cpp
index 3dbcd8cf166..5fec2cfa6ca 100644
--- a/src/analyses/variable-sensitivity/abstract_pointer_object.cpp
+++ b/src/analyses/variable-sensitivity/abstract_pointer_object.cpp
@@ -55,7 +55,7 @@ abstract_object_pointert abstract_pointer_objectt::expression_transform(
       auto pointer = std::dynamic_pointer_cast<const abstract_pointer_objectt>(
         obj->unwrap_context());
       if(pointer)
-        return pointer->typecast(tce.type());
+        return pointer->typecast(tce.type(), environment, ns);
     }
   }
 
@@ -100,8 +100,10 @@ abstract_object_pointert abstract_pointer_objectt::write_dereference(
   return std::make_shared<abstract_pointer_objectt>(type(), true, false);
 }
 
-abstract_object_pointert
-abstract_pointer_objectt::typecast(const typet &new_type) const
+abstract_object_pointert abstract_pointer_objectt::typecast(
+  const typet &new_type,
+  const abstract_environmentt &environment,
+  const namespacet &ns) const
 {
   INVARIANT(is_void_pointer(type()), "Only allow pointer casting from void*");
   return std::make_shared<abstract_pointer_objectt>(
diff --git a/src/analyses/variable-sensitivity/abstract_pointer_object.h b/src/analyses/variable-sensitivity/abstract_pointer_object.h
index 0af41cf1a43..6ce6966b1ef 100644
--- a/src/analyses/variable-sensitivity/abstract_pointer_object.h
+++ b/src/analyses/variable-sensitivity/abstract_pointer_object.h
@@ -96,7 +96,10 @@ class abstract_pointer_objectt : public abstract_objectt,
     const abstract_object_pointert &value,
     bool merging_write) const;
 
-  virtual abstract_object_pointert typecast(const typet &new_type) const;
+  virtual abstract_object_pointert typecast(
+    const typet &new_type,
+    const abstract_environmentt &environment,
+    const namespacet &ns) const;
 };
 
 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_ABSTRACT_POINTER_OBJECT_H
diff --git a/src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp b/src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp
index fac7c692eb4..58ec3e70217 100644
--- a/src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp
+++ b/src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp
@@ -9,6 +9,8 @@
 #include "constant_pointer_abstract_object.h"
 
 #include <analyses/variable-sensitivity/abstract_environment.h>
+#include <util/arith_tools.h>
+#include <util/c_types.h>
 #include <util/pointer_expr.h>
 #include <util/std_expr.h>
 
@@ -207,18 +209,38 @@ abstract_object_pointert constant_pointer_abstract_objectt::write_dereference(
       abstract_object_pointert modified_value =
         environment.write(pointed_value, new_value, stack, ns, merging_write);
       environment.assign(value, modified_value, ns);
-
       // but the pointer itself does not change!
     }
-    return std::dynamic_pointer_cast<const constant_pointer_abstract_objectt>(
-      shared_from_this());
+
+    return shared_from_this();
   }
 }
 
-abstract_object_pointert
-constant_pointer_abstract_objectt::typecast(const typet &new_type) const
+abstract_object_pointert constant_pointer_abstract_objectt::typecast(
+  const typet &new_type,
+  const abstract_environmentt &environment,
+  const namespacet &ns) const
 {
   INVARIANT(is_void_pointer(type()), "Only allow pointer casting from void*");
+
+  // Get an expression that we can assign to
+  exprt value = to_address_of_expr(value_stack.to_expression()).object();
+  if(value.id() == ID_dynamic_object)
+  {
+    auto &env = const_cast<abstract_environmentt &>(environment);
+
+    auto heap_array_type = array_typet(new_type.subtype(), nil_exprt());
+    auto array_object =
+      environment.abstract_object_factory(heap_array_type, ns, true, false);
+    auto heap_symbol = symbol_exprt("heap-object", heap_array_type);
+    env.assign(heap_symbol, array_object, ns);
+    auto heap_address =
+      address_of_exprt(index_exprt(heap_symbol, from_integer(0, size_type())));
+    auto new_pointer = std::make_shared<constant_pointer_abstract_objectt>(
+      heap_address, env, ns);
+    return new_pointer;
+  }
+
   return std::make_shared<constant_pointer_abstract_objectt>(new_type, *this);
 }
 
diff --git a/src/analyses/variable-sensitivity/constant_pointer_abstract_object.h b/src/analyses/variable-sensitivity/constant_pointer_abstract_object.h
index 34645ac075a..8ea94a645c8 100644
--- a/src/analyses/variable-sensitivity/constant_pointer_abstract_object.h
+++ b/src/analyses/variable-sensitivity/constant_pointer_abstract_object.h
@@ -106,7 +106,10 @@ class constant_pointer_abstract_objectt : public abstract_pointer_objectt
     const abstract_object_pointert &value,
     bool merging_write) const override;
 
-  abstract_object_pointert typecast(const typet &new_type) const override;
+  abstract_object_pointert typecast(
+    const typet &new_type,
+    const abstract_environmentt &environment,
+    const namespacet &ns) const override;
 
   void get_statistics(
     abstract_object_statisticst &statistics,
diff --git a/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp b/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp
index 14f2d5a00de..9f398cd469f 100644
--- a/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp
+++ b/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp
@@ -142,8 +142,10 @@ abstract_object_pointert value_set_pointer_abstract_objectt::write_dereference(
   return shared_from_this();
 }
 
-abstract_object_pointert
-value_set_pointer_abstract_objectt::typecast(const typet &new_type) const
+abstract_object_pointert value_set_pointer_abstract_objectt::typecast(
+  const typet &new_type,
+  const abstract_environmentt &environment,
+  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);
diff --git a/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.h b/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.h
index c54fb4c9e6a..38b9f7fc045 100644
--- a/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.h
+++ b/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.h
@@ -68,7 +68,10 @@ class value_set_pointer_abstract_objectt : public abstract_pointer_objectt,
     const abstract_object_pointert &new_value,
     bool merging_write) const override;
 
-  abstract_object_pointert typecast(const typet &new_type) const override;
+  abstract_object_pointert typecast(
+    const typet &new_type,
+    const abstract_environmentt &environment,
+    const namespacet &ns) const override;
 
   void output(std::ostream &out, const ai_baset &ai, const namespacet &ns)
     const override;

From 791d0421f9a4e94e16d62491a45e29917db6b5e0 Mon Sep 17 00:00:00 2001
From: Jez Higgins <jez@jezuk.co.uk>
Date: Fri, 9 Jul 2021 11:09:06 +0100
Subject: [PATCH 04/12] heap object index expression needs to be
 signed_size_type

---
 regression/goto-analyzer/heap-allocation-write/main.c  | 10 +++++++---
 .../heap-allocation-write/test-constant-pointers.desc  |  3 ++-
 .../heap-allocation-write/test-two-value-pointers.desc |  3 ++-
 .../constant_pointer_abstract_object.cpp               |  4 ++--
 4 files changed, 13 insertions(+), 7 deletions(-)

diff --git a/regression/goto-analyzer/heap-allocation-write/main.c b/regression/goto-analyzer/heap-allocation-write/main.c
index 45d67e58415..6019ab2f1d7 100644
--- a/regression/goto-analyzer/heap-allocation-write/main.c
+++ b/regression/goto-analyzer/heap-allocation-write/main.c
@@ -1,7 +1,8 @@
 
-int main() {
-  int* i_was_malloced = malloc(sizeof(int) * 10);
-  int* alias = i_was_malloced;
+int main()
+{
+  int *i_was_malloced = malloc(sizeof(int) * 10);
+  int *alias = i_was_malloced;
 
   *i_was_malloced = 99;
   assert(*alias == 99);
@@ -11,4 +12,7 @@ int main() {
 
   *alias += 1;
   assert(i_was_malloced[0] == 101);
+
+  i_was_malloced[1] = 102;
+  assert(alias[1] == 102);
 }
diff --git a/regression/goto-analyzer/heap-allocation-write/test-constant-pointers.desc b/regression/goto-analyzer/heap-allocation-write/test-constant-pointers.desc
index 2596b4ecffc..0aaca9a8b72 100644
--- a/regression/goto-analyzer/heap-allocation-write/test-constant-pointers.desc
+++ b/regression/goto-analyzer/heap-allocation-write/test-constant-pointers.desc
@@ -5,5 +5,6 @@ main.c
 ^SIGNAL=0$
 \[main.assertion.1\] .*alias == 99: SUCCESS
 \[main.assertion.2\] .*alias == 100: SUCCESS
-\[main.assertion.3\] .*i_was_malloced.* == 101: SUCCESS
+\[main.assertion.3\] .*i_was_malloced\[.*0\] == 101: SUCCESS
+\[main.assertion.4\] .*alias\[.*1\] == 102: SUCCESS
 --
diff --git a/regression/goto-analyzer/heap-allocation-write/test-two-value-pointers.desc b/regression/goto-analyzer/heap-allocation-write/test-two-value-pointers.desc
index f1a6ce1bc8d..8aa9ea66315 100644
--- a/regression/goto-analyzer/heap-allocation-write/test-two-value-pointers.desc
+++ b/regression/goto-analyzer/heap-allocation-write/test-two-value-pointers.desc
@@ -5,5 +5,6 @@ main.c
 ^SIGNAL=0$
 \[main.assertion.1\] .*alias == 99: UNKNOWN
 \[main.assertion.2\] .*alias == 100: UNKNOWN
-\[main.assertion.3\] .*i_was_malloced.* == 101: UNKNOWN
+\[main.assertion.3\] .*i_was_malloced\[.*0\] == 101: UNKNOWN
+\[main.assertion.4\] .*alias\[.*1\] == 102: UNKNOWN
 --
diff --git a/src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp b/src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp
index 58ec3e70217..3389c58fbdd 100644
--- a/src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp
+++ b/src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp
@@ -234,8 +234,8 @@ abstract_object_pointert constant_pointer_abstract_objectt::typecast(
       environment.abstract_object_factory(heap_array_type, ns, true, false);
     auto heap_symbol = symbol_exprt("heap-object", heap_array_type);
     env.assign(heap_symbol, array_object, ns);
-    auto heap_address =
-      address_of_exprt(index_exprt(heap_symbol, from_integer(0, size_type())));
+    auto heap_address = address_of_exprt(
+      index_exprt(heap_symbol, from_integer(0, signed_size_type())));
     auto new_pointer = std::make_shared<constant_pointer_abstract_objectt>(
       heap_address, env, ns);
     return new_pointer;

From ed910a29790f2a484058fbe5b6c9a487390076ba Mon Sep 17 00:00:00 2001
From: Jez Higgins <jez@jezuk.co.uk>
Date: Fri, 9 Jul 2021 11:10:44 +0100
Subject: [PATCH 05/12] Index expression should used signed_size_type rather
 than size_type

I based my code in the previous commit on this code, but then found it
caused a type error. This leads me to believe that while this current
code path may not be called in normal usage, it is in fact a latent bug.
I believe this change is correct.
---
 src/analyses/variable-sensitivity/write_stack.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/analyses/variable-sensitivity/write_stack.cpp b/src/analyses/variable-sensitivity/write_stack.cpp
index f632d5d7f5d..60b7847ca93 100644
--- a/src/analyses/variable-sensitivity/write_stack.cpp
+++ b/src/analyses/variable-sensitivity/write_stack.cpp
@@ -39,10 +39,10 @@ write_stackt::write_stackt(
   if(expr.type().id() == ID_array)
   {
     // We are assigning an array to a pointer, which is equivalent to assigning
-    // the first element of that arary
+    // the first element of that array
     // &(expr)[0]
     construct_stack_to_pointer(
-      address_of_exprt(index_exprt(expr, from_integer(0, size_type()))),
+      address_of_exprt(index_exprt(expr, from_integer(0, signed_size_type()))),
       environment,
       ns);
   }

From a2e84399054da33dabaffb55778649ed730da97a Mon Sep 17 00:00:00 2001
From: Jez Higgins <jez@jezuk.co.uk>
Date: Fri, 9 Jul 2021 12:59:04 +0100
Subject: [PATCH 06/12] Create symbol name on heap allocation

---
 .../heap-allocation/test-constant-pointers.desc             | 2 +-
 .../heap-allocation/test-value-set-pointers.desc            | 2 +-
 src/analyses/variable-sensitivity/abstract_environment.cpp  | 6 ++++--
 .../constant_pointer_abstract_object.cpp                    | 4 ++--
 4 files changed, 8 insertions(+), 6 deletions(-)

diff --git a/regression/goto-analyzer/heap-allocation/test-constant-pointers.desc b/regression/goto-analyzer/heap-allocation/test-constant-pointers.desc
index dc7180016df..28c6791429c 100644
--- a/regression/goto-analyzer/heap-allocation/test-constant-pointers.desc
+++ b/regression/goto-analyzer/heap-allocation/test-constant-pointers.desc
@@ -3,5 +3,5 @@ main.c
 --variable-sensitivity --vsd-pointers constants --show
 ^EXIT=0$
 ^SIGNAL=0$
-main::1::i_was_malloced \(\) -> ptr ->\(heap-object\[0\]\)
+main::1::i_was_malloced \(\) -> ptr ->\(allocated-on-heap\[0\]\)
 --
diff --git a/regression/goto-analyzer/heap-allocation/test-value-set-pointers.desc b/regression/goto-analyzer/heap-allocation/test-value-set-pointers.desc
index 4cd2205b362..a1c19e1b6ef 100644
--- a/regression/goto-analyzer/heap-allocation/test-value-set-pointers.desc
+++ b/regression/goto-analyzer/heap-allocation/test-value-set-pointers.desc
@@ -3,5 +3,5 @@ main.c
 --variable-sensitivity --vsd-pointers value-set --show
 ^EXIT=0$
 ^SIGNAL=0$
-main::1::i_was_malloced \(\) -> value-set-begin: ptr ->\(heap allocation\) :value-set-end
+main::1::i_was_malloced \(\) -> value-set-begin: ptr ->\(allocated-on-heap\) :value-set-end
 --
diff --git a/src/analyses/variable-sensitivity/abstract_environment.cpp b/src/analyses/variable-sensitivity/abstract_environment.cpp
index abb0c03010f..c80b4119563 100644
--- a/src/analyses/variable-sensitivity/abstract_environment.cpp
+++ b/src/analyses/variable-sensitivity/abstract_environment.cpp
@@ -88,8 +88,10 @@ abstract_environmentt::eval(const exprt &expr, const namespacet &ns) const
     simplified_id == ID_side_effect &&
     (simplified_expr.get(ID_statement) == ID_allocate))
   {
-    auto heap_symbol = unary_exprt(
-      ID_address_of, exprt(ID_dynamic_object), simplified_expr.type());
+    auto dynamic_object = exprt(ID_dynamic_object);
+    dynamic_object.set(ID_identifier, "allocated-on-heap");
+    auto heap_symbol =
+      unary_exprt(ID_address_of, dynamic_object, simplified_expr.type());
     auto heap_pointer =
       abstract_object_factory(simplified_expr.type(), heap_symbol, ns);
     return heap_pointer;
diff --git a/src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp b/src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp
index 3389c58fbdd..9519e2ada51 100644
--- a/src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp
+++ b/src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp
@@ -127,7 +127,7 @@ void constant_pointer_abstract_objectt::output(
       }
       else if(addressee.id() == ID_dynamic_object)
       {
-        out << "heap allocation";
+        out << addressee.get(ID_identifier);
       }
       else if(addressee.id() == ID_index)
       {
@@ -232,7 +232,7 @@ abstract_object_pointert constant_pointer_abstract_objectt::typecast(
     auto heap_array_type = array_typet(new_type.subtype(), nil_exprt());
     auto array_object =
       environment.abstract_object_factory(heap_array_type, ns, true, false);
-    auto heap_symbol = symbol_exprt("heap-object", heap_array_type);
+    auto heap_symbol = symbol_exprt(value.get(ID_identifier), heap_array_type);
     env.assign(heap_symbol, array_object, ns);
     auto heap_address = address_of_exprt(
       index_exprt(heap_symbol, from_integer(0, signed_size_type())));

From 4acb53394d14f5542935e4f8935b31193f18269a Mon Sep 17 00:00:00 2001
From: Jez Higgins <jez@jezuk.co.uk>
Date: Fri, 9 Jul 2021 13:09:57 +0100
Subject: [PATCH 07/12] Move heap object creation off into object factory.

This feels like the right place for this, and also gives future options
for configuration/customisation.
---
 .../variable-sensitivity/abstract_environment.cpp  | 11 ++++-------
 .../variable_sensitivity_configuration.h           |  3 ++-
 .../variable_sensitivity_object_factory.cpp        | 14 ++++++++++++++
 3 files changed, 20 insertions(+), 8 deletions(-)

diff --git a/src/analyses/variable-sensitivity/abstract_environment.cpp b/src/analyses/variable-sensitivity/abstract_environment.cpp
index c80b4119563..4723bec5e24 100644
--- a/src/analyses/variable-sensitivity/abstract_environment.cpp
+++ b/src/analyses/variable-sensitivity/abstract_environment.cpp
@@ -88,13 +88,10 @@ abstract_environmentt::eval(const exprt &expr, const namespacet &ns) const
     simplified_id == ID_side_effect &&
     (simplified_expr.get(ID_statement) == ID_allocate))
   {
-    auto dynamic_object = exprt(ID_dynamic_object);
-    dynamic_object.set(ID_identifier, "allocated-on-heap");
-    auto heap_symbol =
-      unary_exprt(ID_address_of, dynamic_object, simplified_expr.type());
-    auto heap_pointer =
-      abstract_object_factory(simplified_expr.type(), heap_symbol, ns);
-    return heap_pointer;
+    return abstract_object_factory(
+      typet(ID_dynamic_object),
+      exprt(ID_dynamic_object, simplified_expr.type()),
+      ns);
   }
 
   // No special handling required by the abstract environment
diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_configuration.h b/src/analyses/variable-sensitivity/variable_sensitivity_configuration.h
index c7dd990bc79..f5d7415cd81 100644
--- a/src/analyses/variable-sensitivity/variable_sensitivity_configuration.h
+++ b/src/analyses/variable-sensitivity/variable_sensitivity_configuration.h
@@ -31,7 +31,8 @@ enum ABSTRACT_OBJECT_TYPET
   STRUCT_INSENSITIVE,
   // TODO: plug in UNION_SENSITIVE HERE
   UNION_INSENSITIVE,
-  VALUE_SET
+  VALUE_SET,
+  HEAP_ALLOCATION
 };
 
 enum class flow_sensitivityt
diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp b/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp
index 4bb1a8cfd16..815e889d517 100644
--- a/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp
+++ b/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp
@@ -114,6 +114,10 @@ variable_sensitivity_object_factoryt::get_abstract_object_type(
   {
     return configuration.union_abstract_type;
   }
+  else if(type.id() == ID_dynamic_object)
+  {
+    return HEAP_ALLOCATION;
+  }
 
   return abstract_object_type;
 }
@@ -174,6 +178,16 @@ variable_sensitivity_object_factoryt::get_abstract_object(
     return initialize_abstract_object<two_value_union_abstract_objectt>(
       followed_type, top, bottom, e, environment, ns, configuration);
 
+  case HEAP_ALLOCATION:
+  {
+    auto dynamic_object = exprt(ID_dynamic_object);
+    dynamic_object.set(ID_identifier, "allocated-on-heap");
+    auto heap_symbol = unary_exprt(ID_address_of, dynamic_object, e.type());
+    auto heap_pointer =
+      get_abstract_object(e.type(), false, false, heap_symbol, environment, ns);
+    return heap_pointer;
+  }
+
   default:
     UNREACHABLE;
     return initialize_abstract_object<abstract_objectt>(

From dc7fb2c132b9a9888ac275465fe3ea39b79756e8 Mon Sep 17 00:00:00 2001
From: Jez Higgins <jez@jezuk.co.uk>
Date: Fri, 9 Jul 2021 13:38:01 +0100
Subject: [PATCH 08/12] Create new symbol for each heap-allocation

---
 .../heap-allocation-write-2/main.c            | 19 +++++++++++++++++++
 .../test-constant-pointers.desc               | 10 ++++++++++
 .../test-two-value-pointers.desc              | 10 ++++++++++
 .../goto-analyzer/heap-allocation/main.c      |  5 ++---
 .../test-constant-pointers.desc               |  3 ++-
 .../test-two-value-pointers.desc              |  3 ++-
 .../test-value-set-pointers.desc              |  3 ++-
 .../variable_sensitivity_object_factory.cpp   |  3 ++-
 .../variable_sensitivity_object_factory.h     |  3 ++-
 9 files changed, 51 insertions(+), 8 deletions(-)
 create mode 100644 regression/goto-analyzer/heap-allocation-write-2/main.c
 create mode 100644 regression/goto-analyzer/heap-allocation-write-2/test-constant-pointers.desc
 create mode 100644 regression/goto-analyzer/heap-allocation-write-2/test-two-value-pointers.desc

diff --git a/regression/goto-analyzer/heap-allocation-write-2/main.c b/regression/goto-analyzer/heap-allocation-write-2/main.c
new file mode 100644
index 00000000000..8666d600ab3
--- /dev/null
+++ b/regression/goto-analyzer/heap-allocation-write-2/main.c
@@ -0,0 +1,19 @@
+
+int main() {
+  int *p = malloc(sizeof(int) * 5);
+  int* q = malloc(sizeof(int) * 10);
+
+  int* pp = p;
+
+  *p = 10;
+  ++p;
+  *p = 20;
+
+  q[0] = 100;
+  q[99] = 101;
+
+  assert(pp[0] == 10);
+  assert(pp[1] == 20);
+  assert(q[0] == 100);
+  assert(q[99] == 101);
+}
diff --git a/regression/goto-analyzer/heap-allocation-write-2/test-constant-pointers.desc b/regression/goto-analyzer/heap-allocation-write-2/test-constant-pointers.desc
new file mode 100644
index 00000000000..dcd33598351
--- /dev/null
+++ b/regression/goto-analyzer/heap-allocation-write-2/test-constant-pointers.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--variable-sensitivity --vsd-pointers constants --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
+--
diff --git a/regression/goto-analyzer/heap-allocation-write-2/test-two-value-pointers.desc b/regression/goto-analyzer/heap-allocation-write-2/test-two-value-pointers.desc
new file mode 100644
index 00000000000..474b957707e
--- /dev/null
+++ b/regression/goto-analyzer/heap-allocation-write-2/test-two-value-pointers.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--variable-sensitivity --vsd-pointers top-bottom --vsd-arrays every-element --verify
+^EXIT=0$
+^SIGNAL=0$
+\[main.assertion.1\] .*p\[.*0\] == 10: UNKNOWN
+\[main.assertion.2\] .*p\[.*1\] == 20: UNKNOWN
+\[main.assertion.3\] .*q\[.*0\] == 100: UNKNOWN
+\[main.assertion.4\] .*q\[.*99\] == 101: UNKNOWN
+--
diff --git a/regression/goto-analyzer/heap-allocation/main.c b/regression/goto-analyzer/heap-allocation/main.c
index 6b4a712b016..c09abc337b8 100644
--- a/regression/goto-analyzer/heap-allocation/main.c
+++ b/regression/goto-analyzer/heap-allocation/main.c
@@ -1,7 +1,6 @@
 
 int main()
 {
-  int *i_was_malloced = malloc(sizeof(int) * 10);
-
-  // q[0] = 99;
+  int *p = malloc(sizeof(int) * 10);
+  int *q = malloc(sizeof(int) * 5);
 }
diff --git a/regression/goto-analyzer/heap-allocation/test-constant-pointers.desc b/regression/goto-analyzer/heap-allocation/test-constant-pointers.desc
index 28c6791429c..8379e910976 100644
--- a/regression/goto-analyzer/heap-allocation/test-constant-pointers.desc
+++ b/regression/goto-analyzer/heap-allocation/test-constant-pointers.desc
@@ -3,5 +3,6 @@ main.c
 --variable-sensitivity --vsd-pointers constants --show
 ^EXIT=0$
 ^SIGNAL=0$
-main::1::i_was_malloced \(\) -> ptr ->\(allocated-on-heap\[0\]\)
+main::1::p \(\) -> ptr ->\(heap-allocation-0\[0\]\)
+main::1::q \(\) -> ptr ->\(heap-allocation-1\[0\]\)
 --
diff --git a/regression/goto-analyzer/heap-allocation/test-two-value-pointers.desc b/regression/goto-analyzer/heap-allocation/test-two-value-pointers.desc
index 7de42fea4c0..9329e3a9ced 100644
--- a/regression/goto-analyzer/heap-allocation/test-two-value-pointers.desc
+++ b/regression/goto-analyzer/heap-allocation/test-two-value-pointers.desc
@@ -3,5 +3,6 @@ main.c
 --variable-sensitivity --vsd-pointers top-bottom --show
 ^EXIT=0$
 ^SIGNAL=0$
-main::1::i_was_malloced \(\) -> TOP
+main::1::p \(\) -> TOP
+main::1::q \(\) -> TOP
 --
diff --git a/regression/goto-analyzer/heap-allocation/test-value-set-pointers.desc b/regression/goto-analyzer/heap-allocation/test-value-set-pointers.desc
index a1c19e1b6ef..3003f5a497c 100644
--- a/regression/goto-analyzer/heap-allocation/test-value-set-pointers.desc
+++ b/regression/goto-analyzer/heap-allocation/test-value-set-pointers.desc
@@ -3,5 +3,6 @@ main.c
 --variable-sensitivity --vsd-pointers value-set --show
 ^EXIT=0$
 ^SIGNAL=0$
-main::1::i_was_malloced \(\) -> value-set-begin: ptr ->\(allocated-on-heap\) :value-set-end
+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
 --
diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp b/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp
index 815e889d517..551a6373450 100644
--- a/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp
+++ b/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp
@@ -181,7 +181,8 @@ variable_sensitivity_object_factoryt::get_abstract_object(
   case HEAP_ALLOCATION:
   {
     auto dynamic_object = exprt(ID_dynamic_object);
-    dynamic_object.set(ID_identifier, "allocated-on-heap");
+    dynamic_object.set(
+      ID_identifier, "heap-allocation-" + std::to_string(heap_allocations++));
     auto heap_symbol = unary_exprt(ID_address_of, dynamic_object, e.type());
     auto heap_pointer =
       get_abstract_object(e.type(), false, false, heap_symbol, environment, ns);
diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.h b/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.h
index edfe5c1b22e..2d4a1143892 100644
--- a/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.h
+++ b/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.h
@@ -44,7 +44,7 @@ class variable_sensitivity_object_factoryt
   }
 
   explicit variable_sensitivity_object_factoryt(const vsd_configt &options)
-    : configuration{options}
+    : configuration{options}, heap_allocations(0)
   {
   }
 
@@ -87,6 +87,7 @@ class variable_sensitivity_object_factoryt
   ABSTRACT_OBJECT_TYPET get_abstract_object_type(const typet &type) const;
 
   vsd_configt configuration;
+  mutable size_t heap_allocations;
 };
 
 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VARIABLE_SENSITIVITY_OBJECT_FACTORY_H // NOLINT(*)

From 786e2a28c1526b07bff086af3e9bf0ab28bfa1fa Mon Sep 17 00:00:00 2001
From: Jez Higgins <jez@jezuk.co.uk>
Date: Fri, 9 Jul 2021 13:49:29 +0100
Subject: [PATCH 09/12] remove redundant apply_comb template

---
 .../value_set_pointer_abstract_object.cpp     | 37 -------------------
 1 file changed, 37 deletions(-)

diff --git a/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp b/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp
index 9f398cd469f..aa706a6d69d 100644
--- a/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp
+++ b/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp
@@ -25,43 +25,6 @@ unwrap_and_extract_values(const abstract_object_sett &values);
 static abstract_object_pointert
 maybe_extract_single_value(const abstract_object_pointert &maybe_singleton);
 
-/// Recursively construct a combination \p sub_con from \p super_con and once
-///   constructed call \p f.
-/// \param super_con: vector of some containers storing the values
-/// \param sub_con: the one combination being currently constructed
-/// \param f: callable with side-effects
-template <typename Con, typename F>
-void apply_comb(
-  const std::vector<Con> &super_con,
-  std::vector<typename Con::value_type> &sub_con,
-  F f)
-{
-  size_t n = sub_con.size();
-  if(n == super_con.size())
-    f(sub_con);
-  else
-  {
-    for(const auto &value : super_con[n])
-    {
-      sub_con.push_back(value);
-      apply_comb(super_con, sub_con, f);
-      sub_con.pop_back();
-    }
-  }
-}
-
-/// Call the function \p f on every combination of elements in \p super_con.
-///   Hence the arity of \p f is `super_con.size()`. <{1,2},{1},{1,2,3}> ->
-///   f(1,1,1), f(1,1,2), f(1,1,3), f(2,1,1), f(2,1,2), f(2,1,3).
-/// \param super_con: vector of some containers storing the values
-/// \param f: callable with side-effects
-template <typename Con, typename F>
-void for_each_comb(const std::vector<Con> &super_con, F f)
-{
-  std::vector<typename Con::value_type> sub_con;
-  apply_comb(super_con, sub_con, f);
-}
-
 value_set_pointer_abstract_objectt::value_set_pointer_abstract_objectt(
   const typet &type)
   : abstract_pointer_objectt(type)

From 689df79a578135c1edb95161e6309387ae7b2d21 Mon Sep 17 00:00:00 2001
From: Jez Higgins <jez@jezuk.co.uk>
Date: Fri, 9 Jul 2021 14:02:05 +0100
Subject: [PATCH 10/12] Typecasting value-set of pointers needs to propagate
 down

---
 .../test-value-set-pointers.desc                | 10 ++++++++++
 .../test-value-set-pointers.desc                | 10 ++++++++++
 .../test-value-set-pointers.desc                |  4 ++--
 .../value_set_pointer_abstract_object.cpp       | 17 +++++++++++++----
 .../value_set_pointer_abstract_object.h         |  4 +++-
 5 files changed, 38 insertions(+), 7 deletions(-)
 create mode 100644 regression/goto-analyzer/heap-allocation-write-2/test-value-set-pointers.desc
 create mode 100644 regression/goto-analyzer/heap-allocation-write/test-value-set-pointers.desc

diff --git a/regression/goto-analyzer/heap-allocation-write-2/test-value-set-pointers.desc b/regression/goto-analyzer/heap-allocation-write-2/test-value-set-pointers.desc
new file mode 100644
index 00000000000..91687849c60
--- /dev/null
+++ b/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
+--
diff --git a/regression/goto-analyzer/heap-allocation-write/test-value-set-pointers.desc b/regression/goto-analyzer/heap-allocation-write/test-value-set-pointers.desc
new file mode 100644
index 00000000000..9d7320b2dc0
--- /dev/null
+++ b/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
+--
diff --git a/regression/goto-analyzer/heap-allocation/test-value-set-pointers.desc b/regression/goto-analyzer/heap-allocation/test-value-set-pointers.desc
index 3003f5a497c..d0feb9fbd22 100644
--- a/regression/goto-analyzer/heap-allocation/test-value-set-pointers.desc
+++ b/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
 --
diff --git a/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp b/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp
index aa706a6d69d..8f5ce72304d 100644
--- a/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp
+++ b/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(
diff --git a/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.h b/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.h
index 38b9f7fc045..4e33a384543 100644
--- a/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.h
+++ b/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);

From dfa01542fed3684eb787797cf8d4fddc600f1ff3 Mon Sep 17 00:00:00 2001
From: Jez Higgins <jez@jezuk.co.uk>
Date: Fri, 9 Jul 2021 14:38:29 +0100
Subject: [PATCH 11/12] heap allocation and value-set tests

---
 regression/goto-analyzer/heap-allocation-nondet-1/main.c | 9 +++++++++
 .../goto-analyzer/heap-allocation-nondet-1/test.desc     | 7 +++++++
 regression/goto-analyzer/heap-allocation-nondet-2/main.c | 6 ++++++
 .../goto-analyzer/heap-allocation-nondet-2/test.desc     | 7 +++++++
 regression/goto-analyzer/heap-allocation-nondet-3/main.c | 9 +++++++++
 .../goto-analyzer/heap-allocation-nondet-3/test.desc     | 7 +++++++
 regression/goto-analyzer/heap-allocation-nondet-4/main.c | 9 +++++++++
 .../goto-analyzer/heap-allocation-nondet-4/test.desc     | 7 +++++++
 8 files changed, 61 insertions(+)
 create mode 100644 regression/goto-analyzer/heap-allocation-nondet-1/main.c
 create mode 100644 regression/goto-analyzer/heap-allocation-nondet-1/test.desc
 create mode 100644 regression/goto-analyzer/heap-allocation-nondet-2/main.c
 create mode 100644 regression/goto-analyzer/heap-allocation-nondet-2/test.desc
 create mode 100644 regression/goto-analyzer/heap-allocation-nondet-3/main.c
 create mode 100644 regression/goto-analyzer/heap-allocation-nondet-3/test.desc
 create mode 100644 regression/goto-analyzer/heap-allocation-nondet-4/main.c
 create mode 100644 regression/goto-analyzer/heap-allocation-nondet-4/test.desc

diff --git a/regression/goto-analyzer/heap-allocation-nondet-1/main.c b/regression/goto-analyzer/heap-allocation-nondet-1/main.c
new file mode 100644
index 00000000000..b9ae05beb62
--- /dev/null
+++ b/regression/goto-analyzer/heap-allocation-nondet-1/main.c
@@ -0,0 +1,9 @@
+
+int main() {
+  int* q = malloc(10);
+  int* r = malloc(10);
+
+  int *p = r;
+  if (nondet())
+    p = q;
+}
diff --git a/regression/goto-analyzer/heap-allocation-nondet-1/test.desc b/regression/goto-analyzer/heap-allocation-nondet-1/test.desc
new file mode 100644
index 00000000000..8e2b3db203e
--- /dev/null
+++ b/regression/goto-analyzer/heap-allocation-nondet-1/test.desc
@@ -0,0 +1,7 @@
+CORE
+main.c
+--variable-sensitivity --vsd-pointers value-set --show
+^EXIT=0$
+^SIGNAL=0$
+main::1::p \(\) -> value-set-begin: ptr ->\(heap-allocation-0\[0\]\), ptr ->\(heap-allocation-1\[0\]\) :value-set-end
+--
diff --git a/regression/goto-analyzer/heap-allocation-nondet-2/main.c b/regression/goto-analyzer/heap-allocation-nondet-2/main.c
new file mode 100644
index 00000000000..b0c0a898ca6
--- /dev/null
+++ b/regression/goto-analyzer/heap-allocation-nondet-2/main.c
@@ -0,0 +1,6 @@
+
+int main() {
+  int *p = malloc(10);
+  if (nondet())
+    ++p;
+}
diff --git a/regression/goto-analyzer/heap-allocation-nondet-2/test.desc b/regression/goto-analyzer/heap-allocation-nondet-2/test.desc
new file mode 100644
index 00000000000..e74d0b420e0
--- /dev/null
+++ b/regression/goto-analyzer/heap-allocation-nondet-2/test.desc
@@ -0,0 +1,7 @@
+CORE
+main.c
+--variable-sensitivity --vsd-pointers value-set --show
+^EXIT=0$
+^SIGNAL=0$
+main::1::p \(\) -> value-set-begin: ptr ->\(heap-allocation-0\[0\]\), ptr ->\(heap-allocation-0\[1\]\) :value-set-end
+--
diff --git a/regression/goto-analyzer/heap-allocation-nondet-3/main.c b/regression/goto-analyzer/heap-allocation-nondet-3/main.c
new file mode 100644
index 00000000000..0fd52bfd79a
--- /dev/null
+++ b/regression/goto-analyzer/heap-allocation-nondet-3/main.c
@@ -0,0 +1,9 @@
+
+int main() {
+  int *q = malloc(10);
+  int r[10];
+
+  int *p = r;
+  if (nondet())
+    p = q;
+}
diff --git a/regression/goto-analyzer/heap-allocation-nondet-3/test.desc b/regression/goto-analyzer/heap-allocation-nondet-3/test.desc
new file mode 100644
index 00000000000..a1d1451339b
--- /dev/null
+++ b/regression/goto-analyzer/heap-allocation-nondet-3/test.desc
@@ -0,0 +1,7 @@
+CORE
+main.c
+--variable-sensitivity --vsd-pointers value-set --show
+^EXIT=0$
+^SIGNAL=0$
+main::1::p \(\) -> value-set-begin: ptr ->\(main::1::r\[0\]\), ptr ->\(heap-allocation-0\[0\]\) :value-set-end
+--
diff --git a/regression/goto-analyzer/heap-allocation-nondet-4/main.c b/regression/goto-analyzer/heap-allocation-nondet-4/main.c
new file mode 100644
index 00000000000..3062eb432bc
--- /dev/null
+++ b/regression/goto-analyzer/heap-allocation-nondet-4/main.c
@@ -0,0 +1,9 @@
+
+int main() {
+  int *q = malloc(10);
+  int r[10];
+
+  int *p = q;
+  if (nondet())
+    p = r;
+}
diff --git a/regression/goto-analyzer/heap-allocation-nondet-4/test.desc b/regression/goto-analyzer/heap-allocation-nondet-4/test.desc
new file mode 100644
index 00000000000..a1d1451339b
--- /dev/null
+++ b/regression/goto-analyzer/heap-allocation-nondet-4/test.desc
@@ -0,0 +1,7 @@
+CORE
+main.c
+--variable-sensitivity --vsd-pointers value-set --show
+^EXIT=0$
+^SIGNAL=0$
+main::1::p \(\) -> value-set-begin: ptr ->\(main::1::r\[0\]\), ptr ->\(heap-allocation-0\[0\]\) :value-set-end
+--

From 1a6a422a04b52e126186a46d4308a32635699b1e Mon Sep 17 00:00:00 2001
From: Jez Higgins <jez@jezuk.co.uk>
Date: Fri, 9 Jul 2021 15:07:04 +0100
Subject: [PATCH 12/12] vsp = nondet ? malloc(a) : malloc(b) works correctly

---
 regression/goto-analyzer/heap-allocation-nondet-1/main.c | 9 +++++----
 regression/goto-analyzer/heap-allocation-nondet-2/main.c | 5 +++--
 regression/goto-analyzer/heap-allocation-nondet-3/main.c | 5 +++--
 regression/goto-analyzer/heap-allocation-nondet-4/main.c | 5 +++--
 regression/goto-analyzer/heap-allocation-nondet-5/main.c | 8 ++++++++
 .../goto-analyzer/heap-allocation-nondet-5/test.desc     | 7 +++++++
 regression/goto-analyzer/heap-allocation-nondet-6/main.c | 5 +++++
 .../goto-analyzer/heap-allocation-nondet-6/test.desc     | 7 +++++++
 regression/goto-analyzer/heap-allocation-write-2/main.c  | 7 ++++---
 .../value_set_pointer_abstract_object.cpp                | 3 +++
 10 files changed, 48 insertions(+), 13 deletions(-)
 create mode 100644 regression/goto-analyzer/heap-allocation-nondet-5/main.c
 create mode 100644 regression/goto-analyzer/heap-allocation-nondet-5/test.desc
 create mode 100644 regression/goto-analyzer/heap-allocation-nondet-6/main.c
 create mode 100644 regression/goto-analyzer/heap-allocation-nondet-6/test.desc

diff --git a/regression/goto-analyzer/heap-allocation-nondet-1/main.c b/regression/goto-analyzer/heap-allocation-nondet-1/main.c
index b9ae05beb62..e022d770c6e 100644
--- a/regression/goto-analyzer/heap-allocation-nondet-1/main.c
+++ b/regression/goto-analyzer/heap-allocation-nondet-1/main.c
@@ -1,9 +1,10 @@
 
-int main() {
-  int* q = malloc(10);
-  int* r = malloc(10);
+int main()
+{
+  int *q = malloc(10);
+  int *r = malloc(10);
 
   int *p = r;
-  if (nondet())
+  if(nondet())
     p = q;
 }
diff --git a/regression/goto-analyzer/heap-allocation-nondet-2/main.c b/regression/goto-analyzer/heap-allocation-nondet-2/main.c
index b0c0a898ca6..84ef19235fe 100644
--- a/regression/goto-analyzer/heap-allocation-nondet-2/main.c
+++ b/regression/goto-analyzer/heap-allocation-nondet-2/main.c
@@ -1,6 +1,7 @@
 
-int main() {
+int main()
+{
   int *p = malloc(10);
-  if (nondet())
+  if(nondet())
     ++p;
 }
diff --git a/regression/goto-analyzer/heap-allocation-nondet-3/main.c b/regression/goto-analyzer/heap-allocation-nondet-3/main.c
index 0fd52bfd79a..d49b7ec72b7 100644
--- a/regression/goto-analyzer/heap-allocation-nondet-3/main.c
+++ b/regression/goto-analyzer/heap-allocation-nondet-3/main.c
@@ -1,9 +1,10 @@
 
-int main() {
+int main()
+{
   int *q = malloc(10);
   int r[10];
 
   int *p = r;
-  if (nondet())
+  if(nondet())
     p = q;
 }
diff --git a/regression/goto-analyzer/heap-allocation-nondet-4/main.c b/regression/goto-analyzer/heap-allocation-nondet-4/main.c
index 3062eb432bc..7870ce77aa5 100644
--- a/regression/goto-analyzer/heap-allocation-nondet-4/main.c
+++ b/regression/goto-analyzer/heap-allocation-nondet-4/main.c
@@ -1,9 +1,10 @@
 
-int main() {
+int main()
+{
   int *q = malloc(10);
   int r[10];
 
   int *p = q;
-  if (nondet())
+  if(nondet())
     p = r;
 }
diff --git a/regression/goto-analyzer/heap-allocation-nondet-5/main.c b/regression/goto-analyzer/heap-allocation-nondet-5/main.c
new file mode 100644
index 00000000000..faa8283feff
--- /dev/null
+++ b/regression/goto-analyzer/heap-allocation-nondet-5/main.c
@@ -0,0 +1,8 @@
+
+int main()
+{
+  int *p = malloc(10);
+
+  if(non_det())
+    p = malloc(20);
+}
diff --git a/regression/goto-analyzer/heap-allocation-nondet-5/test.desc b/regression/goto-analyzer/heap-allocation-nondet-5/test.desc
new file mode 100644
index 00000000000..8e2b3db203e
--- /dev/null
+++ b/regression/goto-analyzer/heap-allocation-nondet-5/test.desc
@@ -0,0 +1,7 @@
+CORE
+main.c
+--variable-sensitivity --vsd-pointers value-set --show
+^EXIT=0$
+^SIGNAL=0$
+main::1::p \(\) -> value-set-begin: ptr ->\(heap-allocation-0\[0\]\), ptr ->\(heap-allocation-1\[0\]\) :value-set-end
+--
diff --git a/regression/goto-analyzer/heap-allocation-nondet-6/main.c b/regression/goto-analyzer/heap-allocation-nondet-6/main.c
new file mode 100644
index 00000000000..8dabb4a1132
--- /dev/null
+++ b/regression/goto-analyzer/heap-allocation-nondet-6/main.c
@@ -0,0 +1,5 @@
+
+int main()
+{
+  int *p = nondet() ? malloc(10) : malloc(20);
+}
diff --git a/regression/goto-analyzer/heap-allocation-nondet-6/test.desc b/regression/goto-analyzer/heap-allocation-nondet-6/test.desc
new file mode 100644
index 00000000000..8e2b3db203e
--- /dev/null
+++ b/regression/goto-analyzer/heap-allocation-nondet-6/test.desc
@@ -0,0 +1,7 @@
+CORE
+main.c
+--variable-sensitivity --vsd-pointers value-set --show
+^EXIT=0$
+^SIGNAL=0$
+main::1::p \(\) -> value-set-begin: ptr ->\(heap-allocation-0\[0\]\), ptr ->\(heap-allocation-1\[0\]\) :value-set-end
+--
diff --git a/regression/goto-analyzer/heap-allocation-write-2/main.c b/regression/goto-analyzer/heap-allocation-write-2/main.c
index 8666d600ab3..020067294d8 100644
--- a/regression/goto-analyzer/heap-allocation-write-2/main.c
+++ b/regression/goto-analyzer/heap-allocation-write-2/main.c
@@ -1,9 +1,10 @@
 
-int main() {
+int main()
+{
   int *p = malloc(sizeof(int) * 5);
-  int* q = malloc(sizeof(int) * 10);
+  int *q = malloc(sizeof(int) * 10);
 
-  int* pp = p;
+  int *pp = p;
 
   *p = 10;
   ++p;
diff --git a/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp b/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp
index 8f5ce72304d..025d2029e09 100644
--- a/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp
+++ b/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp
@@ -115,6 +115,9 @@ abstract_object_pointert value_set_pointer_abstract_objectt::typecast(
   abstract_object_sett new_values;
   for(auto value : values)
   {
+    if(value->is_top()) // multiple mallocs in the same scope can cause spurious
+      continue; // TOP values, which we can safely strip out during the cast
+
     auto pointer =
       std::dynamic_pointer_cast<const abstract_pointer_objectt>(value);
     new_values.insert(pointer->typecast(new_type, environment, ns));