Skip to content

Commit ade4173

Browse files
tautschnigtautschnig
committed
C/C++ library: move free/delete-only 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 memory (de-)allocation library functions.
1 parent 7490f96 commit ade4173

File tree

36 files changed

+216
-210
lines changed

36 files changed

+216
-210
lines changed

‎regression/cbmc-library/alloca-02/main.c

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,9 +4,14 @@
44
void *alloca(size_t alloca_size);
55
#endif
66

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+
711
int *foo()
812
{
913
int *foo_ptr = alloca(sizeof(int));
14+
__CPROVER_assert(foo_ptr == __CPROVER_alloca_object, "may fail");
1015
return foo_ptr;
1116
}
1217

‎regression/cbmc-library/alloca-02/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@ CORE
22
main.c
33
--pointer-check
44
dereference failure: dead object in \*from_foo: FAILURE$
5-
^\*\* 1 of 6 failed
5+
^\*\* 2 of 7 failed
66
^VERIFICATION FAILED$
77
^EXIT=10$
88
^SIGNAL=0$

‎regression/cbmc-library/free-01/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
main.c
33
--pointer-check --bounds-check --stop-on-fail
4-
free argument must be NULL or valid pointer
4+
free argument must be (NULL or valid pointer|dynamic object)
55
^EXIT=10$
66
^SIGNAL=0$
77
^VERIFICATION FAILED$

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--variable-sensitivity --simplify out.gb
44
^EXIT=0$
55
^SIGNAL=0$
6-
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 14, function calls: 2$
6+
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 5, function calls: 0$
7+
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 12, function calls: 2$
88
--
99
^warning: ignoring

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--constants --simplify out.gb
44
^EXIT=0$
55
^SIGNAL=0$
6-
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 14, function calls: 2$
6+
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 5, function calls: 0$
7+
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 12, function calls: 2$
88
--
99
^warning: ignoring

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--variable-sensitivity --simplify out.gb
44
^EXIT=0$
55
^SIGNAL=0$
6-
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 13, function calls: 2$
6+
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$
7+
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
88
--
99
^warning: ignoring

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--constants --simplify out.gb
44
^EXIT=0$
55
^SIGNAL=0$
6-
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 13, function calls: 2$
6+
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$
7+
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
88
--
99
^warning: ignoring

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--variable-sensitivity --simplify out.gb
44
^EXIT=0$
55
^SIGNAL=0$
6-
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 13, function calls: 2$
6+
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$
7+
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
88
--
99
^warning: ignoring

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--constants --simplify out.gb
44
^EXIT=0$
55
^SIGNAL=0$
6-
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 13, function calls: 2$
6+
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$
7+
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
88
--
99
^warning: ignoring

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--variable-sensitivity --simplify out.gb
44
^EXIT=0$
55
^SIGNAL=0$
6-
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 13, function calls: 2$
6+
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$
7+
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
88
--
99
^warning: ignoring

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--constants --simplify out.gb
44
^EXIT=0$
55
^SIGNAL=0$
6-
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 13, function calls: 2$
6+
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$
7+
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
88
--
99
^warning: ignoring

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--variable-sensitivity --simplify out.gb
44
^EXIT=0$
55
^SIGNAL=0$
6-
^Simplified: assert: 1, assume: 0, goto: 3, assigns: 8, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 15, function calls: 2$
6+
^Simplified: assert: 1, assume: 0, goto: 3, assigns: 7, function calls: 0$
7+
^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 13, function calls: 2$
88
--
99
^warning: ignoring

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--constants --simplify out.gb
44
^EXIT=0$
55
^SIGNAL=0$
6-
^Simplified: assert: 1, assume: 0, goto: 3, assigns: 8, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 15, function calls: 2$
6+
^Simplified: assert: 1, assume: 0, goto: 3, assigns: 7, function calls: 0$
7+
^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 13, function calls: 2$
88
--
99
^warning: ignoring

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--variable-sensitivity --vsd-arrays every-element --simplify out.gb
44
^EXIT=0$
55
^SIGNAL=0$
6-
^Simplified: assert: 1, assume: 0, goto: 2, assigns: 7, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 3, assigns: 14, function calls: 2$
6+
^Simplified: assert: 1, assume: 0, goto: 2, assigns: 6, function calls: 0$
7+
^Unmodified: assert: 0, assume: 0, goto: 3, assigns: 12, function calls: 2$
88
--
99
^warning: ignoring

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--variable-sensitivity --vsd-arrays every-element --simplify out.gb
44
^EXIT=0$
55
^SIGNAL=0$
6-
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 11, function calls: 2$
6+
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$
7+
^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 9, function calls: 2$
88
--
99
^warning: ignoring

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--constants --simplify out.gb
44
^EXIT=0$
55
^SIGNAL=0$
6-
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 11, function calls: 2$
6+
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$
7+
^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 9, function calls: 2$
88
--
99
^warning: ignoring

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--variable-sensitivity --simplify out.gb
44
^EXIT=0$
55
^SIGNAL=0$
6-
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 12, function calls: 2$
6+
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 5, function calls: 0$
7+
^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 10, function calls: 2$
88
--
99
^warning: ignoring

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--constants --simplify out.gb
44
^EXIT=0$
55
^SIGNAL=0$
6-
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 12, function calls: 2$
6+
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 5, function calls: 0$
7+
^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 10, function calls: 2$
88
--
99
^warning: ignoring

