Skip to content

Commit edbdc4f

Browse files
author
martin
committed
Update regression tests to cope with changes to initialisation
A recent PR has removed a couple of the in-built global variables that are used for modelling the C standard library. This has a knock on effect for the line numbers in the tests of dependency graphs.
1 parent 9561317 commit edbdc4f

File tree

17 files changed

+200
-200
lines changed

17 files changed

+200
-200
lines changed

‎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: 8, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 18, function calls: 2$
6+
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
7+
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 17, 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: 9, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 17, function calls: 2$
6+
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
7+
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 16, 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: 9, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 17, function calls: 2$
6+
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
7+
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 16, 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: 9, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 17, function calls: 2$
6+
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
7+
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 16, 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: 10, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 19, function calls: 2$
6+
^Simplified: assert: 1, assume: 0, goto: 3, assigns: 9, function calls: 0$
7+
^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 18, 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 --simplify out.gb
44
^EXIT=0$
55
^SIGNAL=0$
6-
^Simplified: assert: 1, assume: 0, goto: 2, assigns: 9, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 3, assigns: 18, function calls: 2$
6+
^Simplified: assert: 1, assume: 0, goto: 2, assigns: 8, function calls: 0$
7+
^Unmodified: assert: 0, assume: 0, goto: 3, assigns: 17, 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 --simplify out.gb
44
^EXIT=0$
55
^SIGNAL=0$
6-
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 9, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 15, function calls: 2$
6+
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
7+
^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 14, 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: 9, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 15, function calls: 2$
6+
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
7+
^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 14, 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: 8, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 16, function calls: 2$
6+
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
7+
^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 15, function calls: 2$
88
--
99
^warning: ignoring

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

