Merge pull request #8363 from tautschnig/temporaries-minimal-scope

tautschnig · web-flow · commit 320843888c17 · 2024-07-22T12:22:07.000+02:00
GOTO conversion: create temporaries with minimal scope
diff --git a/regression/cbmc-cover/location14/test.desc b/regression/cbmc-cover/location14/test.desc
@@ -6,8 +6,9 @@ main.c
 ^\[main.coverage.1\] file main.c line 8 function main block 1.*: SATISFIED$
 ^\[main.coverage.2\] file main.c line 12 function main block 2.*: FAILED$
 ^\[main.coverage.3\] file main.c line 12 function main block 3.*: FAILED$
-^\[main.coverage.4\] file main.c line 13 function main block 4.*: SATISFIED$
+^\[main.coverage.4\] file main.c line 12 function main block 4.*: FAILED$
+^\[main.coverage.5\] file main.c line 13 function main block 5.*: SATISFIED$
 ^\[foo.coverage.1\] file main.c line 3 function foo block 1.*: FAILED$
-^\*\* 2 of 5 covered \(40.0%\)
+^\*\* 2 of 6 covered \(33.3%\)
 --
 ^warning: ignoring
diff --git a/regression/contracts/loop_contracts_do_while/test.desc b/regression/contracts/loop_contracts_do_while/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --apply-loop-contracts
 ^EXIT=0$
@@ -7,4 +7,3 @@ main.c
 --
 --
 This test checks that loop contracts work correctly on do/while loops.
-Fails because contracts are not yet supported on do while loops.
diff --git a/regression/cprover/safety/use_after_free1.desc b/regression/cprover/safety/use_after_free1.desc
@@ -4,5 +4,5 @@ use_after_free1.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^\(\d+\) ∀ ς : state . S11\(ς\) ⇒ S12\(ς\[❝main::\$tmp::return_value_malloc❞:=allocate\(ς, 4\)\]\)$
-^\(\d+\) ∀ ς : state . S15\(ς\) ⇒ S16\(deallocate_state\(ς, cast\(ς\(❝main::1::p❞\), empty\*\)\)\)$
+^\(\d+\) ∀ ς : state . S16\(ς\) ⇒ S17\(deallocate_state\(ς, cast\(ς\(❝main::1::p❞\), empty\*\)\)\)$
 --
diff --git a/regression/goto-analyzer/branching-ge/test-always-constants.desc b/regression/goto-analyzer/branching-ge/test-always-constants.desc
@@ -3,6 +3,6 @@ main-always.c
 --no-standard-checks --variable-sensitivity --vsd-values constants --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* TOP @ \[17, 19\]
-^main::1::p .* TOP @ \[3, 8, 14\]
+^main::1::i .* TOP @ \[23, 25\]
+^main::1::p .* TOP @ \[3, 9, 18\]
 --
diff --git a/regression/goto-analyzer/branching-ge/test-always-intervals.desc b/regression/goto-analyzer/branching-ge/test-always-intervals.desc
@@ -3,6 +3,6 @@ main-always.c
 --no-standard-checks --variable-sensitivity --vsd-values intervals --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* \[5, 5\] @ \[17\]
-^main::1::p .* \[0, A\] @ \[3, 8, 14\]
+^main::1::i .* \[5, 5\] @ \[23\]
+^main::1::p .* \[0, A\] @ \[3, 9, 18\]
 --
diff --git a/regression/goto-analyzer/branching-ge/test-always-value-set.desc b/regression/goto-analyzer/branching-ge/test-always-value-set.desc
@@ -3,6 +3,6 @@ main-always.c
 --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* value-set-begin: 5 :value-set-end @ \[17\]
-^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 8, 14\]
+^main::1::i .* value-set-begin: 5 :value-set-end @ \[23\]
+^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\]
 --
diff --git a/regression/goto-analyzer/branching-ge/test-indeterminate-constants.desc b/regression/goto-analyzer/branching-ge/test-indeterminate-constants.desc
@@ -3,6 +3,6 @@ main-indeterminate.c
 --no-standard-checks --variable-sensitivity --vsd-values constants --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* TOP @ \[17, 19\]
-^main::1::p .* TOP @ \[3, 8, 14\]
+^main::1::i .* TOP @ \[23, 25\]
+^main::1::p .* TOP @ \[3, 9, 18\]
 --
