Replace __CPROVER_malloc_is_new_array by an uninterpreted function

doc/architectural/memory-bounds-checking.md

@@ -30,19 +30,10 @@ inline void *malloc(__CPROVER_size_t malloc_size)
 {
   void *malloc_res;
   malloc_res = __CPROVER_allocate(malloc_size, 0);
-
-  __CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool();
-  __CPROVER_malloc_object = record_malloc ? malloc_res : __CPROVER_malloc_object;
-
   return malloc_res;
 }
 ```
 
-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`):
@@ -73,8 +64,7 @@ int main()
 ```
 
 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 of the first call to
-`malloc()` is recorded in `__CPROVER_malloc_object`.
+fail: for `p1` in `*p1`, `__CPROVER_POINTER_OFFSET` will evaluate to 1 (owing to
+the increment `p1++`, and `__CPROVER_OBJECT_SIZE` will also evaluate to 1.
+Consequently, the less-than comparison in the verification condition evaluates
+to false.

jbmc/src/java_bytecode/java_bytecode_internal_additions.cpp

@@ -36,20 +36,6 @@ void java_internal_additions(symbol_table_baset &dest)
     dest.add(symbol);
   }
 
-  // add __CPROVER_malloc_object
-
-  {
-    symbolt symbol;
-    symbol.base_name = CPROVER_PREFIX "malloc_object";
-    symbol.name=CPROVER_PREFIX "malloc_object";
-    symbol.type = pointer_type(java_void_type());
-    symbol.mode=ID_C;
-    symbol.is_lvalue=true;
-    symbol.is_state_var=true;
-    symbol.is_thread_local=true;
-    dest.add(symbol);
-  }
-
   {
     auxiliary_symbolt symbol;
     symbol.base_name = INFLIGHT_EXCEPTION_VARIABLE_BASENAME;

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: 7, function calls: 0$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$
 ^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 16, function calls: 2$
 --
 ^warning: ignoring

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: 7, function calls: 0$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$
 ^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 16, function calls: 2$
 --
 ^warning: ignoring

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: 8, function calls: 0$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
 ^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 15, function calls: 2$
 --
 ^warning: ignoring

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: 8, function calls: 0$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
 ^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 15, function calls: 2$
 --
 ^warning: ignoring

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: 8, function calls: 0$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
 ^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 15, function calls: 2$
 --
 ^warning: ignoring

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: 8, function calls: 0$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
 ^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 15, function calls: 2$
 --
 ^warning: ignoring

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: 8, function calls: 0$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
 ^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 15, function calls: 2$
 --
 ^warning: ignoring

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: 8, function calls: 0$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
 ^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 15, function calls: 2$
 --
 ^warning: ignoring

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: 9, function calls: 0$
+^Simplified:  assert: 1, assume: 0, goto: 3, assigns: 8, function calls: 0$
 ^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 17, function calls: 2$
 --
 ^warning: ignoring

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: 9, function calls: 0$
+^Simplified:  assert: 1, assume: 0, goto: 3, assigns: 8, function calls: 0$
 ^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 17, function calls: 2$
 --
 ^warning: ignoring

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: 8, function calls: 0$
+^Simplified:  assert: 1, assume: 0, goto: 2, assigns: 7, function calls: 0$
 ^Unmodified:  assert: 0, assume: 0, goto: 3, assigns: 16, function calls: 2$
 --
 ^warning: ignoring

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: 8, function calls: 0$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
 ^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 13, function calls: 2$
 --
 ^warning: ignoring

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: 8, function calls: 0$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
 ^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 13, function calls: 2$
 --
 ^warning: ignoring

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: 7, function calls: 0$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$
 ^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 14, function calls: 2$
 --
 ^warning: ignoring

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: 7, function calls: 0$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$
 ^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 14, function calls: 2$
 --
 ^warning: ignoring

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

@@ -8,30 +8,29 @@ activate-multi-line-match
 main#return_value \(\) -> TOP @ \[1\]
 __CPROVER_dead_object \(\) -> TOP @ \[5\]
 __CPROVER_deallocated \(\) -> TOP @ \[6\]
-__CPROVER_malloc_is_new_array \(\) -> FALSE @ \[9\]
-__CPROVER_malloc_object \(\) -> TOP @ \[10\]
-__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\]
+__CPROVER_memory_leak \(\) -> TOP @ \[10\]
+__CPROVER_new_object \(\) -> TOP @ \[11\]
+__CPROVER_next_thread_key \(\) -> 0ul @ \[13\]
+__CPROVER_pipe_count \(\) -> 0u @ \[14\]
+__CPROVER_rounding_mode \(\) -> 0 @ \[15\]
+__CPROVER_thread_id \(\) -> 0ul @ \[16\]
+__CPROVER_threads_exited \(\) -> TOP @ \[19\]
+do_arrays::1::bool_ \(\) -> TOP @ \[21\]
+do_arrays::1::bool_1 \(\) -> TOP @ \[22\]
+do_arrays::1::bool_2 \(\) -> TOP @ \[23\]
+do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[25\]\n\} @ \[25\]
+do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[25\]\n\[1\] = 20 @ \[26\]\n\} @ \[26\]
+do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[27\]\n\[1\] = 20 @ \[26\]\n\} @ \[27\]
+do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[27\]\n\[1\] = 40 @ \[28\]\n\} @ \[28\]
+do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[27\]\n\[1\] = 30 @ \[29\]\n\} @ \[29\]
+do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[30\]\n\[1\] = 30 @ \[29\]\n\} @ \[30\]
+do_arrays::1::x \(\) -> \{\[0\] = 5 @ \[31\]\n\[1\] = 30 @ \[29\]\n\} @ \[31\]
+do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[32\]\n\[1\] = 30 @ \[29\]\n\} @ \[32\]
+do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[32\]\n\[1\] = 10 @ \[33\]\n\} @ \[33\]
+do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[35\]\n\[1\] = 10 @ \[33\]\n\} @ \[35\]
+do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[35\, 37\]\n\[1\] = 10 @ \[33\]\n\} @ \[35\, 37\]
+do_arrays::1::x \(\) -> \{\[0\] = 0 @ \[39]\n\[1\] = 10 @ \[33\]\n\} @ \[39\]
+do_arrays::1::x \(\) -> \{\[0\] = 3 @ \[41]\n\[1\] = 10 @ \[33\]\n\} @ \[41\]
+do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[41\, 43]\n\[1\] = 10 @ \[33\]\n\} @ \[41\, 43\]
+do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[41\, 43\, 46]\n\[1\] = 10 @ \[48\]\n\} @ \[48\]
+do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[49]\n\[1\] = 10 @ \[48\]\n\} @ \[49\]

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

@@ -8,29 +8,28 @@ activate-multi-line-match
 main#return_value \(\) -> TOP @ \[1\]
 __CPROVER_dead_object \(\) -> TOP @ \[5\]
 __CPROVER_deallocated \(\) -> TOP @ \[6\]
-__CPROVER_malloc_is_new_array \(\) -> FALSE @ \[9\]
-__CPROVER_malloc_object \(\) -> TOP @ \[10\]
-__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\]
+__CPROVER_new_object \(\) -> TOP @ \[11\]
+__CPROVER_memory_leak \(\) -> TOP @ \[10\]
+__CPROVER_next_thread_id \(\) -> 0ul @ \[12\]
+__CPROVER_pipe_count \(\) -> 0u @ \[14\]
+__CPROVER_rounding_mode \(\) -> 0 @ \[15\]
+__CPROVER_thread_id \(\) -> 0ul @ \[16\]
+__CPROVER_threads_exited \(\) -> TOP @ \[19\]
+do_pointers::1::bool_ \(\) -> TOP @ \[21\]
+do_pointers::1::bool_1 \(\) -> TOP @ \[22\]
+do_pointers::1::bool_2 \(\) -> TOP @ \[23\]
+do_pointers::1::x \(\) -> TOP @ \[24\]
+do_pointers::1::x \(\) -> 10 @ \[25\]
+do_pointers::1::x_p \(\) -> TOP @ \[26\]
+do_pointers::1::y \(\) -> TOP @ \[27\]
+do_pointers::1::y \(\) -> 20 @ \[28\]
+do_pointers::1::y_p \(\) -> TOP @ \[29\]
+do_pointers::1::x_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[30\]
+do_pointers::1::x \(\) -> 30 @ \[31\]
+do_pointers::1::x \(\) -> 40 @ \[32\]
+do_pointers::1::x \(\) -> TOP @ \[33\]
+do_pointers::1::x \(\) -> 50 @ \[34\]
+do_pointers::1::y_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[35\]
+do_pointers::1::x \(\) -> 60 @ \[36\]
+do_pointers::1::j \(\) -> TOP @ \[37\]
+do_pointers::1::j \(\) -> 60 @ \[38\]

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

@@ -8,35 +8,34 @@ activate-multi-line-match
 main#return_value \(\) -> TOP @ \[1\]
 __CPROVER_dead_object \(\) -> TOP @ \[5\]
 __CPROVER_deallocated \(\) -> TOP @ \[6\]
-__CPROVER_malloc_is_new_array \(\) -> FALSE @ \[9\]
-__CPROVER_malloc_object \(\) -> TOP @ \[10\]
-__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_structs::1::bool_ \(\) -> TOP @ \[22\]
-do_structs::1::bool_1 \(\) -> TOP @ \[23\]
-do_structs::1::bool_2 \(\) -> TOP @ \[24\]
-do_structs::1::st \(\) -> \{\} @ \[25\]
-do_structs::1::st \(\) -> \{.x=10 @ \[26\]\} @ \[26\]
-do_structs::1::st \(\) -> \{.x=10 @ \[26\]\, .y=20 @ \[27\]\} @ \[27\]
-do_structs::1::st \(\) -> \{.x=30 @ \[28\]\, .y=20 @ \[27\]\} @ \[28\]
-do_structs::1::st \(\) -> \{.x=30 @ \[28\]\, .y=40 @ \[29\]\} @ \[29\]
-do_structs::1::st \(\) -> \{.x=30 @ \[28\]\, .y=30 @ \[30\]\} @ \[30\]
-do_structs::1::st \(\) -> \{.x=30 @ \[31\]\, .y=30 @ \[30\]\} @ \[31\]
-do_structs::1::st \(\) -> \{.x=5 @ \[32\]\, .y=30 @ \[30\]\} @ \[32\]
-do_structs::1::st \(\) -> \{.x=15 @ \[33\]\, .y=30 @ \[30\]\} @ \[33\]
-do_structs::1::st \(\) -> \{.x=15 @ \[33\]\, .y=10 @ \[34\]\} @ \[34\]
-do_structs::1::st \(\) -> \{.x=20 @ \[36\]\, .y=10 @ \[34\]\} @ \[36\]
-do_structs::1::st \(\) -> \{.x=20 @ \[36\, 38\]\, .y=10 @ \[34\]\} @ \[36\, 38\]
-do_structs::1::st \(\) -> \{.x=0 @ \[40\]\, .y=10 @ \[34\]\} @ \[40\]
-do_structs::1::st \(\) -> \{.x=3 @ \[42\]\, .y=10 @ \[34\]\} @ \[42\]
-do_structs::1::st \(\) -> \{.x=TOP @ \[42\, 44\]\, .y=10 @ \[34\]\} @ \[42\, 44\]
-do_structs::1::st \(\) -> \{.x=TOP @ \[42\, 44\, 47\]\, .y=10 @ \[34\]\} @ \[42\, 44\, 47\]
-do_structs::1::st \(\) -> \{.x=TOP @ \[42\, 44\, 47\]\, .y=10 @ \[49\]\} @ \[49\]
-do_structs::1::st \(\) -> \{.x=20 @ \[50\]\, .y=10 @ \[49\]\} @ \[50\]
-do_structs::1::new_age \(\) -> \{\} @ \[51\]
-do_structs::1::new_age \(\) -> \{.x=20 @ \[52\]\, .y=10 @ \[52\]\} @ \[52\]
+__CPROVER_new_object \(\) -> TOP @ \[11\]
+__CPROVER_memory_leak \(\) -> TOP @ \[10\]
+__CPROVER_next_thread_id \(\) -> 0ul @ \[12\]
+__CPROVER_pipe_count \(\) -> 0u @ \[14\]
+__CPROVER_rounding_mode \(\) -> 0 @ \[15\]
+__CPROVER_thread_id \(\) -> 0ul @ \[16\]
+__CPROVER_threads_exited \(\) -> TOP @ \[19\]
+do_structs::1::bool_ \(\) -> TOP @ \[21\]
+do_structs::1::bool_1 \(\) -> TOP @ \[22\]
+do_structs::1::bool_2 \(\) -> TOP @ \[23\]
+do_structs::1::st \(\) -> \{\} @ \[24\]
+do_structs::1::st \(\) -> \{.x=10 @ \[25\]\} @ \[25\]
+do_structs::1::st \(\) -> \{.x=10 @ \[25\]\, .y=20 @ \[26\]\} @ \[26\]
+do_structs::1::st \(\) -> \{.x=30 @ \[27\]\, .y=20 @ \[26\]\} @ \[27\]
+do_structs::1::st \(\) -> \{.x=30 @ \[27\]\, .y=40 @ \[28\]\} @ \[28\]
+do_structs::1::st \(\) -> \{.x=30 @ \[27\]\, .y=30 @ \[29\]\} @ \[29\]
+do_structs::1::st \(\) -> \{.x=30 @ \[30\]\, .y=30 @ \[29\]\} @ \[30\]
+do_structs::1::st \(\) -> \{.x=5 @ \[31\]\, .y=30 @ \[29\]\} @ \[31\]
+do_structs::1::st \(\) -> \{.x=15 @ \[32\]\, .y=30 @ \[29\]\} @ \[32\]
+do_structs::1::st \(\) -> \{.x=15 @ \[32\]\, .y=10 @ \[33\]\} @ \[33\]
+do_structs::1::st \(\) -> \{.x=20 @ \[35\]\, .y=10 @ \[33\]\} @ \[35\]
+do_structs::1::st \(\) -> \{.x=20 @ \[35\, 37\]\, .y=10 @ \[33\]\} @ \[35\, 37\]
+do_structs::1::st \(\) -> \{.x=0 @ \[39\]\, .y=10 @ \[33\]\} @ \[39\]
+do_structs::1::st \(\) -> \{.x=3 @ \[41\]\, .y=10 @ \[33\]\} @ \[41\]
+do_structs::1::st \(\) -> \{.x=TOP @ \[41\, 43\]\, .y=10 @ \[33\]\} @ \[41\, 43\]
+do_structs::1::st \(\) -> \{.x=TOP @ \[41\, 43\, 46\]\, .y=10 @ \[33\]\} @ \[41\, 43\, 46\]
+do_structs::1::st \(\) -> \{.x=TOP @ \[41\, 43\, 46\]\, .y=10 @ \[48\]\} @ \[48\]
+do_structs::1::st \(\) -> \{.x=20 @ \[49\]\, .y=10 @ \[48\]\} @ \[49\]
+do_structs::1::new_age \(\) -> \{\} @ \[50\]
+do_structs::1::new_age \(\) -> \{.x=20 @ \[51\]\, .y=10 @ \[51\]\} @ \[51\]
 --