Lines changed: 28 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -8,31 +8,31 @@ activate-multi-line-match
88
main#return_value \(\) -> TOP @ \[1\]
99
__CPROVER_dead_object \(\) -> TOP @ \[5\]
1010
__CPROVER_deallocated \(\) -> TOP @ \[6\]
11-
__CPROVER_malloc_is_new_array \(\) -> FALSE @ \[10\]
12-
__CPROVER_malloc_object \(\) -> TOP @ \[12\]
13-
__CPROVER_malloc_size \(\) -> 0ull? @ \[13\]
14-
__CPROVER_memory_leak \(\) -> TOP @ \[15\]
15-
__CPROVER_next_thread_id \(\) -> 0ul @ \[16\]
16-
__CPROVER_pipe_count \(\) -> 0u @ \[18\]
17-
__CPROVER_rounding_mode \(\) -> 0 @ \[19\]
18-
__CPROVER_thread_id \(\) -> 0ul @ \[20\]
19-
__CPROVER_threads_exited \(\) -> TOP @ \[23\]
20-
do_arrays::1::bool_ \(\) -> TOP @ \[25\]
21-
do_arrays::1::bool_1 \(\) -> TOP @ \[26\]
22-
do_arrays::1::bool_2 \(\) -> TOP @ \[27\]
23-
do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[29\]\n\} @ \[29\]
24-
do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[29\]\n\[1\] = 20 @ \[30\]\n\} @ \[30\]
25-
do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[31\]\n\[1\] = 20 @ \[30\]\n\} @ \[31\]
26-
do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[31\]\n\[1\] = 40 @ \[32\]\n\} @ \[32\]
27-
do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[31\]\n\[1\] = 30 @ \[33\]\n\} @ \[33\]
28-
do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[34\]\n\[1\] = 30 @ \[33\]\n\} @ \[34\]
29-
do_arrays::1::x \(\) -> \{\[0\] = 5 @ \[35\]\n\[1\] = 30 @ \[33\]\n\} @ \[35\]
30-
do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[36\]\n\[1\] = 30 @ \[33\]\n\} @ \[36\]
31-
do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[36\]\n\[1\] = 10 @ \[37\]\n\} @ \[37\]
32-
do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[39\]\n\[1\] = 10 @ \[37\]\n\} @ \[39\]
33-
do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[39\, 41\]\n\[1\] = 10 @ \[37\]\n\} @ \[39\, 41\]
34-
do_arrays::1::x \(\) -> \{\[0\] = 0 @ \[43]\n\[1\] = 10 @ \[37\]\n\} @ \[43\]
35-
do_arrays::1::x \(\) -> \{\[0\] = 3 @ \[45]\n\[1\] = 10 @ \[37\]\n\} @ \[45\]
36-
do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[45\, 47]\n\[1\] = 10 @ \[37\]\n\} @ \[45\, 47\]
37-
do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[45\, 47\, 50]\n\[1\] = 10 @ \[52\]\n\} @ \[52\]
38-
do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[53]\n\[1\] = 10 @ \[52\]\n\} @ \[53\]
11+
__CPROVER_malloc_is_new_array \(\) -> FALSE @ \[9\]
12+
__CPROVER_malloc_object \(\) -> TOP @ \[10\]
13+
__CPROVER_malloc_size \(\) -> 0ull? @ \[11\]
14+
__CPROVER_memory_leak \(\) -> TOP @ \[13\]
15+
__CPROVER_next_thread_key \(\) -> 0ul @ \[15\]
16+
__CPROVER_pipe_count \(\) -> 0u @ \[16\]
17+
__CPROVER_rounding_mode \(\) -> 0 @ \[17\]
18+
__CPROVER_thread_id \(\) -> 0ul @ \[18\]
19+
__CPROVER_threads_exited \(\) -> TOP @ \[21\]
20+
do_arrays::1::bool_ \(\) -> TOP @ \[23\]
21+
do_arrays::1::bool_1 \(\) -> TOP @ \[24\]
22+
do_arrays::1::bool_2 \(\) -> TOP @ \[25\]
23+
do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[27\]\n\} @ \[27\]
24+
do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[27\]\n\[1\] = 20 @ \[28\]\n\} @ \[28\]
25+
do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[29\]\n\[1\] = 20 @ \[28\]\n\} @ \[29\]
26+
do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[29\]\n\[1\] = 40 @ \[30\]\n\} @ \[30\]
27+
do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[29\]\n\[1\] = 30 @ \[31\]\n\} @ \[31\]
28+
do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[32\]\n\[1\] = 30 @ \[31\]\n\} @ \[32\]
29+
do_arrays::1::x \(\) -> \{\[0\] = 5 @ \[33\]\n\[1\] = 30 @ \[31\]\n\} @ \[33\]
30+
do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[34\]\n\[1\] = 30 @ \[31\]\n\} @ \[34\]
31+
do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[34\]\n\[1\] = 10 @ \[35\]\n\} @ \[35\]
32+
do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[37\]\n\[1\] = 10 @ \[35\]\n\} @ \[37\]
33+
do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[37\, 39\]\n\[1\] = 10 @ \[35\]\n\} @ \[37\, 39\]
34+
do_arrays::1::x \(\) -> \{\[0\] = 0 @ \[41]\n\[1\] = 10 @ \[35\]\n\} @ \[41\]
35+
do_arrays::1::x \(\) -> \{\[0\] = 3 @ \[43]\n\[1\] = 10 @ \[35\]\n\} @ \[43\]
36+
do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[43\, 45]\n\[1\] = 10 @ \[35\]\n\} @ \[43\, 45\]
37+
do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[43\, 45\, 48]\n\[1\] = 10 @ \[50\]\n\} @ \[50\]
38+
do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[51]\n\[1\] = 10 @ \[50\]\n\} @ \[51\]

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