‎regression/goto-analyzer/liveness-function-call/test-liveness-show.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,8 @@ main.c
33
--variable-sensitivity --vsd-liveness --show
44
^EXIT=0$
55
^SIGNAL=0$
6-
globalX .* 0 @ \[24\]
6+
globalX .* 0 @ \[21\]
77
globalX .* 1 @ \[0\]
88
globalX .* 2 @ \[3\]
9-
globalX .* TOP @ \[27\]
9+
globalX .* TOP @ \[24\]
1010
--

‎regression/goto-analyzer/liveness-function-call/test-liveness-three-way-show.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,8 @@ main.c
33
--variable-sensitivity --vsd-liveness --three-way-merge --show
44
^EXIT=0$
55
^SIGNAL=0$
6-
globalX .* 0 @ \[24\]
6+
globalX .* 0 @ \[21\]
77
globalX .* 1 @ \[0\]
88
globalX .* 2 @ \[3\]
9-
globalX .* TOP @ \[27\]
9+
globalX .* TOP @ \[24\]
1010
--

‎regression/goto-analyzer/liveness-function-call/test-write-location-show.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--variable-sensitivity --show
44
^EXIT=0$
55
^SIGNAL=0$
6-
globalX .* 0 @ \[24\]
6+
globalX .* 0 @ \[21\]
77
globalX .* 1 @ \[0\]
88
globalX .* TOP @ \[0, 3\]
99
--

‎regression/goto-analyzer/liveness-function-call/test-write-location-three-way-show.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--variable-sensitivity --three-way-merge --show
44
^EXIT=0$
55
^SIGNAL=0$
6-
globalX .* 0 @ \[24\]
6+
globalX .* 0 @ \[21\]
77
globalX .* 1 @ \[0\]
88
globalX .* 2 @ \[3\]
99
--

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

