C/C++ library: move free/delete-only definitions to library

tautschnig · tautschnig · commit 284ae0353c74 · 2022-02-01T14:07:33.000Z
With the support of building initialisers while adding the library we
can move library-only symbols to the library. This avoids polluting the
initialisation function for all cases that don't actually use
memory (de-)allocation library functions.
diff --git a/regression/cbmc-library/alloca-02/main.c b/regression/cbmc-library/alloca-02/main.c
@@ -4,9 +4,14 @@
 void *alloca(size_t alloca_size);
 #endif
 
+// intentionally type conflicting: the built-in library uses const void*; this
+// is to check that object type updates are performed
+extern const char *__CPROVER_alloca_object;
+
 int *foo()
 {
   int *foo_ptr = alloca(sizeof(int));
+  __CPROVER_assert(foo_ptr == __CPROVER_alloca_object, "may fail");
   return foo_ptr;
 }
 
diff --git a/regression/cbmc-library/alloca-02/test.desc b/regression/cbmc-library/alloca-02/test.desc
@@ -2,7 +2,7 @@ CORE
 main.c
 --pointer-check
 dereference failure: dead object in \*from_foo: FAILURE$
-^\*\* 1 of 6 failed
+^\*\* 2 of 7 failed
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
diff --git a/regression/cbmc-library/free-01/test.desc b/regression/cbmc-library/free-01/test.desc
@@ -1,7 +1,7 @@
 CORE
 main.c
 --pointer-check --bounds-check --stop-on-fail
-free argument must be NULL or valid pointer
+free argument must be (NULL or valid pointer|dynamic object)
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/goto-analyzer/constant_propagation_01/test-vsd.desc b/regression/goto-analyzer/constant_propagation_01/test-vsd.desc
@@ -3,7 +3,7 @@ main.c
 --variable-sensitivity --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 14, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 5, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 12, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_01/test.desc b/regression/goto-analyzer/constant_propagation_01/test.desc
@@ -3,7 +3,7 @@ main.c
 --constants --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 14, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 5, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 12, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_02/test-vsd.desc b/regression/goto-analyzer/constant_propagation_02/test-vsd.desc
@@ -3,7 +3,7 @@ main.c
 --variable-sensitivity --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 13, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_02/test.desc b/regression/goto-analyzer/constant_propagation_02/test.desc
@@ -3,7 +3,7 @@ main.c
 --constants --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 13, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_03/test-vsd.desc b/regression/goto-analyzer/constant_propagation_03/test-vsd.desc
@@ -3,7 +3,7 @@ main.c
 --variable-sensitivity --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 13, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_03/test.desc b/regression/goto-analyzer/constant_propagation_03/test.desc
@@ -3,7 +3,7 @@ main.c
 --constants --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 13, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_04/test-vsd.desc b/regression/goto-analyzer/constant_propagation_04/test-vsd.desc
@@ -3,7 +3,7 @@ main.c
 --variable-sensitivity --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 13, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_04/test.desc b/regression/goto-analyzer/constant_propagation_04/test.desc
@@ -3,7 +3,7 @@ main.c
 --constants --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 13, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_07/test-vsd.desc b/regression/goto-analyzer/constant_propagation_07/test-vsd.desc
@@ -3,7 +3,7 @@ main.c
 --variable-sensitivity --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 3, assigns: 8, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 15, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 3, assigns: 7, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 13, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_07/test.desc b/regression/goto-analyzer/constant_propagation_07/test.desc
@@ -3,7 +3,7 @@ main.c
 --constants --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 3, assigns: 8, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 15, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 3, assigns: 7, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 13, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_08/test-vsd.desc b/regression/goto-analyzer/constant_propagation_08/test-vsd.desc
@@ -3,7 +3,7 @@ main.c
 --variable-sensitivity --vsd-arrays every-element --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 2, assigns: 7, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 3, assigns: 14, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 2, assigns: 6, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 3, assigns: 12, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_11/test-vsd.desc b/regression/goto-analyzer/constant_propagation_11/test-vsd.desc
@@ -3,7 +3,7 @@ main.c
 --variable-sensitivity --vsd-arrays every-element --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 11, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 9, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_11/test.desc b/regression/goto-analyzer/constant_propagation_11/test.desc
@@ -3,7 +3,7 @@ main.c
 --constants --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 11, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 9, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_12/test-vsd.desc b/regression/goto-analyzer/constant_propagation_12/test-vsd.desc
@@ -3,7 +3,7 @@ main.c
 --variable-sensitivity --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 12, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 5, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 10, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_12/test.desc b/regression/goto-analyzer/constant_propagation_12/test.desc
