C library: move pipe() related definitions to library

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
pipe-related library functions.

Author: tautschnig

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: 14, 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: 14, 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: 13, 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: 13, 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: 13, 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: 13, 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: 13, 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: 13, 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: 15, 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: 15, 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: 14, 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: 11, 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: 11, 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: 12, 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: 12, 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 @ \[25\]
+globalX .* 0 @ \[24\]
 globalX .* 1 @ \[0\]
 globalX .* 2 @ \[3\]
-globalX .* TOP @ \[28\]
+globalX .* TOP @ \[27\]
 --

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

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

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

@@ -12,26 +12,25 @@ __CPROVER_malloc_is_new_array \(\) -> FALSE @ \[7\]
 __CPROVER_memory_leak \(\) -> TOP @ \[9\]
 __CPROVER_new_object \(\) -> TOP @ \[10\]
 __CPROVER_next_thread_key \(\) -> 0ul @ \[12\]
-__CPROVER_pipe_count \(\) -> 0u @ \[13\]
-__CPROVER_rounding_mode \(\) -> 0 @ \[14\]
-__CPROVER_thread_id \(\) -> 0ul @ \[15\]
-__CPROVER_threads_exited \(\) -> TOP @ \[18\]
-do_arrays::1::bool_ \(\) -> TOP @ \[20\]
-do_arrays::1::bool_1 \(\) -> TOP @ \[21\]
-do_arrays::1::bool_2 \(\) -> TOP @ \[22\]
-do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[24\]\n\} @ \[24\]
-do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[24\]\n\[1\] = 20 @ \[25\]\n\} @ \[25\]
-do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[26\]\n\[1\] = 20 @ \[25\]\n\} @ \[26\]
-do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[26\]\n\[1\] = 40 @ \[27\]\n\} @ \[27\]
-do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[26\]\n\[1\] = 30 @ \[28\]\n\} @ \[28\]
-do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[29\]\n\[1\] = 30 @ \[28\]\n\} @ \[29\]
-do_arrays::1::x \(\) -> \{\[0\] = 5 @ \[30\]\n\[1\] = 30 @ \[28\]\n\} @ \[30\]
-do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[31\]\n\[1\] = 30 @ \[28\]\n\} @ \[31\]
-do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[31\]\n\[1\] = 10 @ \[32\]\n\} @ \[32\]
-do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[34\]\n\[1\] = 10 @ \[32\]\n\} @ \[34\]
-do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[34\, 36\]\n\[1\] = 10 @ \[32\]\n\} @ \[34\, 36\]
-do_arrays::1::x \(\) -> \{\[0\] = 0 @ \[38]\n\[1\] = 10 @ \[32\]\n\} @ \[38\]
-do_arrays::1::x \(\) -> \{\[0\] = 3 @ \[40]\n\[1\] = 10 @ \[32\]\n\} @ \[40\]
-do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[40\, 42]\n\[1\] = 10 @ \[32\]\n\} @ \[40\, 42\]
-do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[40\, 42\, 45]\n\[1\] = 10 @ \[47\]\n\} @ \[47\]
-do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[48]\n\[1\] = 10 @ \[47\]\n\} @ \[48\]
+__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\]

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

@@ -12,25 +12,24 @@ __CPROVER_malloc_is_new_array \(\) -> FALSE @ \[7\]
 __CPROVER_memory_leak \(\) -> TOP @ \[9\]
 __CPROVER_new_object \(\) -> TOP @ \[10\]
 __CPROVER_next_thread_key \(\) -> 0ul @ \[12\]