Lines changed: 26 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -6,31 +6,29 @@ activate-multi-line-match
66
^EXIT=0$
77
^SIGNAL=0$
88
main#return_value \(\) -> TOP @ \[1\]
9-
__CPROVER_dead_object \(\) -> TOP @ \[5\]
10-
__CPROVER_deallocated \(\) -> TOP @ \[6\]
11-
__CPROVER_malloc_is_new_array \(\) -> FALSE @ \[7\]
12-
__CPROVER_memory_leak \(\) -> TOP @ \[9\]
13-
__CPROVER_new_object \(\) -> TOP @ \[10\]
14-
__CPROVER_next_thread_key \(\) -> 0ul @ \[12\]
15-
__CPROVER_rounding_mode \(\) -> 0 @ \[13\]
16-
__CPROVER_thread_id \(\) -> 0ul @ \[14\]
17-
__CPROVER_threads_exited \(\) -> TOP @ \[17\]
18-
do_arrays::1::bool_ \(\) -> TOP @ \[19\]
19-
do_arrays::1::bool_1 \(\) -> TOP @ \[20\]
20-
do_arrays::1::bool_2 \(\) -> TOP @ \[21\]
21-
do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[23\]\n\} @ \[23\]
22-
do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[23\]\n\[1\] = 20 @ \[24\]\n\} @ \[24\]
23-
do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[25\]\n\[1\] = 20 @ \[24\]\n\} @ \[25\]
24-
do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[25\]\n\[1\] = 40 @ \[26\]\n\} @ \[26\]
25-
do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[25\]\n\[1\] = 30 @ \[27\]\n\} @ \[27\]
26-
do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[28\]\n\[1\] = 30 @ \[27\]\n\} @ \[28\]
27-
do_arrays::1::x \(\) -> \{\[0\] = 5 @ \[29\]\n\[1\] = 30 @ \[27\]\n\} @ \[29\]
28-
do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[30\]\n\[1\] = 30 @ \[27\]\n\} @ \[30\]
29-
do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[30\]\n\[1\] = 10 @ \[31\]\n\} @ \[31\]
30-
do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[33\]\n\[1\] = 10 @ \[31\]\n\} @ \[33\]
31-
do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[33\, 35\]\n\[1\] = 10 @ \[31\]\n\} @ \[33\, 35\]
32-
do_arrays::1::x \(\) -> \{\[0\] = 0 @ \[37]\n\[1\] = 10 @ \[31\]\n\} @ \[37\]
33-
do_arrays::1::x \(\) -> \{\[0\] = 3 @ \[39]\n\[1\] = 10 @ \[31\]\n\} @ \[39\]
34-
do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[39\, 41]\n\[1\] = 10 @ \[31\]\n\} @ \[39\, 41\]
35-
do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[39\, 41\, 44]\n\[1\] = 10 @ \[46\]\n\} @ \[46\]
36-
do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[47]\n\[1\] = 10 @ \[46\]\n\} @ \[47\]
9+
__CPROVER_dead_object \(\) -> TOP @ \[4\]
10+
__CPROVER_deallocated \(\) -> TOP @ \[5\]
11+
__CPROVER_memory_leak \(\) -> TOP @ \[7\]
12+
__CPROVER_next_thread_key \(\) -> 0ul @ \[9\]
13+
__CPROVER_rounding_mode \(\) -> 0 @ \[10\]
14+
__CPROVER_thread_id \(\) -> 0ul @ \[11\]
15+
__CPROVER_threads_exited \(\) -> TOP @ \[14\]
16+
do_arrays::1::bool_ \(\) -> TOP @ \[16\]
17+
do_arrays::1::bool_1 \(\) -> TOP @ \[17\]
18+
do_arrays::1::bool_2 \(\) -> TOP @ \[18\]
19+
do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[20\]\n\} @ \[20\]
20+
do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[20\]\n\[1\] = 20 @ \[21\]\n\} @ \[21\]
21+
do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[22\]\n\[1\] = 20 @ \[21\]\n\} @ \[22\]
22+
do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[22\]\n\[1\] = 40 @ \[23\]\n\} @ \[23\]
23+
do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[22\]\n\[1\] = 30 @ \[24\]\n\} @ \[24\]
24+
do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[25\]\n\[1\] = 30 @ \[24\]\n\} @ \[25\]
25+
do_arrays::1::x \(\) -> \{\[0\] = 5 @ \[26\]\n\[1\] = 30 @ \[24\]\n\} @ \[26\]
26+
do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[27\]\n\[1\] = 30 @ \[24\]\n\} @ \[27\]
27+
do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[27\]\n\[1\] = 10 @ \[28\]\n\} @ \[28\]
28+
do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[30\]\n\[1\] = 10 @ \[28\]\n\} @ \[30\]
29+
do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[30\, 32\]\n\[1\] = 10 @ \[28\]\n\} @ \[30\, 32\]
30+
do_arrays::1::x \(\) -> \{\[0\] = 0 @ \[34]\n\[1\] = 10 @ \[28\]\n\} @ \[34\]
31+
do_arrays::1::x \(\) -> \{\[0\] = 3 @ \[36]\n\[1\] = 10 @ \[28\]\n\} @ \[36\]
32+
do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[36\, 38]\n\[1\] = 10 @ \[28\]\n\} @ \[36\, 38\]
33+
do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[36\, 38\, 41]\n\[1\] = 10 @ \[43\]\n\} @ \[43\]
34+
do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[44]\n\[1\] = 10 @ \[43\]\n\} @ \[44\]

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