Lines changed: 27 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -8,30 +8,30 @@ activate-multi-line-match
88
main#return_value \(\) -> TOP @ \[1\]
99
__CPROVER_dead_object \(\) -> TOP @ \[5\]
1010
__CPROVER_deallocated \(\) -> TOP @ \[6\]
11-
__CPROVER_malloc_is_new_array \(\) -> FALSE @ \[10\]
12-
__CPROVER_malloc_object \(\) -> TOP @ \[12\]
13-
__CPROVER_malloc_size \(\) -> 0ull? @ \[13\]
14-
__CPROVER_memory_leak \(\) -> TOP @ \[15\]
15-
__CPROVER_next_thread_id \(\) -> 0ul @ \[16\]
16-
__CPROVER_pipe_count \(\) -> 0u @ \[18\]
17-
__CPROVER_rounding_mode \(\) -> 0 @ \[19\]
18-
__CPROVER_thread_id \(\) -> 0ul @ \[20\]
19-
__CPROVER_threads_exited \(\) -> TOP @ \[23\]
20-
do_pointers::1::bool_ \(\) -> TOP @ \[25\]
21-
do_pointers::1::bool_1 \(\) -> TOP @ \[26\]
22-
do_pointers::1::bool_2 \(\) -> TOP @ \[27\]
23-
do_pointers::1::x \(\) -> TOP @ \[28\]
24-
do_pointers::1::x \(\) -> 10 @ \[29\]
25-
do_pointers::1::x_p \(\) -> TOP @ \[30\]
26-
do_pointers::1::y \(\) -> TOP @ \[31\]
27-
do_pointers::1::y \(\) -> 20 @ \[32\]
28-
do_pointers::1::y_p \(\) -> TOP @ \[33\]
29-
do_pointers::1::x_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[34\]
30-
do_pointers::1::x \(\) -> 30 @ \[35\]
31-
do_pointers::1::x \(\) -> 40 @ \[36\]
32-
do_pointers::1::x \(\) -> TOP @ \[37\]
33-
do_pointers::1::x \(\) -> 50 @ \[38\]
34-
do_pointers::1::y_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[39\]
35-
do_pointers::1::x \(\) -> 60 @ \[40\]
36-
do_pointers::1::j \(\) -> TOP @ \[41\]
37-
do_pointers::1::j \(\) -> 60 @ \[42\]
11+
__CPROVER_malloc_is_new_array \(\) -> FALSE @ \[9\]
12+
__CPROVER_malloc_object \(\) -> TOP @ \[10\]
13+
__CPROVER_malloc_size \(\) -> 0ull? @ \[11\]
14+
__CPROVER_memory_leak \(\) -> TOP @ \[13\]
15+
__CPROVER_next_thread_id \(\) -> 0ul @ \[14\]
16+
__CPROVER_pipe_count \(\) -> 0u @ \[16\]
17+
__CPROVER_rounding_mode \(\) -> 0 @ \[17\]
18+
__CPROVER_thread_id \(\) -> 0ul @ \[18\]
19+
__CPROVER_threads_exited \(\) -> TOP @ \[21\]
20+
do_pointers::1::bool_ \(\) -> TOP @ \[23\]
21+
do_pointers::1::bool_1 \(\) -> TOP @ \[24\]
22+
do_pointers::1::bool_2 \(\) -> TOP @ \[25\]
23+
do_pointers::1::x \(\) -> TOP @ \[26\]
24+
do_pointers::1::x \(\) -> 10 @ \[27\]
25+
do_pointers::1::x_p \(\) -> TOP @ \[28\]
26+
do_pointers::1::y \(\) -> TOP @ \[29\]
27+
do_pointers::1::y \(\) -> 20 @ \[30\]
28+
do_pointers::1::y_p \(\) -> TOP @ \[31\]
29+
do_pointers::1::x_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[32\]
30+
do_pointers::1::x \(\) -> 30 @ \[33\]
31+
do_pointers::1::x \(\) -> 40 @ \[34\]
32+
do_pointers::1::x \(\) -> TOP @ \[35\]
33+
do_pointers::1::x \(\) -> 50 @ \[36\]
34+
do_pointers::1::y_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[37\]
35+
do_pointers::1::x \(\) -> 60 @ \[38\]
36+
do_pointers::1::j \(\) -> TOP @ \[39\]
37+
do_pointers::1::j \(\) -> 60 @ \[40\]

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