@@ -3,7 +3,7 @@ main.c
 --constants --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 12, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 5, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 10, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/liveness-function-call/test-liveness-show.desc b/regression/goto-analyzer/liveness-function-call/test-liveness-show.desc
@@ -3,8 +3,8 @@ main.c
 --variable-sensitivity --vsd-liveness --show
 ^EXIT=0$
 ^SIGNAL=0$
-globalX .* 0 @ \[24\]
+globalX .* 0 @ \[21\]
 globalX .* 1 @ \[0\]
 globalX .* 2 @ \[3\]
-globalX .* TOP @ \[27\]
+globalX .* TOP @ \[24\]
 --
diff --git a/regression/goto-analyzer/liveness-function-call/test-liveness-three-way-show.desc b/regression/goto-analyzer/liveness-function-call/test-liveness-three-way-show.desc
@@ -3,8 +3,8 @@ main.c
 --variable-sensitivity --vsd-liveness --three-way-merge --show
 ^EXIT=0$
 ^SIGNAL=0$
-globalX .* 0 @ \[24\]
+globalX .* 0 @ \[21\]
 globalX .* 1 @ \[0\]
 globalX .* 2 @ \[3\]
-globalX .* TOP @ \[27\]
+globalX .* TOP @ \[24\]
 --
diff --git a/regression/goto-analyzer/liveness-function-call/test-write-location-show.desc b/regression/goto-analyzer/liveness-function-call/test-write-location-show.desc
@@ -3,7 +3,7 @@ main.c
 --variable-sensitivity --show
 ^EXIT=0$
 ^SIGNAL=0$
-globalX .* 0 @ \[24\]
+globalX .* 0 @ \[21\]
 globalX .* 1 @ \[0\]
 globalX .* TOP @ \[0, 3\]
 --
diff --git a/regression/goto-analyzer/liveness-function-call/test-write-location-three-way-show.desc b/regression/goto-analyzer/liveness-function-call/test-write-location-three-way-show.desc
@@ -3,7 +3,7 @@ main.c
 --variable-sensitivity --three-way-merge --show
 ^EXIT=0$
 ^SIGNAL=0$
-globalX .* 0 @ \[24\]
+globalX .* 0 @ \[21\]
 globalX .* 1 @ \[0\]
 globalX .* 2 @ \[3\]
 --
diff --git a/regression/goto-analyzer/sensitivity-last-written-locations-arrays/test.desc b/regression/goto-analyzer/sensitivity-last-written-locations-arrays/test.desc
@@ -6,31 +6,29 @@ activate-multi-line-match
 ^EXIT=0$
 ^SIGNAL=0$
 main#return_value \(\) -> TOP @ \[1\]