-__CPROVER_pipe_count \(\) -> 0u @ \[13\]
-__CPROVER_rounding_mode \(\) -> 0 @ \[14\]
-__CPROVER_thread_id \(\) -> 0ul @ \[15\]
-__CPROVER_threads_exited \(\) -> TOP @ \[18\]
-do_pointers::1::bool_ \(\) -> TOP @ \[20\]
-do_pointers::1::bool_1 \(\) -> TOP @ \[21\]
-do_pointers::1::bool_2 \(\) -> TOP @ \[22\]
-do_pointers::1::x \(\) -> TOP @ \[23\]
-do_pointers::1::x \(\) -> 10 @ \[24\]
-do_pointers::1::x_p \(\) -> TOP @ \[25\]
-do_pointers::1::y \(\) -> TOP @ \[26\]
-do_pointers::1::y \(\) -> 20 @ \[27\]
-do_pointers::1::y_p \(\) -> TOP @ \[28\]
-do_pointers::1::x_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[29\]
-do_pointers::1::x \(\) -> 30 @ \[30\]
-do_pointers::1::x \(\) -> 40 @ \[31\]
-do_pointers::1::x \(\) -> TOP @ \[32\]
-do_pointers::1::x \(\) -> 50 @ \[33\]
-do_pointers::1::y_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[34\]
-do_pointers::1::x \(\) -> 60 @ \[35\]
-do_pointers::1::j \(\) -> TOP @ \[36\]
-do_pointers::1::j \(\) -> 60 @ \[37\]
+__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\]

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

@@ -12,31 +12,30 @@ __CPROVER_malloc_is_new_array \(\) -> FALSE @ \[7\]
 __CPROVER_memory_leak \(\) -> TOP @ \[9\]
 __CPROVER_new_object \(\) -> TOP @ \[10\]
 __CPROVER_next_thread_key \(\) -> 0ul @ \[12\]