Lines changed: 32 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -8,36 +8,36 @@ activate-multi-line-match
88
main#return_value \(\) -> TOP @ \[1\]
99
__CPROVER_dead_object \(\) -> TOP @ \[5\]
1010
__CPROVER_deallocated \(\) -> TOP @ \[6\]
11-
__CPROVER_malloc_is_new_array \(\) -> FALSE @ \[10\]
12-
__CPROVER_malloc_object \(\) -> TOP @ \[12\]
13-
__CPROVER_malloc_size \(\) -> 0ull? @ \[13\]
14-
__CPROVER_memory_leak \(\) -> TOP @ \[15\]
15-
__CPROVER_next_thread_id \(\) -> 0ul @ \[16\]
16-
__CPROVER_pipe_count \(\) -> 0u @ \[18\]
17-
__CPROVER_rounding_mode \(\) -> 0 @ \[19\]
18-
__CPROVER_thread_id \(\) -> 0ul @ \[20\]
19-
__CPROVER_threads_exited \(\) -> TOP @ \[23\]
20-
do_structs::1::bool_ \(\) -> TOP @ \[25\]
21-
do_structs::1::bool_1 \(\) -> TOP @ \[26\]
22-
do_structs::1::bool_2 \(\) -> TOP @ \[27\]
23-
do_structs::1::st \(\) -> \{\} @ \[28\]
24-
do_structs::1::st \(\) -> \{.x=10 @ \[29\]\} @ \[29\]
25-
do_structs::1::st \(\) -> \{.x=10 @ \[29\]\, .y=20 @ \[30\]\} @ \[30\]
26-
do_structs::1::st \(\) -> \{.x=30 @ \[31\]\, .y=20 @ \[30\]\} @ \[31\]
27-
do_structs::1::st \(\) -> \{.x=30 @ \[31\]\, .y=40 @ \[32\]\} @ \[32\]
28-
do_structs::1::st \(\) -> \{.x=30 @ \[31\]\, .y=30 @ \[33\]\} @ \[33\]
29-
do_structs::1::st \(\) -> \{.x=30 @ \[34\]\, .y=30 @ \[33\]\} @ \[34\]
30-
do_structs::1::st \(\) -> \{.x=5 @ \[35\]\, .y=30 @ \[33\]\} @ \[35\]
31-
do_structs::1::st \(\) -> \{.x=15 @ \[36\]\, .y=30 @ \[33\]\} @ \[36\]
32-
do_structs::1::st \(\) -> \{.x=15 @ \[36\]\, .y=10 @ \[37\]\} @ \[37\]
33-
do_structs::1::st \(\) -> \{.x=20 @ \[39\]\, .y=10 @ \[37\]\} @ \[39\]
34-
do_structs::1::st \(\) -> \{.x=20 @ \[39\, 41\]\, .y=10 @ \[37\]\} @ \[39\, 41\]
35-
do_structs::1::st \(\) -> \{.x=0 @ \[43\]\, .y=10 @ \[37\]\} @ \[43\]
36-
do_structs::1::st \(\) -> \{.x=3 @ \[45\]\, .y=10 @ \[37\]\} @ \[45\]
37-
do_structs::1::st \(\) -> \{.x=TOP @ \[45\, 47\]\, .y=10 @ \[37\]\} @ \[45\, 47\]
38-
do_structs::1::st \(\) -> \{.x=TOP @ \[45\, 47\, 50\]\, .y=10 @ \[37\]\} @ \[45\, 47\, 50\]
39-
do_structs::1::st \(\) -> \{.x=TOP @ \[45\, 47\, 50\]\, .y=10 @ \[52\]\} @ \[52\]
40-
do_structs::1::st \(\) -> \{.x=20 @ \[53\]\, .y=10 @ \[52\]\} @ \[53\]
41-
do_structs::1::new_age \(\) -> \{\} @ \[54\]
42-
do_structs::1::new_age \(\) -> \{.x=20 @ \[55\]\, .y=10 @ \[55\]\} @ \[55\]
11+
__CPROVER_malloc_is_new_array \(\) -> FALSE @ \[9\]
12+
__CPROVER_malloc_object \(\) -> TOP @ \[10\]
13+
__CPROVER_malloc_size \(\) -> 0ull? @ \[11\]
14+
__CPROVER_memory_leak \(\) -> TOP @ \[13\]
15+
__CPROVER_next_thread_id \(\) -> 0ul @ \[14\]
16+
__CPROVER_pipe_count \(\) -> 0u @ \[16\]
17+
__CPROVER_rounding_mode \(\) -> 0 @ \[17\]
18+
__CPROVER_thread_id \(\) -> 0ul @ \[18\]
19+
__CPROVER_threads_exited \(\) -> TOP @ \[21\]
20+
do_structs::1::bool_ \(\) -> TOP @ \[23\]
21+
do_structs::1::bool_1 \(\) -> TOP @ \[24\]
22+
do_structs::1::bool_2 \(\) -> TOP @ \[25\]
23+
do_structs::1::st \(\) -> \{\} @ \[26\]
24+
do_structs::1::st \(\) -> \{.x=10 @ \[27\]\} @ \[27\]
25+
do_structs::1::st \(\) -> \{.x=10 @ \[27\]\, .y=20 @ \[28\]\} @ \[28\]
26+
do_structs::1::st \(\) -> \{.x=30 @ \[29\]\, .y=20 @ \[28\]\} @ \[29\]
27+
do_structs::1::st \(\) -> \{.x=30 @ \[29\]\, .y=40 @ \[30\]\} @ \[30\]
28+
do_structs::1::st \(\) -> \{.x=30 @ \[29\]\, .y=30 @ \[31\]\} @ \[31\]
29+
do_structs::1::st \(\) -> \{.x=30 @ \[32\]\, .y=30 @ \[31\]\} @ \[32\]
30+
do_structs::1::st \(\) -> \{.x=5 @ \[33\]\, .y=30 @ \[31\]\} @ \[33\]
31+
do_structs::1::st \(\) -> \{.x=15 @ \[34\]\, .y=30 @ \[31\]\} @ \[34\]
32+
do_structs::1::st \(\) -> \{.x=15 @ \[34\]\, .y=10 @ \[35\]\} @ \[35\]
33+
do_structs::1::st \(\) -> \{.x=20 @ \[37\]\, .y=10 @ \[35\]\} @ \[37\]
34+
do_structs::1::st \(\) -> \{.x=20 @ \[37\, 39\]\, .y=10 @ \[35\]\} @ \[37\, 39\]
35+
do_structs::1::st \(\) -> \{.x=0 @ \[41\]\, .y=10 @ \[35\]\} @ \[41\]
36+
do_structs::1::st \(\) -> \{.x=3 @ \[43\]\, .y=10 @ \[35\]\} @ \[43\]
37+
do_structs::1::st \(\) -> \{.x=TOP @ \[43\, 45\]\, .y=10 @ \[35\]\} @ \[43\, 45\]
38+
do_structs::1::st \(\) -> \{.x=TOP @ \[43\, 45\, 48\]\, .y=10 @ \[35\]\} @ \[43\, 45\, 48\]
39+
do_structs::1::st \(\) -> \{.x=TOP @ \[43\, 45\, 48\]\, .y=10 @ \[50\]\} @ \[50\]
40+
do_structs::1::st \(\) -> \{.x=20 @ \[51\]\, .y=10 @ \[50\]\} @ \[51\]
41+
do_structs::1::new_age \(\) -> \{\} @ \[52\]
42+
do_structs::1::new_age \(\) -> \{.x=20 @ \[53\]\, .y=10 @ \[53\]\} @ \[53\]
4343
--

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

