Skip to content

Commit 49fb197

Browse files
authored
Merge pull request #6576 from tautschnig/cleanup/init-function-updates
Make re-building __CPROVER_initialize safe
2 parents bd1b8c2 + e631369 commit 49fb197

File tree

48 files changed

+402
-491
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

48 files changed

+402
-491
lines changed

doc/cprover-manual/properties.md

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -412,3 +412,9 @@ those two options are used, CBMC will assume that `malloc` does not fail.
412412
Malloc may also fail for external reasons which are not modelled by CProver. If
413413
you want to replicate this behaviour use the option `--malloc-may-fail` in
414414
conjunction with one of the above modes of failure.
415+
416+
These malloc failure options need to be set when the C library model is added to
417+
the program. Typically this is upon invoking CBMC, but if the user has chosen to
418+
do so via `goto-instrument --add-library`, then the malloc failure mode needs to
419+
be specified with that `goto-instrument` invocation, i.e., as an option to
420+
`goto-instrument`.

jbmc/src/jbmc/jbmc_parse_options.cpp

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -721,10 +721,6 @@ int jbmc_parse_optionst::get_goto_program(
721721

722722
goto_modelt &goto_model = dynamic_cast<goto_modelt &>(*goto_model_ptr);
723723

724-
// if we added the ansi-c library models here this should also call
725-
// add_malloc_may_fail_variable_initializations(goto_model);
726-
// here
727-
728724
if(cmdline.isset("validate-goto-model"))
729725
{
730726
goto_model.validate();

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,6 @@ main.c
44
^EXIT=0$
55
^SIGNAL=0$
66
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 16, function calls: 2$
7+
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 14, function calls: 2$
88
--
99
^warning: ignoring

regression/goto-analyzer/constant_propagation_01/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,6 @@ main.c
44
^EXIT=0$
55
^SIGNAL=0$
66
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 16, function calls: 2$
7+
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 14, function calls: 2$
88
--
99
^warning: ignoring

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,6 @@ main.c
44
^EXIT=0$
55
^SIGNAL=0$
66
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 15, function calls: 2$
7+
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 13, function calls: 2$
88
--
99
^warning: ignoring

regression/goto-analyzer/constant_propagation_02/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,6 @@ main.c
44
^EXIT=0$
55
^SIGNAL=0$
66
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 15, function calls: 2$
7+
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 13, function calls: 2$
88
--
99
^warning: ignoring

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,6 @@ main.c
44
^EXIT=0$
55
^SIGNAL=0$
66
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 15, function calls: 2$
7+
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 13, function calls: 2$
88
--
99
^warning: ignoring

regression/goto-analyzer/constant_propagation_03/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,6 @@ main.c
44
^EXIT=0$
55
^SIGNAL=0$
66
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 15, function calls: 2$
7+
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 13, function calls: 2$
88
--
99
^warning: ignoring

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,6 @@ main.c
44
^EXIT=0$
55
^SIGNAL=0$
66
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 15, function calls: 2$
7+
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 13, function calls: 2$
88
--
99
^warning: ignoring

regression/goto-analyzer/constant_propagation_04/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,6 @@ main.c
44
^EXIT=0$
55
^SIGNAL=0$
66
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 15, function calls: 2$
7+
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 13, function calls: 2$
88
--
99
^warning: ignoring

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,6 @@ main.c
44
^EXIT=0$
55
^SIGNAL=0$
66
^Simplified: assert: 1, assume: 0, goto: 3, assigns: 9, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 17, function calls: 2$
7+
^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 15, function calls: 2$
88
--
99
^warning: ignoring

regression/goto-analyzer/constant_propagation_07/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,6 @@ main.c
44
^EXIT=0$
55
^SIGNAL=0$
66
^Simplified: assert: 1, assume: 0, goto: 3, assigns: 9, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 17, function calls: 2$
7+
^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 15, function calls: 2$
88
--
99
^warning: ignoring

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,6 @@ main.c
44
^EXIT=0$
55
^SIGNAL=0$
66
^Simplified: assert: 1, assume: 0, goto: 2, assigns: 8, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 3, assigns: 16, function calls: 2$
7+
^Unmodified: assert: 0, assume: 0, goto: 3, assigns: 14, function calls: 2$
88
--
99
^warning: ignoring

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,6 @@ main.c
44
^EXIT=0$
55
^SIGNAL=0$
66
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 13, function calls: 2$
7+
^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 11, function calls: 2$
88
--
99
^warning: ignoring

regression/goto-analyzer/constant_propagation_11/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,6 @@ main.c
44
^EXIT=0$
55
^SIGNAL=0$
66
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 13, function calls: 2$
7+
^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 11, function calls: 2$
88
--
99
^warning: ignoring

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,6 @@ main.c
44
^EXIT=0$
55
^SIGNAL=0$
66
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 14, function calls: 2$
7+
^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 12, function calls: 2$
88
--
99
^warning: ignoring

regression/goto-analyzer/constant_propagation_12/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,6 @@ main.c
44
^EXIT=0$
55
^SIGNAL=0$
66
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 14, function calls: 2$
7+
^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 12, 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 @ \[27\]
6+
globalX .* 0 @ \[25\]
77
globalX .* 1 @ \[0\]
88
globalX .* 2 @ \[3\]
9-
globalX .* TOP @ \[30\]
9+
globalX .* TOP @ \[28\]
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 @ \[27\]
6+
globalX .* 0 @ \[25\]
77
globalX .* 1 @ \[0\]
88
globalX .* 2 @ \[3\]
9-
globalX .* TOP @ \[30\]
9+
globalX .* TOP @ \[28\]
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 @ \[27\]
6+
globalX .* 0 @ \[25\]
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 @ \[27\]
6+
globalX .* 0 @ \[25\]
77
globalX .* 1 @ \[0\]
88
globalX .* 2 @ \[3\]
99
--

regression/goto-analyzer/sensitivity-last-written-locations-arrays/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 @ \[9\]
12-
__CPROVER_memory_leak \(\) -> TOP @ \[11\]
13-
__CPROVER_new_object \(\) -> TOP @ \[12\]
14-
__CPROVER_next_thread_key \(\) -> 0ul @ \[14\]
15-
__CPROVER_pipe_count \(\) -> 0u @ \[15\]
16-
__CPROVER_rounding_mode \(\) -> 0 @ \[16\]
17-
__CPROVER_thread_id \(\) -> 0ul @ \[17\]
18-
__CPROVER_threads_exited \(\) -> TOP @ \[20\]
19-
do_arrays::1::bool_ \(\) -> TOP @ \[22\]
20-
do_arrays::1::bool_1 \(\) -> TOP @ \[23\]
21-
do_arrays::1::bool_2 \(\) -> TOP @ \[24\]
22-
do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[26\]\n\} @ \[26\]
23-
do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[26\]\n\[1\] = 20 @ \[27\]\n\} @ \[27\]
24-
do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[28\]\n\[1\] = 20 @ \[27\]\n\} @ \[28\]
25-
do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[28\]\n\[1\] = 40 @ \[29\]\n\} @ \[29\]
26-
do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[28\]\n\[1\] = 30 @ \[30\]\n\} @ \[30\]
27-
do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[31\]\n\[1\] = 30 @ \[30\]\n\} @ \[31\]
28-
do_arrays::1::x \(\) -> \{\[0\] = 5 @ \[32\]\n\[1\] = 30 @ \[30\]\n\} @ \[32\]
29-
do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[33\]\n\[1\] = 30 @ \[30\]\n\} @ \[33\]
30-
do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[33\]\n\[1\] = 10 @ \[34\]\n\} @ \[34\]
31-
do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[36\]\n\[1\] = 10 @ \[34\]\n\} @ \[36\]
32-
do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[36\, 38\]\n\[1\] = 10 @ \[34\]\n\} @ \[36\, 38\]
33-
do_arrays::1::x \(\) -> \{\[0\] = 0 @ \[40]\n\[1\] = 10 @ \[34\]\n\} @ \[40\]
34-
do_arrays::1::x \(\) -> \{\[0\] = 3 @ \[42]\n\[1\] = 10 @ \[34\]\n\} @ \[42\]
35-
do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[42\, 44]\n\[1\] = 10 @ \[34\]\n\} @ \[42\, 44\]
36-
do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[42\, 44\, 47]\n\[1\] = 10 @ \[49\]\n\} @ \[49\]
37-
do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[50]\n\[1\] = 10 @ \[49\]\n\} @ \[50\]
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_pipe_count \(\) -> 0u @ \[13\]
16+
__CPROVER_rounding_mode \(\) -> 0 @ \[14\]
17+
__CPROVER_thread_id \(\) -> 0ul @ \[15\]
18+
__CPROVER_threads_exited \(\) -> TOP @ \[18\]
19+
do_arrays::1::bool_ \(\) -> TOP @ \[20\]
20+
do_arrays::1::bool_1 \(\) -> TOP @ \[21\]
21+
do_arrays::1::bool_2 \(\) -> TOP @ \[22\]
22+
do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[24\]\n\} @ \[24\]
23+
do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[24\]\n\[1\] = 20 @ \[25\]\n\} @ \[25\]
24+
do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[26\]\n\[1\] = 20 @ \[25\]\n\} @ \[26\]
25+
do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[26\]\n\[1\] = 40 @ \[27\]\n\} @ \[27\]
26+
do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[26\]\n\[1\] = 30 @ \[28\]\n\} @ \[28\]
27+
do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[29\]\n\[1\] = 30 @ \[28\]\n\} @ \[29\]
28+
do_arrays::1::x \(\) -> \{\[0\] = 5 @ \[30\]\n\[1\] = 30 @ \[28\]\n\} @ \[30\]
29+
do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[31\]\n\[1\] = 30 @ \[28\]\n\} @ \[31\]
30+
do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[31\]\n\[1\] = 10 @ \[32\]\n\} @ \[32\]
31+
do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[34\]\n\[1\] = 10 @ \[32\]\n\} @ \[34\]
32+
do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[34\, 36\]\n\[1\] = 10 @ \[32\]\n\} @ \[34\, 36\]
33+
do_arrays::1::x \(\) -> \{\[0\] = 0 @ \[38]\n\[1\] = 10 @ \[32\]\n\} @ \[38\]
34+
do_arrays::1::x \(\) -> \{\[0\] = 3 @ \[40]\n\[1\] = 10 @ \[32\]\n\} @ \[40\]
35+
do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[40\, 42]\n\[1\] = 10 @ \[32\]\n\} @ \[40\, 42\]
36+
do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[40\, 42\, 45]\n\[1\] = 10 @ \[47\]\n\} @ \[47\]
37+
do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[48]\n\[1\] = 10 @ \[47\]\n\} @ \[48\]

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