Lines changed: 25 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -6,30 +6,28 @@ activate-multi-line-match
66
^EXIT=0$
77
^SIGNAL=0$
88
main#return_value \(\) -> TOP @ \[1\]
9-
__CPROVER_dead_object \(\) -> TOP @ \[5\]
10-
__CPROVER_deallocated \(\) -> TOP @ \[6\]
11-
__CPROVER_malloc_is_new_array \(\) -> FALSE @ \[7\]
12-
__CPROVER_memory_leak \(\) -> TOP @ \[9\]
13-
__CPROVER_new_object \(\) -> TOP @ \[10\]
14-
__CPROVER_next_thread_key \(\) -> 0ul @ \[12\]
15-
__CPROVER_rounding_mode \(\) -> 0 @ \[13\]
16-
__CPROVER_thread_id \(\) -> 0ul @ \[14\]
17-
__CPROVER_threads_exited \(\) -> TOP @ \[17\]
18-
do_pointers::1::bool_ \(\) -> TOP @ \[19\]
19-
do_pointers::1::bool_1 \(\) -> TOP @ \[20\]
20-
do_pointers::1::bool_2 \(\) -> TOP @ \[21\]
21-
do_pointers::1::x \(\) -> TOP @ \[22\]
22-
do_pointers::1::x \(\) -> 10 @ \[23\]
23-
do_pointers::1::x_p \(\) -> TOP @ \[24\]
24-
do_pointers::1::y \(\) -> TOP @ \[25\]
25-
do_pointers::1::y \(\) -> 20 @ \[26\]
26-
do_pointers::1::y_p \(\) -> TOP @ \[27\]
27-
do_pointers::1::x_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[28\]
28-
do_pointers::1::x \(\) -> 30 @ \[29\]
29-
do_pointers::1::x \(\) -> 40 @ \[30\]
30-
do_pointers::1::x \(\) -> TOP @ \[31\]
31-
do_pointers::1::x \(\) -> 50 @ \[32\]
32-
do_pointers::1::y_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[33\]
33-
do_pointers::1::x \(\) -> 60 @ \[34\]
34-
do_pointers::1::j \(\) -> TOP @ \[35\]
35-
do_pointers::1::j \(\) -> 60 @ \[36\]
9+
__CPROVER_dead_object \(\) -> TOP @ \[4\]
10+
__CPROVER_deallocated \(\) -> TOP @ \[5\]
11+
__CPROVER_memory_leak \(\) -> TOP @ \[7\]
12+
__CPROVER_next_thread_key \(\) -> 0ul @ \[9\]
13+
__CPROVER_rounding_mode \(\) -> 0 @ \[10\]
14+
__CPROVER_thread_id \(\) -> 0ul @ \[11\]
15+
__CPROVER_threads_exited \(\) -> TOP @ \[14\]
16+
do_pointers::1::bool_ \(\) -> TOP @ \[16\]
17+
do_pointers::1::bool_1 \(\) -> TOP @ \[17\]
18+
do_pointers::1::bool_2 \(\) -> TOP @ \[18\]
19+
do_pointers::1::x \(\) -> TOP @ \[19\]
20+
do_pointers::1::x \(\) -> 10 @ \[20\]
21+
do_pointers::1::x_p \(\) -> TOP @ \[21\]
22+
do_pointers::1::y \(\) -> TOP @ \[22\]
23+
do_pointers::1::y \(\) -> 20 @ \[23\]
24+
do_pointers::1::y_p \(\) -> TOP @ \[24\]
25+
do_pointers::1::x_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[25\]
26+
do_pointers::1::x \(\) -> 30 @ \[26\]
27+
do_pointers::1::x \(\) -> 40 @ \[27\]
28+
do_pointers::1::x \(\) -> TOP @ \[28\]
29+
do_pointers::1::x \(\) -> 50 @ \[29\]
30+
do_pointers::1::y_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[30\]
31+
do_pointers::1::x \(\) -> 60 @ \[31\]
32+
do_pointers::1::j \(\) -> TOP @ \[32\]
33+
do_pointers::1::j \(\) -> 60 @ \[33\]

0 commit comments

Comments
 (0)