-__CPROVER_dead_object \(\) -> TOP @ \[5\]
-__CPROVER_deallocated \(\) -> TOP @ \[6\]
-__CPROVER_malloc_is_new_array \(\) -> FALSE @ \[7\]
-__CPROVER_memory_leak \(\) -> TOP @ \[9\]
-__CPROVER_new_object \(\) -> TOP @ \[10\]
-__CPROVER_next_thread_key \(\) -> 0ul @ \[12\]
-__CPROVER_rounding_mode \(\) -> 0 @ \[13\]
-__CPROVER_thread_id \(\) -> 0ul @ \[14\]
-__CPROVER_threads_exited \(\) -> TOP @ \[17\]
-do_arrays::1::bool_ \(\) -> TOP @ \[19\]
-do_arrays::1::bool_1 \(\) -> TOP @ \[20\]
-do_arrays::1::bool_2 \(\) -> TOP @ \[21\]
-do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[23\]\n\} @ \[23\]
-do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[23\]\n\[1\] = 20 @ \[24\]\n\} @ \[24\]
-do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[25\]\n\[1\] = 20 @ \[24\]\n\} @ \[25\]
-do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[25\]\n\[1\] = 40 @ \[26\]\n\} @ \[26\]
-do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[25\]\n\[1\] = 30 @ \[27\]\n\} @ \[27\]
-do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[28\]\n\[1\] = 30 @ \[27\]\n\} @ \[28\]
-do_arrays::1::x \(\) -> \{\[0\] = 5 @ \[29\]\n\[1\] = 30 @ \[27\]\n\} @ \[29\]
-do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[30\]\n\[1\] = 30 @ \[27\]\n\} @ \[30\]
-do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[30\]\n\[1\] = 10 @ \[31\]\n\} @ \[31\]
-do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[33\]\n\[1\] = 10 @ \[31\]\n\} @ \[33\]
-do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[33\, 35\]\n\[1\] = 10 @ \[31\]\n\} @ \[33\, 35\]
-do_arrays::1::x \(\) -> \{\[0\] = 0 @ \[37]\n\[1\] = 10 @ \[31\]\n\} @ \[37\]
-do_arrays::1::x \(\) -> \{\[0\] = 3 @ \[39]\n\[1\] = 10 @ \[31\]\n\} @ \[39\]
-do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[39\, 41]\n\[1\] = 10 @ \[31\]\n\} @ \[39\, 41\]
-do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[39\, 41\, 44]\n\[1\] = 10 @ \[46\]\n\} @ \[46\]
-do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[47]\n\[1\] = 10 @ \[46\]\n\} @ \[47\]
+__CPROVER_dead_object \(\) -> TOP @ \[4\]
+__CPROVER_deallocated \(\) -> TOP @ \[5\]
+__CPROVER_memory_leak \(\) -> TOP @ \[7\]
+__CPROVER_next_thread_key \(\) -> 0ul @ \[9\]
+__CPROVER_rounding_mode \(\) -> 0 @ \[10\]
+__CPROVER_thread_id \(\) -> 0ul @ \[11\]
+__CPROVER_threads_exited \(\) -> TOP @ \[14\]
+do_arrays::1::bool_ \(\) -> TOP @ \[16\]
+do_arrays::1::bool_1 \(\) -> TOP @ \[17\]
+do_arrays::1::bool_2 \(\) -> TOP @ \[18\]
+do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[20\]\n\} @ \[20\]
+do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[20\]\n\[1\] = 20 @ \[21\]\n\} @ \[21\]
+do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[22\]\n\[1\] = 20 @ \[21\]\n\} @ \[22\]
+do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[22\]\n\[1\] = 40 @ \[23\]\n\} @ \[23\]
+do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[22\]\n\[1\] = 30 @ \[24\]\n\} @ \[24\]
+do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[25\]\n\[1\] = 30 @ \[24\]\n\} @ \[25\]
+do_arrays::1::x \(\) -> \{\[0\] = 5 @ \[26\]\n\[1\] = 30 @ \[24\]\n\} @ \[26\]
+do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[27\]\n\[1\] = 30 @ \[24\]\n\} @ \[27\]
+do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[27\]\n\[1\] = 10 @ \[28\]\n\} @ \[28\]
+do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[30\]\n\[1\] = 10 @ \[28\]\n\} @ \[30\]
+do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[30\, 32\]\n\[1\] = 10 @ \[28\]\n\} @ \[30\, 32\]
+do_arrays::1::x \(\) -> \{\[0\] = 0 @ \[34]\n\[1\] = 10 @ \[28\]\n\} @ \[34\]
+do_arrays::1::x \(\) -> \{\[0\] = 3 @ \[36]\n\[1\] = 10 @ \[28\]\n\} @ \[36\]
+do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[36\, 38]\n\[1\] = 10 @ \[28\]\n\} @ \[36\, 38\]
+do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[36\, 38\, 41]\n\[1\] = 10 @ \[43\]\n\} @ \[43\]
+do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[44]\n\[1\] = 10 @ \[43\]\n\} @ \[44\]
diff --git a/regression/goto-analyzer/sensitivity-last-written-locations-pointers/test.desc b/regression/goto-analyzer/sensitivity-last-written-locations-pointers/test.desc
@@ -6,30 +6,28 @@ activate-multi-line-match
 ^EXIT=0$
 ^SIGNAL=0$
 main#return_value \(\) -> TOP @ \[1\]