-__CPROVER_pipe_count \(\) -> 0u @ \[13\]
-__CPROVER_rounding_mode \(\) -> 0 @ \[14\]
-__CPROVER_thread_id \(\) -> 0ul @ \[15\]
-__CPROVER_threads_exited \(\) -> TOP @ \[18\]
-do_structs::1::bool_ \(\) -> TOP @ \[20\]
-do_structs::1::bool_1 \(\) -> TOP @ \[21\]
-do_structs::1::bool_2 \(\) -> TOP @ \[22\]
-do_structs::1::st \(\) -> \{\} @ \[23\]
-do_structs::1::st \(\) -> \{.x=10 @ \[24\]\} @ \[24\]
-do_structs::1::st \(\) -> \{.x=10 @ \[24\]\, .y=20 @ \[25\]\} @ \[25\]
-do_structs::1::st \(\) -> \{.x=30 @ \[26\]\, .y=20 @ \[25\]\} @ \[26\]
-do_structs::1::st \(\) -> \{.x=30 @ \[26\]\, .y=40 @ \[27\]\} @ \[27\]
-do_structs::1::st \(\) -> \{.x=30 @ \[26\]\, .y=30 @ \[28\]\} @ \[28\]
-do_structs::1::st \(\) -> \{.x=30 @ \[29\]\, .y=30 @ \[28\]\} @ \[29\]
-do_structs::1::st \(\) -> \{.x=5 @ \[30\]\, .y=30 @ \[28\]\} @ \[30\]
-do_structs::1::st \(\) -> \{.x=15 @ \[31\]\, .y=30 @ \[28\]\} @ \[31\]
-do_structs::1::st \(\) -> \{.x=15 @ \[31\]\, .y=10 @ \[32\]\} @ \[32\]
-do_structs::1::st \(\) -> \{.x=20 @ \[34\]\, .y=10 @ \[32\]\} @ \[34\]
-do_structs::1::st \(\) -> \{.x=20 @ \[34\, 36\]\, .y=10 @ \[32\]\} @ \[34\, 36\]
-do_structs::1::st \(\) -> \{.x=0 @ \[38\]\, .y=10 @ \[32\]\} @ \[38\]
-do_structs::1::st \(\) -> \{.x=3 @ \[40\]\, .y=10 @ \[32\]\} @ \[40\]
-do_structs::1::st \(\) -> \{.x=TOP @ \[40\, 42\]\, .y=10 @ \[32\]\} @ \[40\, 42\]
-do_structs::1::st \(\) -> \{.x=TOP @ \[40\, 42\, 45\]\, .y=10 @ \[32\]\} @ \[40\, 42\, 45\]
-do_structs::1::st \(\) -> \{.x=TOP @ \[40\, 42\, 45\]\, .y=10 @ \[47\]\} @ \[47\]
-do_structs::1::st \(\) -> \{.x=20 @ \[48\]\, .y=10 @ \[47\]\} @ \[48\]
-do_structs::1::new_age \(\) -> \{\} @ \[49\]
-do_structs::1::new_age \(\) -> \{.x=20 @ \[50\]\, .y=10 @ \[50\]\} @ \[50\]
+__CPROVER_rounding_mode \(\) -> 0 @ \[13\]
+__CPROVER_thread_id \(\) -> 0ul @ \[14\]
+__CPROVER_threads_exited \(\) -> TOP @ \[17\]
+do_structs::1::bool_ \(\) -> TOP @ \[19\]
+do_structs::1::bool_1 \(\) -> TOP @ \[20\]
+do_structs::1::bool_2 \(\) -> TOP @ \[21\]
+do_structs::1::st \(\) -> \{\} @ \[22\]
+do_structs::1::st \(\) -> \{.x=10 @ \[23\]\} @ \[23\]
+do_structs::1::st \(\) -> \{.x=10 @ \[23\]\, .y=20 @ \[24\]\} @ \[24\]
+do_structs::1::st \(\) -> \{.x=30 @ \[25\]\, .y=20 @ \[24\]\} @ \[25\]
+do_structs::1::st \(\) -> \{.x=30 @ \[25\]\, .y=40 @ \[26\]\} @ \[26\]
+do_structs::1::st \(\) -> \{.x=30 @ \[25\]\, .y=30 @ \[27\]\} @ \[27\]
+do_structs::1::st \(\) -> \{.x=30 @ \[28\]\, .y=30 @ \[27\]\} @ \[28\]
+do_structs::1::st \(\) -> \{.x=5 @ \[29\]\, .y=30 @ \[27\]\} @ \[29\]
+do_structs::1::st \(\) -> \{.x=15 @ \[30\]\, .y=30 @ \[27\]\} @ \[30\]
+do_structs::1::st \(\) -> \{.x=15 @ \[30\]\, .y=10 @ \[31\]\} @ \[31\]
+do_structs::1::st \(\) -> \{.x=20 @ \[33\]\, .y=10 @ \[31\]\} @ \[33\]
+do_structs::1::st \(\) -> \{.x=20 @ \[33\, 35\]\, .y=10 @ \[31\]\} @ \[33\, 35\]
+do_structs::1::st \(\) -> \{.x=0 @ \[37\]\, .y=10 @ \[31\]\} @ \[37\]
+do_structs::1::st \(\) -> \{.x=3 @ \[39\]\, .y=10 @ \[31\]\} @ \[39\]
+do_structs::1::st \(\) -> \{.x=TOP @ \[39\, 41\]\, .y=10 @ \[31\]\} @ \[39\, 41\]
+do_structs::1::st \(\) -> \{.x=TOP @ \[39\, 41\, 44\]\, .y=10 @ \[31\]\} @ \[39\, 41\, 44\]
+do_structs::1::st \(\) -> \{.x=TOP @ \[39\, 41\, 44\]\, .y=10 @ \[46\]\} @ \[46\]
+do_structs::1::st \(\) -> \{.x=20 @ \[47\]\, .y=10 @ \[46\]\} @ \[47\]
+do_structs::1::new_age \(\) -> \{\} @ \[48\]
+do_structs::1::new_age \(\) -> \{.x=20 @ \[49\]\, .y=10 @ \[49\]\} @ \[49\]
 --

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

@@ -11,35 +11,34 @@ __CPROVER_malloc_is_new_array \(\) -> FALSE @ \[7\]
 __CPROVER_memory_leak \(\) -> TOP @ \[9\]
 __CPROVER_new_object \(\) -> TOP @ \[10\]
 __CPROVER_next_thread_key \(\) -> 0ul @ \[12\]
