Skip to content

Commit 10bec57

Browse files
tautschnigtautschnig
committed
C library: move pthreads 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 pthreads-related library functions. This removal of unused symbols required adding a symbol into the array_of_bool_as_bitvec test, which previously implicitly relied on those library-specific symbols in the patterns being tested for.
1 parent 297f294 commit 10bec57

File tree

34 files changed

+227
-235
lines changed

34 files changed

+227
-235
lines changed

‎regression/cbmc-concurrency/thread_chain_cbmc1/main.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@
1818
typedef unsigned long thread_id_t;
1919

2020
// Internal unbounded array indexed by local thread identifiers
21-
extern __CPROVER_bool __CPROVER_threads_exited[];
21+
__CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint];
2222

2323
// A thread_chain is like a chain of threads `f, g, ...` where `f`
2424
// must terminate before `g` can start to run, and so forth.

‎regression/cbmc-concurrency/thread_chain_cbmc2/main.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@
1818
typedef unsigned long thread_id_t;
1919

2020
// Internal unbounded array indexed by local thread identifiers
21-
extern __CPROVER_bool __CPROVER_threads_exited[];
21+
__CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint];
2222

2323
// A thread_chain is like a chain of threads `f, g, ...` where `f`
2424
// must terminate before `g` can start to run, and so forth.

‎regression/cbmc/array_of_bool_as_bitvec/main.c

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@
33
#include <stdlib.h>
44

55
__CPROVER_bool w[8];
6+
__CPROVER_bool v[__CPROVER_constant_infinity_uint];
67