Lines changed: 26 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -8,29 +8,29 @@ 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 @ \[9\]
12-
__CPROVER_memory_leak \(\) -> TOP @ \[11\]
13-
__CPROVER_new_object \(\) -> TOP @ \[12\]
14-
__CPROVER_next_thread_key \(\) -> 0ul @ \[14\]
15-
__CPROVER_pipe_count \(\) -> 0u @ \[15\]
16-
__CPROVER_rounding_mode \(\) -> 0 @ \[16\]
17-
__CPROVER_thread_id \(\) -> 0ul @ \[17\]
18-
__CPROVER_threads_exited \(\) -> TOP @ \[20\]
19-
do_pointers::1::bool_ \(\) -> TOP @ \[22\]
20-
do_pointers::1::bool_1 \(\) -> TOP @ \[23\]
21-
do_pointers::1::bool_2 \(\) -> TOP @ \[24\]
22-
do_pointers::1::x \(\) -> TOP @ \[25\]
23-
do_pointers::1::x \(\) -> 10 @ \[26\]
24-
do_pointers::1::x_p \(\) -> TOP @ \[27\]
25-
do_pointers::1::y \(\) -> TOP @ \[28\]
26-
do_pointers::1::y \(\) -> 20 @ \[29\]
27-
do_pointers::1::y_p \(\) -> TOP @ \[30\]
28-
do_pointers::1::x_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[31\]
29-
do_pointers::1::x \(\) -> 30 @ \[32\]
30-
do_pointers::1::x \(\) -> 40 @ \[33\]
31-
do_pointers::1::x \(\) -> TOP @ \[34\]
32-
do_pointers::1::x \(\) -> 50 @ \[35\]
33-
do_pointers::1::y_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[36\]
34-
do_pointers::1::x \(\) -> 60 @ \[37\]
35-
do_pointers::1::j \(\) -> TOP @ \[38\]
36-
do_pointers::1::j \(\) -> 60 @ \[39\]
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_pipe_count \(\) -> 0u @ \[13\]
16+
__CPROVER_rounding_mode \(\) -> 0 @ \[14\]
17+
__CPROVER_thread_id \(\) -> 0ul @ \[15\]
18+
__CPROVER_threads_exited \(\) -> TOP @ \[18\]
19+
do_pointers::1::bool_ \(\) -> TOP @ \[20\]
20+
do_pointers::1::bool_1 \(\) -> TOP @ \[21\]
21+
do_pointers::1::bool_2 \(\) -> TOP @ \[22\]
22+
do_pointers::1::x \(\) -> TOP @ \[23\]
23+
do_pointers::1::x \(\) -> 10 @ \[24\]
24+
do_pointers::1::x_p \(\) -> TOP @ \[25\]
25+
do_pointers::1::y \(\) -> TOP @ \[26\]
26+
do_pointers::1::y \(\) -> 20 @ \[27\]
27+
do_pointers::1::y_p \(\) -> TOP @ \[28\]
28+
do_pointers::1::x_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[29\]
29+
do_pointers::1::x \(\) -> 30 @ \[30\]
30+
do_pointers::1::x \(\) -> 40 @ \[31\]
31+
do_pointers::1::x \(\) -> TOP @ \[32\]
32+
do_pointers::1::x \(\) -> 50 @ \[33\]
33+
do_pointers::1::y_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[34\]
34+
do_pointers::1::x \(\) -> 60 @ \[35\]
35+
do_pointers::1::j \(\) -> TOP @ \[36\]
36+
do_pointers::1::j \(\) -> 60 @ \[37\]

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