-__CPROVER_pipe_count \(\) -> 0u @ \[13\]
-__CPROVER_rounding_mode \(\) -> 0 @ \[14\]
-__CPROVER_thread_id \(\) -> 0ul @ \[15\]
-__CPROVER_threads_exited \(\) -> TOP @ \[18\]
-global_x \(\) -> 0 @ \[19\]
-do_variables::1::bool_ \(\) -> TOP @ \[21\]
-do_variables::1::bool_1 \(\) -> TOP @ \[22\]
-do_variables::1::bool_2 \(\) -> TOP @ \[23\]
-global_x \(\) -> 5 @ \[24\]
-do_variables::1::x \(\) -> TOP @ \[25\]
-do_variables::1::x \(\) -> 10 @ \[26\]
-do_variables::1::y \(\) -> TOP @ \[27\]
-do_variables::1::y \(\) -> 20 @ \[28\]
-do_variables::1::x \(\) -> 30 @ \[29\]
-do_variables::1::y \(\) -> 40 @ \[30\]
-do_variables::1::y \(\) -> 30 @ \[31\]
-do_variables::1::x \(\) -> 30 @ \[32\]
-do_variables::1::x \(\) -> 5 @ \[33\]
-do_variables::1::x \(\) -> 15 @ \[34\]
-do_variables::1::y \(\) -> 10 @ \[35\]
-do_variables::1::x \(\) -> 20 @ \[37\]
-do_variables::1::x \(\) -> 20 @ \[37\, 39\]
-do_variables::1::x \(\) -> 50 @ \[41\]
-do_variables::1::x \(\) -> 20 @ \[43\]
-do_variables::1::x \(\) -> TOP @ \[43\, 45\]
-do_variables::1::x \(\) -> 0 @ \[47\]
-do_variables::1::x \(\) -> 3 @ \[49\]
-do_variables::1::x \(\) -> TOP @ \[49\, 51\]
-do_variables::1::x \(\) -> TOP @ \[49\, 51\, 54\]
-do_variables::1::y \(\) -> 10 @ \[56\]
-do_variables::1::x \(\) -> 20 @ \[57\]
+__CPROVER_rounding_mode \(\) -> 0 @ \[13\]
+__CPROVER_thread_id \(\) -> 0ul @ \[14\]
+__CPROVER_threads_exited \(\) -> TOP @ \[17\]
+global_x \(\) -> 0 @ \[18\]
+do_variables::1::bool_ \(\) -> TOP @ \[20\]
+do_variables::1::bool_1 \(\) -> TOP @ \[21\]
+do_variables::1::bool_2 \(\) -> TOP @ \[22\]
+global_x \(\) -> 5 @ \[23\]
+do_variables::1::x \(\) -> TOP @ \[24\]
+do_variables::1::x \(\) -> 10 @ \[25\]
+do_variables::1::y \(\) -> TOP @ \[26\]
+do_variables::1::y \(\) -> 20 @ \[27\]
+do_variables::1::x \(\) -> 30 @ \[28\]
+do_variables::1::y \(\) -> 40 @ \[29\]
+do_variables::1::y \(\) -> 30 @ \[30\]
+do_variables::1::x \(\) -> 30 @ \[31\]
+do_variables::1::x \(\) -> 5 @ \[32\]
+do_variables::1::x \(\) -> 15 @ \[33\]
+do_variables::1::y \(\) -> 10 @ \[34\]
+do_variables::1::x \(\) -> 20 @ \[36\]
+do_variables::1::x \(\) -> 20 @ \[36\, 38\]
+do_variables::1::x \(\) -> 50 @ \[40\]
+do_variables::1::x \(\) -> 20 @ \[42\]
+do_variables::1::x \(\) -> TOP @ \[42\, 44\]
+do_variables::1::x \(\) -> 0 @ \[46\]
+do_variables::1::x \(\) -> 3 @ \[48\]
+do_variables::1::x \(\) -> TOP @ \[48\, 50\]
+do_variables::1::x \(\) -> TOP @ \[48\, 50\, 53\]
+do_variables::1::y \(\) -> 10 @ \[55\]
+do_variables::1::x \(\) -> 20 @ \[56\]
 --