-__CPROVER_dead_object \(\) -> TOP @ \[5\]
-__CPROVER_deallocated \(\) -> TOP @ \[6\]
-__CPROVER_malloc_is_new_array \(\) -> FALSE @ \[7\]
-__CPROVER_memory_leak \(\) -> TOP @ \[9\]
-__CPROVER_new_object \(\) -> TOP @ \[10\]
-__CPROVER_next_thread_key \(\) -> 0ul @ \[12\]
-__CPROVER_rounding_mode \(\) -> 0 @ \[13\]
-__CPROVER_thread_id \(\) -> 0ul @ \[14\]
-__CPROVER_threads_exited \(\) -> TOP @ \[17\]
-do_pointers::1::bool_ \(\) -> TOP @ \[19\]
-do_pointers::1::bool_1 \(\) -> TOP @ \[20\]
-do_pointers::1::bool_2 \(\) -> TOP @ \[21\]
-do_pointers::1::x \(\) -> TOP @ \[22\]
-do_pointers::1::x \(\) -> 10 @ \[23\]
-do_pointers::1::x_p \(\) -> TOP @ \[24\]
-do_pointers::1::y \(\) -> TOP @ \[25\]
-do_pointers::1::y \(\) -> 20 @ \[26\]
-do_pointers::1::y_p \(\) -> TOP @ \[27\]
-do_pointers::1::x_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[28\]
-do_pointers::1::x \(\) -> 30 @ \[29\]
-do_pointers::1::x \(\) -> 40 @ \[30\]
-do_pointers::1::x \(\) -> TOP @ \[31\]
-do_pointers::1::x \(\) -> 50 @ \[32\]
-do_pointers::1::y_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[33\]
-do_pointers::1::x \(\) -> 60 @ \[34\]
-do_pointers::1::j \(\) -> TOP @ \[35\]
-do_pointers::1::j \(\) -> 60 @ \[36\]
+__CPROVER_dead_object \(\) -> TOP @ \[4\]
+__CPROVER_deallocated \(\) -> TOP @ \[5\]
+__CPROVER_memory_leak \(\) -> TOP @ \[7\]
+__CPROVER_next_thread_key \(\) -> 0ul @ \[9\]
+__CPROVER_rounding_mode \(\) -> 0 @ \[10\]
+__CPROVER_thread_id \(\) -> 0ul @ \[11\]
+__CPROVER_threads_exited \(\) -> TOP @ \[14\]
+do_pointers::1::bool_ \(\) -> TOP @ \[16\]
+do_pointers::1::bool_1 \(\) -> TOP @ \[17\]
+do_pointers::1::bool_2 \(\) -> TOP @ \[18\]
+do_pointers::1::x \(\) -> TOP @ \[19\]
+do_pointers::1::x \(\) -> 10 @ \[20\]
+do_pointers::1::x_p \(\) -> TOP @ \[21\]
+do_pointers::1::y \(\) -> TOP @ \[22\]
+do_pointers::1::y \(\) -> 20 @ \[23\]
+do_pointers::1::y_p \(\) -> TOP @ \[24\]
+do_pointers::1::x_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[25\]
+do_pointers::1::x \(\) -> 30 @ \[26\]
+do_pointers::1::x \(\) -> 40 @ \[27\]
+do_pointers::1::x \(\) -> TOP @ \[28\]
+do_pointers::1::x \(\) -> 50 @ \[29\]
+do_pointers::1::y_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[30\]
+do_pointers::1::x \(\) -> 60 @ \[31\]
+do_pointers::1::j \(\) -> TOP @ \[32\]
+do_pointers::1::j \(\) -> 60 @ \[33\]
diff --git a/regression/goto-analyzer/sensitivity-last-written-locations-structs/test.desc b/regression/goto-analyzer/sensitivity-last-written-locations-structs/test.desc
diff --git a/regression/goto-analyzer/sensitivity-last-written-locations-variables/test.desc b/regression/goto-analyzer/sensitivity-last-written-locations-variables/test.desc
diff --git a/regression/goto-analyzer/sensitivity-test-data-dependency-context/test.desc b/regression/goto-analyzer/sensitivity-test-data-dependency-context/test.desc
diff --git a/regression/goto-analyzer/variable-sensitivity-dependence-graph-toyota/test.desc b/regression/goto-analyzer/variable-sensitivity-dependence-graph-toyota/test.desc
diff --git a/regression/goto-analyzer/variable-sensitivity-dependence-graph/test.desc b/regression/goto-analyzer/variable-sensitivity-dependence-graph/test.desc
diff --git a/regression/goto-analyzer/variable-sensitivity-dependence-graph17/test.desc b/regression/goto-analyzer/variable-sensitivity-dependence-graph17/test.desc
diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp
diff --git a/src/ansi-c/library/cprover.h b/src/ansi-c/library/cprover.h
diff --git a/src/ansi-c/library/stdlib.c b/src/ansi-c/library/stdlib.c
diff --git a/src/cpp/cpp_internal_additions.cpp b/src/cpp/cpp_internal_additions.cpp
diff --git a/src/cpp/library/cprover.h b/src/cpp/library/cprover.h
diff --git a/src/cpp/library/new.c b/src/cpp/library/new.c

Original file line number	Diff line number	Diff line change
`@@ -4,9 +4,14 @@`
`4`	`4`	`void *alloca(size_t alloca_size);`
`5`	`5`	`#endif`
`6`	`6`
	`7`	`+// intentionally type conflicting: the built-in library uses const void*; this`
	`8`	`+// is to check that object type updates are performed`
	`9`	`+extern const char *__CPROVER_alloca_object;`
	`10`	`+`
`7`	`11`	`int *foo()`
`8`	`12`	`{`
`9`	`13`	`int *foo_ptr = alloca(sizeof(int));`
	`14`	`+ __CPROVER_assert(foo_ptr == __CPROVER_alloca_object, "may fail");`
`10`	`15`	`return foo_ptr;`
`11`	`16`	`}`
`12`	`17`