Lines changed: 39 additions & 39 deletions
Original file line numberDiff line numberDiff line change
@@ -7,43 +7,43 @@ main#return_value \(\) -> TOP @ \[1\]
77
__CPROVER_alloca_object \(\) -> TOP @ \[4\]
88
__CPROVER_dead_object \(\) -> TOP @ \[5\]
99
__CPROVER_deallocated \(\) -> TOP @ \[6\]
10-
__CPROVER_malloc_is_new_array \(\) -> FALSE @ \[10\]
11-
__CPROVER_malloc_object \(\) -> TOP @ \[12\]
12-
__CPROVER_malloc_size \(\) -> 0ull? @ \[13\]
13-
__CPROVER_memory_leak \(\) -> TOP @ \[15\]
14-
__CPROVER_next_thread_id \(\) -> 0ul @ \[16\]
15-
__CPROVER_next_thread_key \(\) -> 0ul @ \[17\]
16-
__CPROVER_pipe_count \(\) -> 0u @ \[18\]
17-
__CPROVER_rounding_mode \(\) -> 0 @ \[19\]
18-
__CPROVER_thread_id \(\) -> 0ul @ \[20\]
19-
__CPROVER_thread_key_dtors \(\) -> TOP @ \[21\]
20-
__CPROVER_thread_keys \(\) -> TOP @ \[22\]
21-
__CPROVER_threads_exited \(\) -> TOP @ \[23\]
22-
global_x \(\) -> 0 @ \[24\]
23-
do_variables::1::bool_ \(\) -> TOP @ \[26\]
24-
do_variables::1::bool_1 \(\) -> TOP @ \[27\]
25-
do_variables::1::bool_2 \(\) -> TOP @ \[28\]
26-
global_x \(\) -> 5 @ \[29\]
27-
do_variables::1::x \(\) -> TOP @ \[30\]
28-
do_variables::1::x \(\) -> 10 @ \[31\]
29-
do_variables::1::y \(\) -> TOP @ \[32\]
30-
do_variables::1::y \(\) -> 20 @ \[33\]
31-
do_variables::1::x \(\) -> 30 @ \[34\]
32-
do_variables::1::y \(\) -> 40 @ \[35\]
33-
do_variables::1::y \(\) -> 30 @ \[36\]
34-
do_variables::1::x \(\) -> 30 @ \[37\]
35-
do_variables::1::x \(\) -> 5 @ \[38\]
36-
do_variables::1::x \(\) -> 15 @ \[39\]
37-
do_variables::1::y \(\) -> 10 @ \[40\]
38-
do_variables::1::x \(\) -> 20 @ \[42\]
39-
do_variables::1::x \(\) -> 20 @ \[42\, 44\]
40-
do_variables::1::x \(\) -> 50 @ \[46\]
41-
do_variables::1::x \(\) -> 20 @ \[48\]
42-
do_variables::1::x \(\) -> TOP @ \[48\, 50\]
43-
do_variables::1::x \(\) -> 0 @ \[52\]
44-
do_variables::1::x \(\) -> 3 @ \[54\]
45-
do_variables::1::x \(\) -> TOP @ \[54\, 56\]
46-
do_variables::1::x \(\) -> TOP @ \[54\, 56\, 59\]
47-
do_variables::1::y \(\) -> 10 @ \[61\]
48-
do_variables::1::x \(\) -> 20 @ \[62\]
10+
__CPROVER_malloc_is_new_array \(\) -> FALSE @ \[9\]
11+
__CPROVER_malloc_object \(\) -> TOP @ \[10\]
12+
__CPROVER_malloc_size \(\) -> 0ull? @ \[11\]
13+
__CPROVER_memory_leak \(\) -> TOP @ \[13\]
14+
__CPROVER_next_thread_id \(\) -> 0ul @ \[14\]
15+
__CPROVER_next_thread_key \(\) -> 0ul @ \[15\]
16+
__CPROVER_pipe_count \(\) -> 0u @ \[16\]
17+
__CPROVER_rounding_mode \(\) -> 0 @ \[17\]
18+
__CPROVER_thread_id \(\) -> 0ul @ \[18\]
19+
__CPROVER_thread_key_dtors \(\) -> TOP @ \[19\]
20+
__CPROVER_thread_keys \(\) -> TOP @ \[20\]
21+
__CPROVER_threads_exited \(\) -> TOP @ \[21\]
22+
global_x \(\) -> 0 @ \[22\]
23+
do_variables::1::bool_ \(\) -> TOP @ \[24\]
24+
do_variables::1::bool_1 \(\) -> TOP @ \[25\]
25+
do_variables::1::bool_2 \(\) -> TOP @ \[26\]
26+
global_x \(\) -> 5 @ \[27\]
27+
do_variables::1::x \(\) -> TOP @ \[28\]
28+
do_variables::1::x \(\) -> 10 @ \[29\]
29+
do_variables::1::y \(\) -> TOP @ \[30\]
30+
do_variables::1::y \(\) -> 20 @ \[31\]
31+
do_variables::1::x \(\) -> 30 @ \[32\]
32+
do_variables::1::y \(\) -> 40 @ \[33\]
33+
do_variables::1::y \(\) -> 30 @ \[34\]
34+
do_variables::1::x \(\) -> 30 @ \[35\]
35+
do_variables::1::x \(\) -> 5 @ \[36\]
36+
do_variables::1::x \(\) -> 15 @ \[37\]
37+
do_variables::1::y \(\) -> 10 @ \[38\]
38+
do_variables::1::x \(\) -> 20 @ \[40\]
39+
do_variables::1::x \(\) -> 20 @ \[40\, 42\]
40+
do_variables::1::x \(\) -> 50 @ \[44\]
41+
do_variables::1::x \(\) -> 20 @ \[46\]
42+
do_variables::1::x \(\) -> TOP @ \[46\, 48\]
43+
do_variables::1::x \(\) -> 0 @ \[50\]
44+
do_variables::1::x \(\) -> 3 @ \[52\]
45+
do_variables::1::x \(\) -> TOP @ \[52\, 54\]
46+
do_variables::1::x \(\) -> TOP @ \[52\, 54\, 57\]
47+
do_variables::1::y \(\) -> 10 @ \[59\]
48+
do_variables::1::x \(\) -> 20 @ \[60\]
4949
--

