Create new symbol for each heap-allocation

Author: jezhiggins

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);
+}

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
+--

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
+--

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);
 }

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\]\)
 --

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
 --

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
 --

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);

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(*)