Lines changed: 31 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -8,35 +8,35 @@ 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 @ \[9\]
12-
__CPROVER_memory_leak \(\) -> TOP @ \[11\]
13-
__CPROVER_new_object \(\) -> TOP @ \[12\]
14-
__CPROVER_next_thread_key \(\) -> 0ul @ \[14\]
15-
__CPROVER_pipe_count \(\) -> 0u @ \[15\]
16-
__CPROVER_rounding_mode \(\) -> 0 @ \[16\]
17-
__CPROVER_thread_id \(\) -> 0ul @ \[17\]
18-
__CPROVER_threads_exited \(\) -> TOP @ \[20\]
19-
do_structs::1::bool_ \(\) -> TOP @ \[22\]
20-
do_structs::1::bool_1 \(\) -> TOP @ \[23\]
21-
do_structs::1::bool_2 \(\) -> TOP @ \[24\]
22-
do_structs::1::st \(\) -> \{\} @ \[25\]
23-
do_structs::1::st \(\) -> \{.x=10 @ \[26\]\} @ \[26\]
24-
do_structs::1::st \(\) -> \{.x=10 @ \[26\]\, .y=20 @ \[27\]\} @ \[27\]
25-
do_structs::1::st \(\) -> \{.x=30 @ \[28\]\, .y=20 @ \[27\]\} @ \[28\]
26-
do_structs::1::st \(\) -> \{.x=30 @ \[28\]\, .y=40 @ \[29\]\} @ \[29\]
27-
do_structs::1::st \(\) -> \{.x=30 @ \[28\]\, .y=30 @ \[30\]\} @ \[30\]
28-
do_structs::1::st \(\) -> \{.x=30 @ \[31\]\, .y=30 @ \[30\]\} @ \[31\]
29-
do_structs::1::st \(\) -> \{.x=5 @ \[32\]\, .y=30 @ \[30\]\} @ \[32\]
30-
do_structs::1::st \(\) -> \{.x=15 @ \[33\]\, .y=30 @ \[30\]\} @ \[33\]
31-
do_structs::1::st \(\) -> \{.x=15 @ \[33\]\, .y=10 @ \[34\]\} @ \[34\]
32-
do_structs::1::st \(\) -> \{.x=20 @ \[36\]\, .y=10 @ \[34\]\} @ \[36\]
33-
do_structs::1::st \(\) -> \{.x=20 @ \[36\, 38\]\, .y=10 @ \[34\]\} @ \[36\, 38\]
34-
do_structs::1::st \(\) -> \{.x=0 @ \[40\]\, .y=10 @ \[34\]\} @ \[40\]
35-
do_structs::1::st \(\) -> \{.x=3 @ \[42\]\, .y=10 @ \[34\]\} @ \[42\]
36-
do_structs::1::st \(\) -> \{.x=TOP @ \[42\, 44\]\, .y=10 @ \[34\]\} @ \[42\, 44\]
37-
do_structs::1::st \(\) -> \{.x=TOP @ \[42\, 44\, 47\]\, .y=10 @ \[34\]\} @ \[42\, 44\, 47\]
38-
do_structs::1::st \(\) -> \{.x=TOP @ \[42\, 44\, 47\]\, .y=10 @ \[49\]\} @ \[49\]
39-
do_structs::1::st \(\) -> \{.x=20 @ \[50\]\, .y=10 @ \[49\]\} @ \[50\]
40-
do_structs::1::new_age \(\) -> \{\} @ \[51\]
41-
do_structs::1::new_age \(\) -> \{.x=20 @ \[52\]\, .y=10 @ \[52\]\} @ \[52\]
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_pipe_count \(\) -> 0u @ \[13\]
16+
__CPROVER_rounding_mode \(\) -> 0 @ \[14\]
17+
__CPROVER_thread_id \(\) -> 0ul @ \[15\]
18+
__CPROVER_threads_exited \(\) -> TOP @ \[18\]
19+
do_structs::1::bool_ \(\) -> TOP @ \[20\]
20+
do_structs::1::bool_1 \(\) -> TOP @ \[21\]
21+
do_structs::1::bool_2 \(\) -> TOP @ \[22\]
22+
do_structs::1::st \(\) -> \{\} @ \[23\]
23+
do_structs::1::st \(\) -> \{.x=10 @ \[24\]\} @ \[24\]
24+
do_structs::1::st \(\) -> \{.x=10 @ \[24\]\, .y=20 @ \[25\]\} @ \[25\]
25+
do_structs::1::st \(\) -> \{.x=30 @ \[26\]\, .y=20 @ \[25\]\} @ \[26\]
26+
do_structs::1::st \(\) -> \{.x=30 @ \[26\]\, .y=40 @ \[27\]\} @ \[27\]
27+
do_structs::1::st \(\) -> \{.x=30 @ \[26\]\, .y=30 @ \[28\]\} @ \[28\]
28+
do_structs::1::st \(\) -> \{.x=30 @ \[29\]\, .y=30 @ \[28\]\} @ \[29\]
29+
do_structs::1::st \(\) -> \{.x=5 @ \[30\]\, .y=30 @ \[28\]\} @ \[30\]
30+
do_structs::1::st \(\) -> \{.x=15 @ \[31\]\, .y=30 @ \[28\]\} @ \[31\]
31+
do_structs::1::st \(\) -> \{.x=15 @ \[31\]\, .y=10 @ \[32\]\} @ \[32\]
32+
do_structs::1::st \(\) -> \{.x=20 @ \[34\]\, .y=10 @ \[32\]\} @ \[34\]
33+
do_structs::1::st \(\) -> \{.x=20 @ \[34\, 36\]\, .y=10 @ \[32\]\} @ \[34\, 36\]
34+
do_structs::1::st \(\) -> \{.x=0 @ \[38\]\, .y=10 @ \[32\]\} @ \[38\]
35+
do_structs::1::st \(\) -> \{.x=3 @ \[40\]\, .y=10 @ \[32\]\} @ \[40\]
36+
do_structs::1::st \(\) -> \{.x=TOP @ \[40\, 42\]\, .y=10 @ \[32\]\} @ \[40\, 42\]
37+
do_structs::1::st \(\) -> \{.x=TOP @ \[40\, 42\, 45\]\, .y=10 @ \[32\]\} @ \[40\, 42\, 45\]
38+
do_structs::1::st \(\) -> \{.x=TOP @ \[40\, 42\, 45\]\, .y=10 @ \[47\]\} @ \[47\]
39+
do_structs::1::st \(\) -> \{.x=20 @ \[48\]\, .y=10 @ \[47\]\} @ \[48\]
40+
do_structs::1::new_age \(\) -> \{\} @ \[49\]
41+
do_structs::1::new_age \(\) -> \{.x=20 @ \[50\]\, .y=10 @ \[50\]\} @ \[50\]
4242
--

0 commit comments

Comments
 (0)