diff --git a/regression/goto-analyzer/branching-ge/test-indeterminate-intervals.desc b/regression/goto-analyzer/branching-ge/test-indeterminate-intervals.desc
@@ -3,6 +3,6 @@ main-indeterminate.c
 --no-standard-checks --variable-sensitivity --vsd-values intervals --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* \[FFFFFFFB, 5\] @ \[17, 19\]
-^main::1::p .* \[0, A\] @ \[3, 8, 14\]
+^main::1::i .* \[FFFFFFFB, 5\] @ \[23, 25\]
+^main::1::p .* \[0, A\] @ \[3, 9, 18\]
 --
diff --git a/regression/goto-analyzer/branching-ge/test-indeterminate-value-set.desc b/regression/goto-analyzer/branching-ge/test-indeterminate-value-set.desc
@@ -3,6 +3,6 @@ main-indeterminate.c
 --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* value-set-begin: 5, -5 :value-set-end @ \[17, 19\]
-^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 8, 14\]
+^main::1::i .* value-set-begin: 5, -5 :value-set-end @ \[23, 25\]
+^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\]
 --
diff --git a/regression/goto-analyzer/branching-ge/test-never-constants.desc b/regression/goto-analyzer/branching-ge/test-never-constants.desc
@@ -3,6 +3,6 @@ main-never.c
 --no-standard-checks --variable-sensitivity --vsd-values constants --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* TOP @ \[17, 19\]
-^main::1::p .* TOP @ \[3, 8, 14\]
+^main::1::i .* TOP @ \[23, 25\]
+^main::1::p .* TOP @ \[3, 9, 18\]
 --
diff --git a/regression/goto-analyzer/branching-ge/test-never-intervals.desc b/regression/goto-analyzer/branching-ge/test-never-intervals.desc
@@ -3,6 +3,6 @@ main-never.c
 --no-standard-checks --variable-sensitivity --vsd-values intervals --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* \[FFFFFFFB, FFFFFFFB\] @ \[19\]
-^main::1::p .* \[0, A\] @ \[3, 8, 14\]
+^main::1::i .* \[FFFFFFFB, FFFFFFFB\] @ \[25\]
+^main::1::p .* \[0, A\] @ \[3, 9, 18\]
 --
diff --git a/regression/goto-analyzer/branching-ge/test-never-value-set.desc b/regression/goto-analyzer/branching-ge/test-never-value-set.desc
@@ -3,6 +3,6 @@ main-never.c
 --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* value-set-begin: -5 :value-set-end @ \[19\]
-^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 8, 14\]
+^main::1::i .* value-set-begin: -5 :value-set-end @ \[25\]
+^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\]
 --
diff --git a/regression/goto-analyzer/branching-gt/test-always-constants.desc b/regression/goto-analyzer/branching-gt/test-always-constants.desc
@@ -3,6 +3,6 @@ main-always.c
 --no-standard-checks --variable-sensitivity --vsd-values constants --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* TOP @ \[17, 19\]
-^main::1::p .* TOP @ \[3, 8, 14\]
+^main::1::i .* TOP @ \[23, 25\]
+^main::1::p .* TOP @ \[3, 9, 18\]
 --
diff --git a/regression/goto-analyzer/branching-gt/test-always-intervals.desc b/regression/goto-analyzer/branching-gt/test-always-intervals.desc
@@ -3,6 +3,6 @@ main-always.c
 --no-standard-checks --variable-sensitivity --vsd-values intervals --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* \[5, 5\] @ \[17\]
-^main::1::p .* \[0, A\] @ \[3, 8, 14\]
+^main::1::i .* \[5, 5\] @ \[23\]
+^main::1::p .* \[0, A\] @ \[3, 9, 18\]
 --
diff --git a/regression/goto-analyzer/branching-gt/test-always-value-set.desc b/regression/goto-analyzer/branching-gt/test-always-value-set.desc
@@ -3,6 +3,6 @@ main-always.c
 --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* value-set-begin: 5 :value-set-end @ \[17\]
-^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 8, 14\]
+^main::1::i .* value-set-begin: 5 :value-set-end @ \[23\]
+^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\]
 --
diff --git a/regression/goto-analyzer/branching-gt/test-indeterminate-constants.desc b/regression/goto-analyzer/branching-gt/test-indeterminate-constants.desc
@@ -3,6 +3,6 @@ main-indeterminate.c
 --no-standard-checks --variable-sensitivity --vsd-values constants --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* TOP @ \[17, 19\]