78
void main()
89
{

‎regression/cbmc/array_of_bool_as_bitvec/test-smt2-outfile.desc

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,15 @@
11
CORE broken-smt-backend
22
main.c
33
--smt2 --outfile -
4-
\(= \(select array_of\.2 i\) \(ite false #b1 #b0\)\)
5-
\(= \(select array\.3 \(\(_ zero_extend 32\) \|main::1::idx!0@1#1\|\)\) #b1\)
6-
\(= \(select array\.3 \(_ bv\d+ 64\)\) \(ite false #b1 #b0\)\)
4+
\(= \(select array_of\.0 i\) \(ite false #b1 #b0\)\)
5+
\(= \(select array\.1 \(\(_ zero_extend 32\) \|main::1::idx!0@1#1\|\)\) #b1\)
6+
\(= \(select array\.1 \(_ bv\d+ 64\)\) \(ite false #b1 #b0\)\)
77
^EXIT=0$
88
^SIGNAL=0$
99
--
10-
\(= \(select array_of\.2 i\) false\)
11-
\(= \(select array\.3 \(\(_ zero_extend 32\) \|main::1::idx!0@1#1\|\)\) #b1 #b0\)
12-
\(= \(select array\.3 \(_ bv\d+ 64\)\) false\)
10+
\(= \(select array_of\.0 i\) false\)
11+
\(= \(select array\.1 \(\(_ zero_extend 32\) \|main::1::idx!0@1#1\|\)\) #b1 #b0\)
12+
\(= \(select array\.1 \(_ bv\d+ 64\)\) false\)
1313
--
1414
This test checks for correctness of BitVec-array encoding of Boolean arrays.
1515

‎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: 5, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 12, function calls: 2$
6+
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 2, function calls: 0$
7+
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 9, 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: 5, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 12, function calls: 2$
6+
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 2, function calls: 0$
7+
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 9, 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: 6, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
6+
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 3, function calls: 0$
7+
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 8, 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: 6, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
6+
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 3, function calls: 0$
7+
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 8, 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: 6, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
6+
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 3, function calls: 0$
7+
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 8, 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: 6, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
6+
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 3, function calls: 0$
7+
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 8, 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: 6, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
6+
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 3, function calls: 0$
7+
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 8, 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: 6, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
6+
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 3, function calls: 0$
7+
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 8, 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: 7, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 13, function calls: 2$
6+
^Simplified: assert: 1, assume: 0, goto: 3, assigns: 4, 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_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: 7, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 13, function calls: 2$
6+
^Simplified: assert: 1, assume: 0, goto: 3, assigns: 4, 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_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: 6, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 3, assigns: 12, function calls: 2$
6+
^Simplified: assert: 1, assume: 0, goto: 2, assigns: 3, function calls: 0$
7+
^Unmodified: assert: 0, assume: 0, goto: 3, assigns: 9, 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: 6, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 9, function calls: 2$
6+
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 3, function calls: 0$
7+
^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 6, 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: 6, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 9, function calls: 2$
6+
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 3, function calls: 0$
7+
^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 6, 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: 5, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 10, function calls: 2$
6+
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 2, function calls: 0$
7+
^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 7, 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: 5, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 10, function calls: 2$
6+
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 2, function calls: 0$
7+
^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 7, 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 @ \[21\]
6+
globalX .* 0 @ \[15\]
77
globalX .* 1 @ \[0\]
88
globalX .* 2 @ \[3\]
9-
globalX .* TOP @ \[24\]
9+
globalX .* TOP @ \[18\]
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 @ \[21\]
6+
globalX .* 0 @ \[15\]
77
globalX .* 1 @ \[0\]
88
globalX .* 2 @ \[3\]
9-
globalX .* TOP @ \[24\]
9+
globalX .* TOP @ \[18\]
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 @ \[21\]
6+
globalX .* 0 @ \[15\]
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 @ \[21\]
6+
globalX .* 0 @ \[15\]
77
globalX .* 1 @ \[0\]
88
globalX .* 2 @ \[3\]
99
--

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

Lines changed: 20 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -9,26 +9,23 @@ main#return_value \(\) -> TOP @ \[1\]
99
__CPROVER_dead_object \(\) -> TOP @ \[4\]
1010
__CPROVER_deallocated \(\) -> TOP @ \[5\]
1111
__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\]
12+
__CPROVER_rounding_mode \(\) -> 0 @ \[8\]
13+
do_arrays::1::bool_ \(\) -> TOP @ \[10\]
14+
do_arrays::1::bool_1 \(\) -> TOP @ \[11\]
15+
do_arrays::1::bool_2 \(\) -> TOP @ \[12\]
16+
do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[14\]\n\} @ \[14\]
17+
do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[14\]\n\[1\] = 20 @ \[15\]\n\} @ \[15\]
18+
do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[16\]\n\[1\] = 20 @ \[15\]\n\} @ \[16\]
19+
do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[16\]\n\[1\] = 40 @ \[17\]\n\} @ \[17\]
20+
do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[16\]\n\[1\] = 30 @ \[18\]\n\} @ \[18\]
21+
do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[19\]\n\[1\] = 30 @ \[18\]\n\} @ \[19\]
22+
do_arrays::1::x \(\) -> \{\[0\] = 5 @ \[20\]\n\[1\] = 30 @ \[18\]\n\} @ \[20\]
23+
do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[21\]\n\[1\] = 30 @ \[18\]\n\} @ \[21\]
24+
do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[21\]\n\[1\] = 10 @ \[22\]\n\} @ \[22\]
25+
do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[24\]\n\[1\] = 10 @ \[22\]\n\} @ \[24\]
26+
do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[24\, 26\]\n\[1\] = 10 @ \[22\]\n\} @ \[24\, 26\]
27+
do_arrays::1::x \(\) -> \{\[0\] = 0 @ \[28]\n\[1\] = 10 @ \[22\]\n\} @ \[28\]
28+
do_arrays::1::x \(\) -> \{\[0\] = 3 @ \[30]\n\[1\] = 10 @ \[22\]\n\} @ \[30\]
29+
do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[30\, 32]\n\[1\] = 10 @ \[22\]\n\} @ \[30\, 32\]
30+
do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[30\, 32\, 35]\n\[1\] = 10 @ \[37\]\n\} @ \[37\]
31+
do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[38]\n\[1\] = 10 @ \[37\]\n\} @ \[38\]

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

Lines changed: 19 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -9,25 +9,22 @@ main#return_value \(\) -> TOP @ \[1\]
99
__CPROVER_dead_object \(\) -> TOP @ \[4\]
1010
__CPROVER_deallocated \(\) -> TOP @ \[5\]
1111
__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\]
12+
__CPROVER_rounding_mode \(\) -> 0 @ \[8\]
13+
do_pointers::1::bool_ \(\) -> TOP @ \[10\]
14+
do_pointers::1::bool_1 \(\) -> TOP @ \[11\]
15+
do_pointers::1::bool_2 \(\) -> TOP @ \[12\]
16+
do_pointers::1::x \(\) -> TOP @ \[13\]
17+
do_pointers::1::x \(\) -> 10 @ \[14\]
18+
do_pointers::1::x_p \(\) -> TOP @ \[15\]
19+
do_pointers::1::y \(\) -> TOP @ \[16\]
20+
do_pointers::1::y \(\) -> 20 @ \[17\]
21+
do_pointers::1::y_p \(\) -> TOP @ \[18\]
22+
do_pointers::1::x_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[19\]
23+
do_pointers::1::x \(\) -> 30 @ \[20\]
24+
do_pointers::1::x \(\) -> 40 @ \[21\]
25+
do_pointers::1::x \(\) -> TOP @ \[22\]
26+
do_pointers::1::x \(\) -> 50 @ \[23\]
27+
do_pointers::1::y_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[24\]
28+
do_pointers::1::x \(\) -> 60 @ \[25\]
29+
do_pointers::1::j \(\) -> TOP @ \[26\]
30+
do_pointers::1::j \(\) -> 60 @ \[27\]

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

Lines changed: 24 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -9,31 +9,28 @@ main#return_value \(\) -> TOP @ \[1\]
99
__CPROVER_dead_object \(\) -> TOP @ \[4\]
1010
__CPROVER_deallocated \(\) -> TOP @ \[5\]
1111
__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_structs::1::bool_ \(\) -> TOP @ \[16\]
17-
do_structs::1::bool_1 \(\) -> TOP @ \[17\]
18-
do_structs::1::bool_2 \(\) -> TOP @ \[18\]
19-
do_structs::1::st \(\) -> \{\} @ \[19\]
20-
do_structs::1::st \(\) -> \{.x=10 @ \[20\]\} @ \[20\]
21-
do_structs::1::st \(\) -> \{.x=10 @ \[20\]\, .y=20 @ \[21\]\} @ \[21\]
22-
do_structs::1::st \(\) -> \{.x=30 @ \[22\]\, .y=20 @ \[21\]\} @ \[22\]
23-
do_structs::1::st \(\) -> \{.x=30 @ \[22\]\, .y=40 @ \[23\]\} @ \[23\]
24-
do_structs::1::st \(\) -> \{.x=30 @ \[22\]\, .y=30 @ \[24\]\} @ \[24\]
25-
do_structs::1::st \(\) -> \{.x=30 @ \[25\]\, .y=30 @ \[24\]\} @ \[25\]
26-
do_structs::1::st \(\) -> \{.x=5 @ \[26\]\, .y=30 @ \[24\]\} @ \[26\]
27-
do_structs::1::st \(\) -> \{.x=15 @ \[27\]\, .y=30 @ \[24\]\} @ \[27\]
28-
do_structs::1::st \(\) -> \{.x=15 @ \[27\]\, .y=10 @ \[28\]\} @ \[28\]
29-
do_structs::1::st \(\) -> \{.x=20 @ \[30\]\, .y=10 @ \[28\]\} @ \[30\]
30-
do_structs::1::st \(\) -> \{.x=20 @ \[30\, 32\]\, .y=10 @ \[28\]\} @ \[30\, 32\]
31-
do_structs::1::st \(\) -> \{.x=0 @ \[34\]\, .y=10 @ \[28\]\} @ \[34\]
32-
do_structs::1::st \(\) -> \{.x=3 @ \[36\]\, .y=10 @ \[28\]\} @ \[36\]
33-
do_structs::1::st \(\) -> \{.x=TOP @ \[36\, 38\]\, .y=10 @ \[28\]\} @ \[36\, 38\]
34-
do_structs::1::st \(\) -> \{.x=TOP @ \[36\, 38\, 41\]\, .y=10 @ \[28\]\} @ \[36\, 38\, 41\]
35-
do_structs::1::st \(\) -> \{.x=TOP @ \[36\, 38\, 41\]\, .y=10 @ \[43\]\} @ \[43\]
36-
do_structs::1::st \(\) -> \{.x=20 @ \[44\]\, .y=10 @ \[43\]\} @ \[44\]
37-
do_structs::1::new_age \(\) -> \{\} @ \[45\]
38-
do_structs::1::new_age \(\) -> \{.x=20 @ \[46\]\, .y=10 @ \[46\]\} @ \[46\]
12+
__CPROVER_rounding_mode \(\) -> 0 @ \[8\]
13+
do_structs::1::bool_ \(\) -> TOP @ \[10\]
14+
do_structs::1::bool_1 \(\) -> TOP @ \[11\]
15+
do_structs::1::bool_2 \(\) -> TOP @ \[12\]
16+
do_structs::1::st \(\) -> \{\} @ \[13\]
17+
do_structs::1::st \(\) -> \{.x=10 @ \[14\]\} @ \[14\]
18+
do_structs::1::st \(\) -> \{.x=10 @ \[14\]\, .y=20 @ \[15\]\} @ \[15\]
19+
do_structs::1::st \(\) -> \{.x=30 @ \[16\]\, .y=20 @ \[15\]\} @ \[16\]
20+
do_structs::1::st \(\) -> \{.x=30 @ \[16\]\, .y=40 @ \[17\]\} @ \[17\]
21+
do_structs::1::st \(\) -> \{.x=30 @ \[16\]\, .y=30 @ \[18\]\} @ \[18\]
22+
do_structs::1::st \(\) -> \{.x=30 @ \[19\]\, .y=30 @ \[18\]\} @ \[19\]
23+
do_structs::1::st \(\) -> \{.x=5 @ \[20\]\, .y=30 @ \[18\]\} @ \[20\]
24+
do_structs::1::st \(\) -> \{.x=15 @ \[21\]\, .y=30 @ \[18\]\} @ \[21\]
25+
do_structs::1::st \(\) -> \{.x=15 @ \[21\]\, .y=10 @ \[22\]\} @ \[22\]
26+
do_structs::1::st \(\) -> \{.x=20 @ \[24\]\, .y=10 @ \[22\]\} @ \[24\]
27+
do_structs::1::st \(\) -> \{.x=20 @ \[24\, 26\]\, .y=10 @ \[22\]\} @ \[24\, 26\]
28+
do_structs::1::st \(\) -> \{.x=0 @ \[28\]\, .y=10 @ \[22\]\} @ \[28\]
29+
do_structs::1::st \(\) -> \{.x=3 @ \[30\]\, .y=10 @ \[22\]\} @ \[30\]
30+
do_structs::1::st \(\) -> \{.x=TOP @ \[30\, 32\]\, .y=10 @ \[22\]\} @ \[30\, 32\]
31+
do_structs::1::st \(\) -> \{.x=TOP @ \[30\, 32\, 35\]\, .y=10 @ \[22\]\} @ \[30\, 32\, 35\]
32+
do_structs::1::st \(\) -> \{.x=TOP @ \[30\, 32\, 35\]\, .y=10 @ \[37\]\} @ \[37\]
33+
do_structs::1::st \(\) -> \{.x=20 @ \[38\]\, .y=10 @ \[37\]\} @ \[38\]
34+
do_structs::1::new_age \(\) -> \{\} @ \[39\]
35+
do_structs::1::new_age \(\) -> \{.x=20 @ \[40\]\, .y=10 @ \[40\]\} @ \[40\]
3936
--

0 commit comments

Comments
 (0)