Remove __CPROVER_malloc_size

doc/architectural/memory-bounds-checking.md

@@ -33,28 +33,27 @@ inline void *malloc(__CPROVER_size_t malloc_size)
 
   __CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool();
   __CPROVER_malloc_object = record_malloc ? malloc_res : __CPROVER_malloc_object;
-  __CPROVER_malloc_size = record_malloc ? malloc_size : __CPROVER_malloc_size;
 
   return malloc_res;
 }
 ```
 
-Both internal variables `__CPROVER_malloc_object` and `__CPROVER_malloc_size`
-are initialized to 0 in the `__CPROVER_initialize()` function of a goto program.
-The nondeterministic switch controls whether the address and size of the memory
-block allocated in this particular invocation of `malloc()` are recorded.
+The internal variable `__CPROVER_malloc_object`
+is initialized to 0 in the `__CPROVER_initialize()` function of a goto program.
+The nondeterministic switch controls whether the address of the memory
+block allocated in this particular invocation of `malloc()` is recorded.
 
 When the option `--pointer-check` is used, cbmc generates the following
 verification condition for each pointer dereference expression (e.g.,
 `*pointer`):
 
 ```C
-__CPROVER_POINTER_OBJECT(pointer) == __CPROVER_POINTER_OBJECT(__CPROVER_malloc_object) ==>
-__CPROVER_POINTER_OFFSET(pointer) >= 0 && __CPROVER_POINTER_OFFSET(pointer) < __CPROVER_malloc_size
+__CPROVER_POINTER_OFFSET(pointer) >= 0 &&
+__CPROVER_POINTER_OFFSET(pointer) < __CPROVER_OBJECT_SIZE(pointer)
 ```
 
-The primitives `__CPROVER_POINTER_OBJECT()` and `__CPROVER_POINTER_OFFSET()` extract
-the object id, and pointer offset, respectively. Similar conditions are
+The primitives `__CPROVER_POINTER_OFFSET()` and `__CPROVER_OBJECT_SIZE()` extract
+the pointer offset and size of the object pointed to, respectively. Similar conditions are
 generated for `assert(__CPROVER_r_ok(pointer, size))` and
 `assert(__CPROVER_w_ok(pointer, size))`.
 
@@ -77,9 +76,5 @@ Here the verification condition generated for the pointer dereference should
 fail. In the approach outlined above it indeed can, as one can choose true for
 `__VERIFIER_nondet___CPROVER_bool()` in the first call
 to `malloc()`, and false for `__VERIFIER_nondet___CPROVER_bool()` in the second
-call to `malloc()`. Thus, the object address and size of the first call to
-`malloc()` are recorded in `__CPROVER_malloc_object` and `__CPROVER_malloc_size`
-respectively. Thus, the premise of the implication in the verification condition
-above is true, while the conclusion is false, hence the overall condition is
-false.
-
+call to `malloc()`. Thus, the object address of the first call to
+`malloc()` is recorded in `__CPROVER_malloc_object`.

regression/cbmc-with-incr/Pointer_byte_extract8/main.c

@@ -12,14 +12,11 @@ typedef struct
   Union List[1];
 } __attribute__((packed)) Struct3;
 
-extern size_t __CPROVER_malloc_size;
-
 int main()
 {
   Struct3 *p = malloc (sizeof (int) + 2 * sizeof(Union));
   p->Count = 3;
   int po=0;
-  size_t m=__CPROVER_malloc_size;
 
   // this should be fine
   p->List[0].a = 555;

regression/contracts/function_check_mem_01/main.c

@@ -7,21 +7,16 @@
 
 #include <stddef.h>
 
-#define __CPROVER_VALID_MEM(ptr, size) \
-  __CPROVER_POINTER_OBJECT((ptr)) != __CPROVER_POINTER_OBJECT(NULL) && \
-  !__CPROVER_invalid_pointer((ptr)) && \
-  __CPROVER_POINTER_OBJECT((ptr)) != \
-  __CPROVER_POINTER_OBJECT(__CPROVER_deallocated) && \
-  __CPROVER_POINTER_OBJECT((ptr)) != \
-  __CPROVER_POINTER_OBJECT(__CPROVER_dead_object) && \
-  (__builtin_object_size((ptr), 1) >= (size) && \
-  __CPROVER_POINTER_OFFSET((ptr)) >= 0l || \
-   __CPROVER_DYNAMIC_OBJECT((ptr))) && \
-  (__CPROVER_POINTER_OFFSET((ptr)) >= 0 && \
-   __CPROVER_malloc_size >= (size) + __CPROVER_POINTER_OFFSET((ptr)) || \
-   __CPROVER_POINTER_OBJECT((ptr)) != \
-   __CPROVER_POINTER_OBJECT(__CPROVER_malloc_object))
-
+#define __CPROVER_VALID_MEM(ptr, size)                                         \
+  __CPROVER_POINTER_OBJECT((ptr)) != __CPROVER_POINTER_OBJECT(NULL) &&         \
+    !__CPROVER_invalid_pointer((ptr)) &&                                       \
+    __CPROVER_POINTER_OBJECT((ptr)) !=                                         \
+      __CPROVER_POINTER_OBJECT(__CPROVER_deallocated) &&                       \
+    __CPROVER_POINTER_OBJECT((ptr)) !=                                         \
+      __CPROVER_POINTER_OBJECT(__CPROVER_dead_object) &&                       \
+    (__builtin_object_size((ptr), 1) >= (size) &&                              \
+     __CPROVER_POINTER_OFFSET((ptr)) >= 0l)
+
 typedef struct bar
 {
   int x;

regression/goto-analyzer/constant_propagation_01/test-vsd.desc

@@ -4,6 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 17, function calls: 2$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 16, function calls: 2$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_01/test.desc

@@ -4,6 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 17, function calls: 2$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 16, function calls: 2$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_02/test-vsd.desc

@@ -4,6 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 16, function calls: 2$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 15, function calls: 2$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_02/test.desc

@@ -4,6 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 16, function calls: 2$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 15, function calls: 2$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_03/test-vsd.desc

@@ -4,6 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 16, function calls: 2$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 15, function calls: 2$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_03/test.desc

@@ -4,6 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 16, function calls: 2$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 15, function calls: 2$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_04/test-vsd.desc

@@ -4,6 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 16, function calls: 2$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 15, function calls: 2$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_04/test.desc

@@ -4,6 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 16, function calls: 2$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 15, function calls: 2$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_07/test-vsd.desc

@@ -4,6 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^Simplified:  assert: 1, assume: 0, goto: 3, assigns: 9, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 18, function calls: 2$
+^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 17, function calls: 2$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_07/test.desc

@@ -4,6 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^Simplified:  assert: 1, assume: 0, goto: 3, assigns: 9, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 18, function calls: 2$
+^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 17, function calls: 2$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_08/test-vsd.desc

@@ -4,6 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^Simplified:  assert: 1, assume: 0, goto: 2, assigns: 8, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 3, assigns: 17, function calls: 2$
+^Unmodified:  assert: 0, assume: 0, goto: 3, assigns: 16, function calls: 2$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_11/test-vsd.desc

@@ -4,6 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 14, function calls: 2$
+^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 13, function calls: 2$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_11/test.desc

@@ -4,6 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 14, function calls: 2$
+^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 13, function calls: 2$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_12/test-vsd.desc

@@ -4,6 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 15, function calls: 2$
+^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 14, function calls: 2$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_12/test.desc

@@ -4,6 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 15, function calls: 2$
+^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 14, function calls: 2$
 --
 ^warning: ignoring

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 @ \[28\]
+globalX .* 0 @ \[27\]
 globalX .* 1 @ \[0\]
 globalX .* 2 @ \[3\]
-globalX .* TOP @ \[31\]
+globalX .* TOP @ \[30\]
 --

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 @ \[28\]
+globalX .* 0 @ \[27\]
 globalX .* 1 @ \[0\]
 globalX .* 2 @ \[3\]
-globalX .* TOP @ \[31\]
+globalX .* TOP @ \[30\]
 --

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 @ \[28\]
+globalX .* 0 @ \[27\]
 globalX .* 1 @ \[0\]
 globalX .* TOP @ \[0, 3\]
 --

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 @ \[28\]
+globalX .* 0 @ \[27\]
 globalX .* 1 @ \[0\]
 globalX .* 2 @ \[3\]
 --

regression/goto-analyzer/sensitivity-last-written-locations-arrays/test.desc

@@ -10,29 +10,28 @@ __CPROVER_dead_object \(\) -> TOP @ \[5\]
 __CPROVER_deallocated \(\) -> TOP @ \[6\]
 __CPROVER_malloc_is_new_array \(\) -> FALSE @ \[9\]
 __CPROVER_malloc_object \(\) -> TOP @ \[10\]
-__CPROVER_malloc_size \(\) -> 0ull? @ \[11\]
-__CPROVER_memory_leak \(\) -> TOP @ \[13\]
-__CPROVER_next_thread_key \(\) -> 0ul @ \[15\]
-__CPROVER_pipe_count \(\) -> 0u @ \[16\]
-__CPROVER_rounding_mode \(\) -> 0 @ \[17\]
-__CPROVER_thread_id \(\) -> 0ul @ \[18\]
-__CPROVER_threads_exited \(\) -> TOP @ \[21\]
-do_arrays::1::bool_ \(\) -> TOP @ \[23\]
-do_arrays::1::bool_1 \(\) -> TOP @ \[24\]
-do_arrays::1::bool_2 \(\) -> TOP @ \[25\]
-do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[27\]\n\} @ \[27\]
-do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[27\]\n\[1\] = 20 @ \[28\]\n\} @ \[28\]
-do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[29\]\n\[1\] = 20 @ \[28\]\n\} @ \[29\]
-do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[29\]\n\[1\] = 40 @ \[30\]\n\} @ \[30\]
-do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[29\]\n\[1\] = 30 @ \[31\]\n\} @ \[31\]
-do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[32\]\n\[1\] = 30 @ \[31\]\n\} @ \[32\]
-do_arrays::1::x \(\) -> \{\[0\] = 5 @ \[33\]\n\[1\] = 30 @ \[31\]\n\} @ \[33\]
-do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[34\]\n\[1\] = 30 @ \[31\]\n\} @ \[34\]
-do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[34\]\n\[1\] = 10 @ \[35\]\n\} @ \[35\]
-do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[37\]\n\[1\] = 10 @ \[35\]\n\} @ \[37\]
-do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[37\, 39\]\n\[1\] = 10 @ \[35\]\n\} @ \[37\, 39\]
-do_arrays::1::x \(\) -> \{\[0\] = 0 @ \[41]\n\[1\] = 10 @ \[35\]\n\} @ \[41\]
-do_arrays::1::x \(\) -> \{\[0\] = 3 @ \[43]\n\[1\] = 10 @ \[35\]\n\} @ \[43\]
-do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[43\, 45]\n\[1\] = 10 @ \[35\]\n\} @ \[43\, 45\]
-do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[43\, 45\, 48]\n\[1\] = 10 @ \[50\]\n\} @ \[50\]
-do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[51]\n\[1\] = 10 @ \[50\]\n\} @ \[51\]
+__CPROVER_memory_leak \(\) -> TOP @ \[12\]
+__CPROVER_next_thread_key \(\) -> 0ul @ \[14\]
+__CPROVER_pipe_count \(\) -> 0u @ \[15\]
+__CPROVER_rounding_mode \(\) -> 0 @ \[16\]
+__CPROVER_thread_id \(\) -> 0ul @ \[17\]
+__CPROVER_threads_exited \(\) -> TOP @ \[20\]
+do_arrays::1::bool_ \(\) -> TOP @ \[22\]
+do_arrays::1::bool_1 \(\) -> TOP @ \[23\]
+do_arrays::1::bool_2 \(\) -> TOP @ \[24\]
+do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[26\]\n\} @ \[26\]
+do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[26\]\n\[1\] = 20 @ \[27\]\n\} @ \[27\]
+do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[28\]\n\[1\] = 20 @ \[27\]\n\} @ \[28\]
+do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[28\]\n\[1\] = 40 @ \[29\]\n\} @ \[29\]
+do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[28\]\n\[1\] = 30 @ \[30\]\n\} @ \[30\]
+do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[31\]\n\[1\] = 30 @ \[30\]\n\} @ \[31\]
+do_arrays::1::x \(\) -> \{\[0\] = 5 @ \[32\]\n\[1\] = 30 @ \[30\]\n\} @ \[32\]
+do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[33\]\n\[1\] = 30 @ \[30\]\n\} @ \[33\]
+do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[33\]\n\[1\] = 10 @ \[34\]\n\} @ \[34\]
+do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[36\]\n\[1\] = 10 @ \[34\]\n\} @ \[36\]
+do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[36\, 38\]\n\[1\] = 10 @ \[34\]\n\} @ \[36\, 38\]
+do_arrays::1::x \(\) -> \{\[0\] = 0 @ \[40]\n\[1\] = 10 @ \[34\]\n\} @ \[40\]
+do_arrays::1::x \(\) -> \{\[0\] = 3 @ \[42]\n\[1\] = 10 @ \[34\]\n\} @ \[42\]
+do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[42\, 44]\n\[1\] = 10 @ \[34\]\n\} @ \[42\, 44\]
+do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[42\, 44\, 47]\n\[1\] = 10 @ \[49\]\n\} @ \[49\]
+do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[50]\n\[1\] = 10 @ \[49\]\n\} @ \[50\]

regression/goto-analyzer/sensitivity-last-written-locations-pointers/test.desc

@@ -10,28 +10,27 @@ __CPROVER_dead_object \(\) -> TOP @ \[5\]
 __CPROVER_deallocated \(\) -> TOP @ \[6\]
 __CPROVER_malloc_is_new_array \(\) -> FALSE @ \[9\]
 __CPROVER_malloc_object \(\) -> TOP @ \[10\]
-__CPROVER_malloc_size \(\) -> 0ull? @ \[11\]
-__CPROVER_memory_leak \(\) -> TOP @ \[13\]
-__CPROVER_next_thread_id \(\) -> 0ul @ \[14\]
-__CPROVER_pipe_count \(\) -> 0u @ \[16\]
-__CPROVER_rounding_mode \(\) -> 0 @ \[17\]
-__CPROVER_thread_id \(\) -> 0ul @ \[18\]
-__CPROVER_threads_exited \(\) -> TOP @ \[21\]
-do_pointers::1::bool_ \(\) -> TOP @ \[23\]
-do_pointers::1::bool_1 \(\) -> TOP @ \[24\]
-do_pointers::1::bool_2 \(\) -> TOP @ \[25\]
-do_pointers::1::x \(\) -> TOP @ \[26\]
-do_pointers::1::x \(\) -> 10 @ \[27\]
-do_pointers::1::x_p \(\) -> TOP @ \[28\]
-do_pointers::1::y \(\) -> TOP @ \[29\]
-do_pointers::1::y \(\) -> 20 @ \[30\]
-do_pointers::1::y_p \(\) -> TOP @ \[31\]
-do_pointers::1::x_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[32\]
-do_pointers::1::x \(\) -> 30 @ \[33\]
-do_pointers::1::x \(\) -> 40 @ \[34\]
-do_pointers::1::x \(\) -> TOP @ \[35\]
-do_pointers::1::x \(\) -> 50 @ \[36\]
-do_pointers::1::y_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[37\]
-do_pointers::1::x \(\) -> 60 @ \[38\]
-do_pointers::1::j \(\) -> TOP @ \[39\]
-do_pointers::1::j \(\) -> 60 @ \[40\]
+__CPROVER_memory_leak \(\) -> TOP @ \[12\]
+__CPROVER_next_thread_key \(\) -> 0ul @ \[14\]
+__CPROVER_pipe_count \(\) -> 0u @ \[15\]
+__CPROVER_rounding_mode \(\) -> 0 @ \[16\]
+__CPROVER_thread_id \(\) -> 0ul @ \[17\]
+__CPROVER_threads_exited \(\) -> TOP @ \[20\]
+do_pointers::1::bool_ \(\) -> TOP @ \[22\]
+do_pointers::1::bool_1 \(\) -> TOP @ \[23\]
+do_pointers::1::bool_2 \(\) -> TOP @ \[24\]
+do_pointers::1::x \(\) -> TOP @ \[25\]
+do_pointers::1::x \(\) -> 10 @ \[26\]
+do_pointers::1::x_p \(\) -> TOP @ \[27\]
+do_pointers::1::y \(\) -> TOP @ \[28\]
+do_pointers::1::y \(\) -> 20 @ \[29\]
+do_pointers::1::y_p \(\) -> TOP @ \[30\]
+do_pointers::1::x_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[31\]
+do_pointers::1::x \(\) -> 30 @ \[32\]
+do_pointers::1::x \(\) -> 40 @ \[33\]
+do_pointers::1::x \(\) -> TOP @ \[34\]
+do_pointers::1::x \(\) -> 50 @ \[35\]
+do_pointers::1::y_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[36\]
+do_pointers::1::x \(\) -> 60 @ \[37\]
+do_pointers::1::j \(\) -> TOP @ \[38\]
+do_pointers::1::j \(\) -> 60 @ \[39\]