-^main::1::p .* TOP @ \[3, 8, 14\]
+^main::1::i .* TOP @ \[23, 25\]
+^main::1::p .* TOP @ \[3, 9, 18\]
 --
diff --git a/regression/goto-analyzer/branching-gt/test-indeterminate-intervals.desc b/regression/goto-analyzer/branching-gt/test-indeterminate-intervals.desc
@@ -3,6 +3,6 @@ main-indeterminate.c
 --no-standard-checks --variable-sensitivity --vsd-values intervals --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* \[FFFFFFFB, 5\] @ \[17, 19\]
-^main::1::p .* \[0, A\] @ \[3, 8, 14\]
+^main::1::i .* \[FFFFFFFB, 5\] @ \[23, 25\]
+^main::1::p .* \[0, A\] @ \[3, 9, 18\]
 --
diff --git a/regression/goto-analyzer/branching-gt/test-indeterminate-value-set.desc b/regression/goto-analyzer/branching-gt/test-indeterminate-value-set.desc
@@ -3,6 +3,6 @@ main-indeterminate.c
 --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* value-set-begin: 5, -5 :value-set-end @ \[17, 19\]
-^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 8, 14\]
+^main::1::i .* value-set-begin: 5, -5 :value-set-end @ \[23, 25\]
+^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\]
 --
diff --git a/regression/goto-analyzer/branching-gt/test-never-constants.desc b/regression/goto-analyzer/branching-gt/test-never-constants.desc
@@ -3,6 +3,6 @@ main-never.c
 --no-standard-checks --variable-sensitivity --vsd-values constants --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* TOP @ \[17, 19\]
-^main::1::p .* TOP @ \[3, 8, 14\]
+^main::1::i .* TOP @ \[23, 25\]
+^main::1::p .* TOP @ \[3, 9, 18\]
 --
diff --git a/regression/goto-analyzer/branching-gt/test-never-intervals.desc b/regression/goto-analyzer/branching-gt/test-never-intervals.desc
@@ -3,6 +3,6 @@ main-never.c
 --no-standard-checks --variable-sensitivity --vsd-values intervals --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* \[FFFFFFFB, FFFFFFFB\] @ \[19\]
-^main::1::p .* \[0, A\] @ \[3, 8, 14\]
+^main::1::i .* \[FFFFFFFB, FFFFFFFB\] @ \[25\]
+^main::1::p .* \[0, A\] @ \[3, 9, 18\]
 --
diff --git a/regression/goto-analyzer/branching-gt/test-never-value-set.desc b/regression/goto-analyzer/branching-gt/test-never-value-set.desc
@@ -3,6 +3,6 @@ main-never.c
 --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* value-set-begin: -5 :value-set-end @ \[19\]
-^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 8, 14\]
+^main::1::i .* value-set-begin: -5 :value-set-end @ \[25\]
+^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\]
 --
diff --git a/regression/goto-analyzer/branching-le/test-always-constants.desc b/regression/goto-analyzer/branching-le/test-always-constants.desc
@@ -3,6 +3,6 @@ main-always.c
 --no-standard-checks --variable-sensitivity --vsd-values constants --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* TOP @ \[17, 19\]
-^main::1::p .* TOP @ \[3, 8, 14\]
+^main::1::i .* TOP @ \[23, 25\]
+^main::1::p .* TOP @ \[3, 9, 18\]
 --
diff --git a/regression/goto-analyzer/branching-le/test-always-intervals.desc b/regression/goto-analyzer/branching-le/test-always-intervals.desc
@@ -3,6 +3,6 @@ main-always.c
 --no-standard-checks --variable-sensitivity --vsd-values intervals --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* \[5, 5\] @ \[17\]
-^main::1::p .* \[0, A\] @ \[3, 8, 14\]
+^main::1::i .* \[5, 5\] @ \[23\]
+^main::1::p .* \[0, A\] @ \[3, 9, 18\]
 --
diff --git a/regression/goto-analyzer/branching-le/test-always-value-set.desc b/regression/goto-analyzer/branching-le/test-always-value-set.desc
@@ -3,6 +3,6 @@ main-always.c
 --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* value-set-begin: 5 :value-set-end @ \[17\]
-^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 8, 14\]
+^main::1::i .* value-set-begin: 5 :value-set-end @ \[23\]
+^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\]
 --