‎regression/goto-analyzer/sensitivity-test-data-dependency-context/test.desc

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -5,8 +5,8 @@ data-dependency-context.c
55
activate-multi-line-match
66
^EXIT=0$
77
^SIGNAL=0$
8-
st \(\) -> \{.a=.* @ \[2, 57\]\[Data dependencies: 57, 2\]\[Data dominators: \], .b=.* @ \[5, 57\]\[Data dependencies: 57, 5\]\[Data dominators: \]\} @ \[2, 5, 57\]\[Data dependencies: 57, 5, 2\]\[Data dominators: 57\]
9-
ar \(\) -> \{\[0\] = TOP @ \[11\, 51\]\[Data dependencies: 51\, 11\]\[Data dominators: \]\n\[1\] = TOP @ \[14\, 51\]\[Data dependencies: 51\, 14\]\[Data dominators: \]\n\} @ \[11\, 14\, 51\]\[Data dependencies: 51\, 14\, 11\]\[Data dominators: 51\]
10-
arr \(\) -> \{\[0\] = 1 @ \[19\]\[Data dependencies: 19\]\[Data dominators: 19\]\n\[1\] = 2 @ \[20\]\[Data dependencies: 20\]\[Data dominators: 20\]\n\[2\] = TOP @ \[21, 23\]\[Data dependencies: 23, 21\]\[Data dominators: \]\n\} @ \[21, 23\]\[Data dependencies: 23, 21\]\[Data dominators: 52\]
8+
st \(\) -> \{.a=.* @ \[2, 55\]\[Data dependencies: 55, 2\]\[Data dominators: \], .b=.* @ \[5, 55\]\[Data dependencies: 55, 5\]\[Data dominators: \]\} @ \[2, 5, 55\]\[Data dependencies: 55, 5, 2\]\[Data dominators: 55\]
9+
ar \(\) -> \{\[0\] = TOP @ \[11\, 49\]\[Data dependencies: 49\, 11\]\[Data dominators: \]\n\[1\] = TOP @ \[14\, 49\]\[Data dependencies: 49\, 14\]\[Data dominators: \]\n\} @ \[11\, 14\, 49\]\[Data dependencies: 49\, 14\, 11\]\[Data dominators: 49\]
10+
arr \(\) -> \{\[0\] = 1 @ \[19\]\[Data dependencies: 19\]\[Data dominators: 19\]\n\[1\] = 2 @ \[20\]\[Data dependencies: 20\]\[Data dominators: 20\]\n\[2\] = TOP @ \[21, 23\]\[Data dependencies: 23, 21\]\[Data dominators: \]\n\} @ \[21, 23\]\[Data dependencies: 23, 21\]\[Data dominators: 50\]
1111
--
1212
^warning: ignoring

0 commit comments

Comments
 (0)