diff --git a/regression/goto-analyzer/branching-le/test-indeterminate-constants.desc b/regression/goto-analyzer/branching-le/test-indeterminate-constants.desc
@@ -3,6 +3,6 @@ main-indeterminate.c
 --no-standard-checks --variable-sensitivity --vsd-values constants --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* TOP @ \[17, 19\]
-^main::1::p .* TOP @ \[3, 8, 14\]
+^main::1::i .* TOP @ \[23, 25\]
+^main::1::p .* TOP @ \[3, 9, 18\]
 --
diff --git a/regression/goto-analyzer/branching-le/test-indeterminate-intervals.desc b/regression/goto-analyzer/branching-le/test-indeterminate-intervals.desc
@@ -3,6 +3,6 @@ main-indeterminate.c
 --no-standard-checks --variable-sensitivity --vsd-values intervals --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* \[FFFFFFFB, 5\] @ \[17, 19\]
-^main::1::p .* \[0, A\] @ \[3, 8, 14\]
+^main::1::i .* \[FFFFFFFB, 5\] @ \[23, 25\]
+^main::1::p .* \[0, A\] @ \[3, 9, 18\]
 --
diff --git a/regression/goto-analyzer/branching-le/test-indeterminate-value-set.desc b/regression/goto-analyzer/branching-le/test-indeterminate-value-set.desc
@@ -3,6 +3,6 @@ main-indeterminate.c
 --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* value-set-begin: 5, -5 :value-set-end @ \[17, 19\]
-^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 8, 14\]
+^main::1::i .* value-set-begin: 5, -5 :value-set-end @ \[23, 25\]
+^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\]
 --
diff --git a/regression/goto-analyzer/branching-le/test-never-constants.desc b/regression/goto-analyzer/branching-le/test-never-constants.desc
@@ -3,6 +3,6 @@ main-never.c
 --no-standard-checks --variable-sensitivity --vsd-values constants --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* TOP @ \[17, 19\]
-^main::1::p .* TOP @ \[3, 8, 14\]
+^main::1::i .* TOP @ \[23, 25\]
+^main::1::p .* TOP @ \[3, 9, 18\]
 --
diff --git a/regression/goto-analyzer/branching-le/test-never-intervals.desc b/regression/goto-analyzer/branching-le/test-never-intervals.desc
@@ -3,6 +3,6 @@ main-never.c
 --no-standard-checks --variable-sensitivity --vsd-values intervals --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* \[FFFFFFFB, FFFFFFFB\] @ \[19\]
-^main::1::p .* \[0, A\] @ \[3, 8, 14\]
+^main::1::i .* \[FFFFFFFB, FFFFFFFB\] @ \[25\]
+^main::1::p .* \[0, A\] @ \[3, 9, 18\]
 --
diff --git a/regression/goto-analyzer/branching-le/test-never-value-set.desc b/regression/goto-analyzer/branching-le/test-never-value-set.desc
@@ -3,6 +3,6 @@ main-never.c
 --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* value-set-begin: -5 :value-set-end @ \[19\]
-^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 8, 14\]
+^main::1::i .* value-set-begin: -5 :value-set-end @ \[25\]
+^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\]
 --
diff --git a/regression/goto-analyzer/branching-lt/test-always-constants.desc b/regression/goto-analyzer/branching-lt/test-always-constants.desc
@@ -3,6 +3,6 @@ main-always.c
 --no-standard-checks --variable-sensitivity --vsd-values constants --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* TOP @ \[17, 19\]
-^main::1::p .* TOP @ \[3, 8, 14\]
+^main::1::i .* TOP @ \[23, 25\]
+^main::1::p .* TOP @ \[3, 9, 18\]
 --
diff --git a/regression/goto-analyzer/branching-lt/test-always-intervals.desc b/regression/goto-analyzer/branching-lt/test-always-intervals.desc
@@ -3,6 +3,6 @@ main-always.c
 --no-standard-checks --variable-sensitivity --vsd-values intervals --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* \[5, 5\] @ \[17\]
-^main::1::p .* \[0, A\] @ \[3, 8, 14\]
+^main::1::i .* \[5, 5\] @ \[23\]
+^main::1::p .* \[0, A\] @ \[3, 9, 18\]
 --
diff --git a/regression/goto-analyzer/branching-lt/test-always-value-set.desc b/regression/goto-analyzer/branching-lt/test-always-value-set.desc
@@ -3,6 +3,6 @@ main-always.c
 --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* value-set-begin: 5 :value-set-end @ \[17\]
-^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 8, 14\]
+^main::1::i .* value-set-begin: 5 :value-set-end @ \[23\]
+^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\]
 --
diff --git a/regression/goto-analyzer/branching-lt/test-indeterminate-constants.desc b/regression/goto-analyzer/branching-lt/test-indeterminate-constants.desc
@@ -3,6 +3,6 @@ main-indeterminate.c
 --no-standard-checks --variable-sensitivity --vsd-values constants --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* TOP @ \[17, 19\]
-^main::1::p .* TOP @ \[3, 8, 14\]
+^main::1::i .* TOP @ \[23, 25\]
+^main::1::p .* TOP @ \[3, 9, 18\]
 --
diff --git a/regression/goto-analyzer/branching-lt/test-indeterminate-intervals.desc b/regression/goto-analyzer/branching-lt/test-indeterminate-intervals.desc
@@ -3,6 +3,6 @@ main-indeterminate.c
 --no-standard-checks --variable-sensitivity --vsd-values intervals --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* \[FFFFFFFB, 5\] @ \[17, 19\]
-^main::1::p .* \[0, A\] @ \[3, 8, 14\]
+^main::1::i .* \[FFFFFFFB, 5\] @ \[23, 25\]
+^main::1::p .* \[0, A\] @ \[3, 9, 18\]
 --
diff --git a/regression/goto-analyzer/branching-lt/test-indeterminate-value-set.desc b/regression/goto-analyzer/branching-lt/test-indeterminate-value-set.desc
@@ -3,6 +3,6 @@ main-indeterminate.c
 --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* value-set-begin: 5, -5 :value-set-end @ \[17, 19\]
-^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 8, 14\]
+^main::1::i .* value-set-begin: 5, -5 :value-set-end @ \[23, 25\]
+^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\]
 --
diff --git a/regression/goto-analyzer/branching-lt/test-never-constants.desc b/regression/goto-analyzer/branching-lt/test-never-constants.desc
@@ -3,6 +3,6 @@ main-never.c
 --no-standard-checks --variable-sensitivity --vsd-values constants --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* TOP @ \[17, 19\]
-^main::1::p .* TOP @ \[3, 8, 14\]
+^main::1::i .* TOP @ \[23, 25\]
+^main::1::p .* TOP @ \[3, 9, 18\]
 --
diff --git a/regression/goto-analyzer/branching-lt/test-never-intervals.desc b/regression/goto-analyzer/branching-lt/test-never-intervals.desc
@@ -3,6 +3,6 @@ main-never.c
 --no-standard-checks --variable-sensitivity --vsd-values intervals --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* \[FFFFFFFB, FFFFFFFB\] @ \[19\]
-^main::1::p .* \[0, A\] @ \[3, 8, 14\]
+^main::1::i .* \[FFFFFFFB, FFFFFFFB\] @ \[25\]
+^main::1::p .* \[0, A\] @ \[3, 9, 18\]
 --
diff --git a/regression/goto-analyzer/branching-lt/test-never-value-set.desc b/regression/goto-analyzer/branching-lt/test-never-value-set.desc
@@ -3,6 +3,6 @@ main-never.c
 --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show
 ^EXIT=0$
 ^SIGNAL=0$
-^main::1::i .* value-set-begin: -5 :value-set-end @ \[19\]
-^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 8, 14\]
+^main::1::i .* value-set-begin: -5 :value-set-end @ \[25\]
+^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\]
 --
diff --git a/regression/goto-instrument/ensure-one-backedge-per-target-not-lexical/with-transform.desc b/regression/goto-instrument/ensure-one-backedge-per-target-not-lexical/with-transform.desc
@@ -2,6 +2,6 @@ CORE
 main.c
 --ensure-one-backedge-per-target --show-lexical-loops
 ^3 is head of \{ 3, 4, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26 \(backedge\) \}$
-^16 is head of \{ 16, 17, 22, 23, 24, 25 \(backedge\) \}$
+^17 is head of \{ 17, 18, 22, 23, 24, 25 \(backedge\) \}$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/goto-instrument/ensure-one-backedge-per-target-not-lexical/without-transform.desc b/regression/goto-instrument/ensure-one-backedge-per-target-not-lexical/without-transform.desc
@@ -1,7 +1,7 @@
 CORE
 main.c
 --show-lexical-loops
-^16 is head of \{ 16, 17, 22, 23, 24, 25 \(backedge\) \}$
+^17 is head of \{ 17, 18, 22, 23, 24, 25 \(backedge\) \}$
 Note not all loops were in lexical loop form
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/goto-instrument/region-analysis-14/test.desc b/regression/goto-instrument/region-analysis-14/test.desc
@@ -3,6 +3,6 @@ test.c
 --show-sese-regions
 ^Function contains 2 single-entry, single-exit regions:$
 ^Region starting at \(2, [0-9]+\) .*::x := 0 ends at \(5, [0-9]+\) SKIP$
-^Region starting at \(0, [0-9]+\) IF .*5.* THEN GOTO 2 ends at \(9, [0-9]+\) 3: SKIP$
+^Region starting at \(0, [0-9]+\) IF .*5.* THEN GOTO 2 ends at \(10, [0-9]+\) 3: SKIP$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/goto-instrument/region-analysis-15/test.desc b/regression/goto-instrument/region-analysis-15/test.desc
@@ -2,7 +2,7 @@ CORE
 test.c
 --show-sese-regions
 ^Function contains 2 single-entry, single-exit regions:$
-^Region starting at \(2, [0-9]+\) .*::x := 0 ends at \(8, [0-9]+\) 2: SKIP$
-^Region starting at \(0, [0-9]+\) IF .*5.* THEN GOTO 3 ends at \(12, [0-9]+\) 4: SKIP$
+^Region starting at \(2, [0-9]+\) .*::x := 0 ends at \(9, [0-9]+\) 2: SKIP$
+^Region starting at \(0, [0-9]+\) IF .*5.* THEN GOTO 3 ends at \(13, [0-9]+\) 4: SKIP$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/goto-instrument/region-analysis-16/test.desc b/regression/goto-instrument/region-analysis-16/test.desc
@@ -3,7 +3,7 @@ test.c
 --show-sese-regions
 ^Function contains 3 single-entry, single-exit regions:$
 ^Region starting at \(3, [0-9]+\) 1: IF .*7.* THEN GOTO 2 ends at \(8, [0-9]+\) 3: IF .*::x < 10 THEN GOTO 1$
-^Region starting at \(0, [0-9]+\) IF .*5.* THEN GOTO 4 ends at \(13, [0-9]+\) 5: SKIP$
+^Region starting at \(0, [0-9]+\) IF .*5.* THEN GOTO 4 ends at \(14, [0-9]+\) 5: SKIP$
 ^Region starting at \(2, [0-9]+\) .*::x := 0 ends at \(9, [0-9]+\) SKIP$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/src/analyses/variable-sensitivity/abstract_value_object.cpp b/src/analyses/variable-sensitivity/abstract_value_object.cpp
diff --git a/src/ansi-c/goto-conversion/builtin_functions.cpp b/src/ansi-c/goto-conversion/builtin_functions.cpp
diff --git a/src/ansi-c/goto-conversion/destructor.cpp b/src/ansi-c/goto-conversion/destructor.cpp
diff --git a/src/ansi-c/goto-conversion/destructor.h b/src/ansi-c/goto-conversion/destructor.h
diff --git a/src/ansi-c/goto-conversion/goto_clean_expr.cpp b/src/ansi-c/goto-conversion/goto_clean_expr.cpp
diff --git a/src/ansi-c/goto-conversion/goto_convert.cpp b/src/ansi-c/goto-conversion/goto_convert.cpp
diff --git a/src/ansi-c/goto-conversion/goto_convert_class.h b/src/ansi-c/goto-conversion/goto_convert_class.h
diff --git a/src/ansi-c/goto-conversion/goto_convert_function_call.cpp b/src/ansi-c/goto-conversion/goto_convert_function_call.cpp
diff --git a/src/ansi-c/goto-conversion/goto_convert_side_effect.cpp b/src/ansi-c/goto-conversion/goto_convert_side_effect.cpp
diff --git a/src/cprover/simplify_state_expr.cpp b/src/cprover/simplify_state_expr.cpp
diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp
diff --git a/src/goto-instrument/contracts/instrument_spec_assigns.cpp b/src/goto-instrument/contracts/instrument_spec_assigns.cpp
diff --git a/src/goto-instrument/contracts/utils.h b/src/goto-instrument/contracts/utils.h
