diff --git a/regression/cbmc-cover/location14/test.desc b/regression/cbmc-cover/location14/test.desc index 7c95cd977c4..f2ffb5c4d1e 100644 --- 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 index b48cda7c0d9..9c52a782fea 100644 --- 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 index a2f4b160356..e6cd066a3cd 100644 --- 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 index fe7cc203863..73167c183a9 100644 --- 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 index 9a781120569..e35fdffedda 100644 --- 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 index 656e57f9b4d..6fa9bae0c29 100644 --- 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 index 796fb44c24f..c23c3655f5f 100644 --- 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 index 1cd97258e06..5313cd50951 100644 --- 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 index a6dc611327e..406cd930231 100644 --- 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 index c0648a45058..2d1d6df13a0 100644 --- 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 index 3918aa7b40f..9c31600de4f 100644 --- 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 index 281a3a3aedb..f8f2a0aa278 100644 --- 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 index fe7cc203863..73167c183a9 100644 --- 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 index 9a781120569..e35fdffedda 100644 --- 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 index 656e57f9b4d..6fa9bae0c29 100644 --- 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 index 796fb44c24f..c23c3655f5f 100644 --- 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 index 1cd97258e06..5313cd50951 100644 --- 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 index a6dc611327e..406cd930231 100644 --- 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 index c0648a45058..2d1d6df13a0 100644 --- 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 index 3918aa7b40f..9c31600de4f 100644 --- 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 index 281a3a3aedb..f8f2a0aa278 100644 --- 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 index fe7cc203863..73167c183a9 100644 --- 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 index 9a781120569..e35fdffedda 100644 --- 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 index 656e57f9b4d..6fa9bae0c29 100644 --- 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 index 796fb44c24f..c23c3655f5f 100644 --- 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 index 1cd97258e06..5313cd50951 100644 --- 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 index a6dc611327e..406cd930231 100644 --- 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 index c0648a45058..2d1d6df13a0 100644 --- 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 index 3918aa7b40f..9c31600de4f 100644 --- 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 index 281a3a3aedb..f8f2a0aa278 100644 --- 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 index fe7cc203863..73167c183a9 100644 --- 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 index 9a781120569..e35fdffedda 100644 --- 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 index 656e57f9b4d..6fa9bae0c29 100644 --- 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 index 796fb44c24f..c23c3655f5f 100644 --- 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 index 1cd97258e06..5313cd50951 100644 --- 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 index a6dc611327e..406cd930231 100644 --- 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 index c0648a45058..2d1d6df13a0 100644 --- 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 index 3918aa7b40f..9c31600de4f 100644 --- 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 index 281a3a3aedb..f8f2a0aa278 100644 --- 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 index cce4bb55b58..4df83b91759 100644 --- 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 index 6a808e9a0e2..3c75bba4947 100644 --- 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 index ff87ce2a2e6..a689de8ff78 100644 --- 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 index 910291e08be..214c3e45004 100644 --- 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 index 92d06f8055b..0ab1668f9bc 100644 --- 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 index aa4c94c21c9..2b339a3f5f3 100644 --- a/src/analyses/variable-sensitivity/abstract_value_object.cpp +++ b/src/analyses/variable-sensitivity/abstract_value_object.cpp @@ -438,7 +438,7 @@ class interval_evaluator } INVARIANT( - result.type() == expression.type(), + result.is_top() || result.type() == expression.type(), "Type of result interval should match expression type"); return make_interval(result); } diff --git a/src/ansi-c/goto-conversion/builtin_functions.cpp b/src/ansi-c/goto-conversion/builtin_functions.cpp index dc944e3d964..bf864fcdb1e 100644 --- a/src/ansi-c/goto-conversion/builtin_functions.cpp +++ b/src/ansi-c/goto-conversion/builtin_functions.cpp @@ -27,6 +27,7 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include "destructor.h" #include "format_strings.h" void goto_convertt::do_prob_uniform( @@ -400,6 +401,7 @@ void goto_convertt::do_cpp_new( bool new_array = rhs.get(ID_statement) == ID_cpp_new_array; exprt count; + clean_expr_resultt side_effects; if(new_array) { @@ -407,7 +409,8 @@ void goto_convertt::do_cpp_new( static_cast(rhs.find(ID_size)), object_size.type()); // might have side-effect - clean_expr(count, dest, ID_cpp); + side_effects.add(clean_expr(count, ID_cpp)); + dest.destructive_append(side_effects.side_effects); } exprt tmp_symbol_expr; @@ -493,6 +496,9 @@ void goto_convertt::do_cpp_new( typecast_exprt(tmp_symbol_expr, lhs.type()), rhs.find_source_location())); + side_effects.add_temporary(to_symbol_expr(tmp_symbol_expr).get_identifier()); + destruct_locals(side_effects.temporaries, dest, ns); + // grab initializer goto_programt tmp_initializer; cpp_new_initializer(lhs, rhs, tmp_initializer); @@ -685,6 +691,8 @@ void goto_convertt::do_havoc_slice( codet array_replace(ID_array_replace, {arg0, arg1}, source_location); dest.add(goto_programt::make_other(array_replace, source_location)); + + destruct_locals({nondet_contents.name}, dest, ns); } /// alloca allocates memory that is freed when leaving the function (and not the @@ -773,6 +781,9 @@ void goto_convertt::do_alloca( dest.add(goto_programt::make_assignment( this_alloca_ptr, std::move(rhs), source_location)); + if(lhs.is_nil()) + destruct_locals({to_symbol_expr(new_lhs).get_identifier()}, dest, ns); + // mark pointer to alloca result as dead, unless the alloca result (in // this_alloca_ptr) is still NULL symbol_exprt dead_object_sym = diff --git a/src/ansi-c/goto-conversion/destructor.cpp b/src/ansi-c/goto-conversion/destructor.cpp index e8ce48211c0..330b11003c2 100644 --- a/src/ansi-c/goto-conversion/destructor.cpp +++ b/src/ansi-c/goto-conversion/destructor.cpp @@ -11,10 +11,12 @@ Author: Daniel Kroening, kroening@kroening.com #include "destructor.h" +#include #include #include +#include -#include +#include code_function_callt get_destructor(const namespacet &ns, const typet &type) { @@ -56,3 +58,33 @@ code_function_callt get_destructor(const namespacet &ns, const typet &type) return static_cast(get_nil_irep()); } + +void destruct_locals( + const std::list &vars, + goto_programt &dest, + const namespacet &ns) +{ + for(const auto &id : vars) + { + const symbolt &symbol = ns.lookup(id); + + // do destructor + code_function_callt destructor = get_destructor(ns, symbol.type); + + if(destructor.is_not_nil()) + { + // add "this" + address_of_exprt this_expr( + symbol.symbol_expr(), pointer_type(symbol.type)); + destructor.arguments().push_back(this_expr); + + dest.add(goto_programt::make_function_call( + destructor, destructor.source_location())); + } + + // now create a 'dead' instruction -- will be added after the + // destructor created below as unwind_destructor_stack pops off the + // top of the destructor stack + dest.add(goto_programt::make_dead(symbol.symbol_expr(), symbol.location)); + } +} diff --git a/src/ansi-c/goto-conversion/destructor.h b/src/ansi-c/goto-conversion/destructor.h index 7cfbb594a61..d362135e7d0 100644 --- a/src/ansi-c/goto-conversion/destructor.h +++ b/src/ansi-c/goto-conversion/destructor.h @@ -12,10 +12,20 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_GOTO_PROGRAMS_DESTRUCTOR_H #define CPROVER_GOTO_PROGRAMS_DESTRUCTOR_H +#include + +#include + +class goto_programt; class namespacet; class typet; class code_function_callt get_destructor(const namespacet &ns, const typet &type); +void destruct_locals( + const std::list &vars, + goto_programt &dest, + const namespacet &ns); + #endif // CPROVER_GOTO_PROGRAMS_DESTRUCTOR_H diff --git a/src/ansi-c/goto-conversion/goto_clean_expr.cpp b/src/ansi-c/goto-conversion/goto_clean_expr.cpp index f8de1cff1ed..c015c1fe414 100644 --- a/src/ansi-c/goto-conversion/goto_clean_expr.cpp +++ b/src/ansi-c/goto-conversion/goto_clean_expr.cpp @@ -17,6 +17,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include "destructor.h" + symbol_exprt goto_convertt::make_compound_literal( const exprt &expr, goto_programt &dest, @@ -164,9 +166,8 @@ void goto_convertt::rewrite_boolean(exprt &expr) expr.swap(tmp); } -void goto_convertt::clean_expr( +goto_convertt::clean_expr_resultt goto_convertt::clean_expr( exprt &expr, - goto_programt &dest, const irep_idt &mode, bool result_is_used) { @@ -179,7 +180,7 @@ void goto_convertt::clean_expr( // compound literals if(!needs_cleaning(expr)) - return; + return {}; if(expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_implies) { @@ -187,19 +188,21 @@ void goto_convertt::clean_expr( rewrite_boolean(expr); // recursive call - clean_expr(expr, dest, mode, result_is_used); - return; + return clean_expr(expr, mode, result_is_used); } else if(expr.id() == ID_if) { // first clean condition - clean_expr(to_if_expr(expr).cond(), dest, mode, true); + clean_expr_resultt side_effects = + clean_expr(to_if_expr(expr).cond(), mode, true); // possibly done now if( !needs_cleaning(to_if_expr(expr).true_case()) && !needs_cleaning(to_if_expr(expr).false_case())) - return; + { + return side_effects; + } // copy expression if_exprt if_expr = to_if_expr(expr); @@ -232,28 +235,32 @@ void goto_convertt::clean_expr( } #endif - goto_programt tmp_true; - clean_expr(if_expr.true_case(), tmp_true, mode, result_is_used); + clean_expr_resultt tmp_true( + clean_expr(if_expr.true_case(), mode, result_is_used)); - goto_programt tmp_false; - clean_expr(if_expr.false_case(), tmp_false, mode, result_is_used); + clean_expr_resultt tmp_false( + clean_expr(if_expr.false_case(), mode, result_is_used)); if(result_is_used) { - symbolt &new_symbol = - new_tmp_symbol(expr.type(), "if_expr", dest, source_location, mode); + symbolt &new_symbol = new_tmp_symbol( + expr.type(), + "if_expr", + side_effects.side_effects, + source_location, + mode); code_assignt assignment_true; assignment_true.lhs() = new_symbol.symbol_expr(); assignment_true.rhs() = if_expr.true_case(); assignment_true.add_source_location() = source_location; - convert(assignment_true, tmp_true, mode); + convert(assignment_true, tmp_true.side_effects, mode); code_assignt assignment_false; assignment_false.lhs() = new_symbol.symbol_expr(); assignment_false.rhs() = if_expr.false_case(); assignment_false.add_source_location() = source_location; - convert(assignment_false, tmp_false, mode); + convert(assignment_false, tmp_false.side_effects, mode); // overwrites expr expr = new_symbol.symbol_expr(); @@ -267,7 +274,7 @@ void goto_convertt::clean_expr( // expression is just a constant code_expressiont code_expression( typecast_exprt(if_expr.true_case(), empty_typet())); - convert(code_expression, tmp_true, mode); + convert(code_expression, tmp_true.side_effects, mode); } if(if_expr.false_case().is_not_nil()) @@ -276,7 +283,7 @@ void goto_convertt::clean_expr( // expression is just a constant code_expressiont code_expression( typecast_exprt(if_expr.false_case(), empty_typet())); - convert(code_expression, tmp_false, mode); + convert(code_expression, tmp_false.side_effects, mode); } expr = nil_exprt(); @@ -286,17 +293,27 @@ void goto_convertt::clean_expr( generate_ifthenelse( if_expr.cond(), source_location, - tmp_true, + tmp_true.side_effects, if_expr.true_case().source_location(), - tmp_false, + tmp_false.side_effects, if_expr.false_case().source_location(), - dest, + side_effects.side_effects, mode); - return; + destruct_locals(tmp_false.temporaries, side_effects.side_effects, ns); + destruct_locals(tmp_true.temporaries, side_effects.side_effects, ns); + destruct_locals(side_effects.temporaries, side_effects.side_effects, ns); + side_effects.temporaries.clear(); + + if(expr.is_not_nil()) + side_effects.add_temporary(to_symbol_expr(expr).get_identifier()); + + return side_effects; } else if(expr.id() == ID_comma) { + clean_expr_resultt side_effects; + if(result_is_used) { exprt result; @@ -309,15 +326,15 @@ void goto_convertt::clean_expr( if(last) { result.swap(*it); - clean_expr(result, dest, mode, true); + side_effects.add(clean_expr(result, mode, true)); } else { - clean_expr(*it, dest, mode, false); + side_effects.add(clean_expr(*it, mode, false)); // remember these for later checks if(it->is_not_nil()) - convert(code_expressiont(*it), dest, mode); + convert(code_expressiont(*it), side_effects.side_effects, mode); } } @@ -327,29 +344,30 @@ void goto_convertt::clean_expr( { Forall_operands(it, expr) { - clean_expr(*it, dest, mode, false); + side_effects.add(clean_expr(*it, mode, false)); // remember as expression statement for later checks if(it->is_not_nil()) - convert(code_expressiont(*it), dest, mode); + convert(code_expressiont(*it), side_effects.side_effects, mode); } expr = nil_exprt(); } - return; + return side_effects; } else if(expr.id() == ID_typecast) { typecast_exprt &typecast = to_typecast_expr(expr); // preserve 'result_is_used' - clean_expr(typecast.op(), dest, mode, result_is_used); + clean_expr_resultt side_effects = + clean_expr(typecast.op(), mode, result_is_used); if(typecast.op().is_nil()) expr.make_nil(); - return; + return side_effects; } else if(expr.id() == ID_side_effect) { @@ -359,16 +377,14 @@ void goto_convertt::clean_expr( if(statement == ID_gcc_conditional_expression) { // need to do separately - remove_gcc_conditional_expression(expr, dest, mode); - return; + return remove_gcc_conditional_expression(expr, mode); } else if(statement == ID_statement_expression) { // need to do separately to prevent that // the operands of expr get 'cleaned' - remove_statement_expression( - to_side_effect_expr(expr), dest, mode, result_is_used); - return; + return remove_statement_expression( + to_side_effect_expr(expr), mode, result_is_used); } else if(statement == ID_assign) { @@ -384,17 +400,17 @@ void goto_convertt::clean_expr( to_side_effect_expr(side_effect_assign.rhs()).get_statement() == ID_function_call) { - clean_expr(side_effect_assign.lhs(), dest, mode); + clean_expr_resultt side_effects = + clean_expr(side_effect_assign.lhs(), mode); exprt lhs = side_effect_assign.lhs(); const bool must_use_rhs = assignment_lhs_needs_temporary(lhs); if(must_use_rhs) { - remove_function_call( + side_effects.add(remove_function_call( to_side_effect_expr_function_call(side_effect_assign.rhs()), - dest, mode, - true); + true)); } // turn into code @@ -403,13 +419,14 @@ void goto_convertt::clean_expr( side_effect_assign.rhs(), new_lhs.type()); code_assignt assignment(std::move(new_lhs), new_rhs); assignment.add_source_location() = expr.source_location(); - convert_assign(assignment, dest, mode); + convert_assign(assignment, side_effects.side_effects, mode); if(result_is_used) expr = must_use_rhs ? new_rhs : lhs; else expr.make_nil(); - return; + + return side_effects; } } } @@ -422,19 +439,20 @@ void goto_convertt::clean_expr( else if(expr.id() == ID_address_of) { address_of_exprt &addr = to_address_of_expr(expr); - clean_expr_address_of(addr.object(), dest, mode); - return; + return clean_expr_address_of(addr.object(), mode); } + clean_expr_resultt side_effects; + // TODO: evaluation order Forall_operands(it, expr) - clean_expr(*it, dest, mode); + side_effects.add(clean_expr(*it, mode)); if(expr.id() == ID_side_effect) { - remove_side_effect( - to_side_effect_expr(expr), dest, mode, result_is_used, false); + side_effects.add(remove_side_effect( + to_side_effect_expr(expr), mode, result_is_used, false)); } else if(expr.id() == ID_compound_literal) { @@ -443,13 +461,15 @@ void goto_convertt::clean_expr( expr.operands().size() == 1, "ID_compound_literal has a single operand"); expr = to_unary_expr(expr).op(); } + + return side_effects; } -void goto_convertt::clean_expr_address_of( - exprt &expr, - goto_programt &dest, - const irep_idt &mode) +goto_convertt::clean_expr_resultt +goto_convertt::clean_expr_address_of(exprt &expr, const irep_idt &mode) { + clean_expr_resultt side_effects; + // The address of object constructors can be taken, // which is re-written into the address of a variable. @@ -457,8 +477,9 @@ void goto_convertt::clean_expr_address_of( { DATA_INVARIANT( expr.operands().size() == 1, "ID_compound_literal has a single operand"); - clean_expr(to_unary_expr(expr).op(), dest, mode); - expr = make_compound_literal(to_unary_expr(expr).op(), dest, mode); + side_effects.add(clean_expr(to_unary_expr(expr).op(), mode)); + expr = make_compound_literal( + to_unary_expr(expr).op(), side_effects.side_effects, mode); } else if(expr.id() == ID_string_constant) { @@ -468,13 +489,13 @@ void goto_convertt::clean_expr_address_of( else if(expr.id() == ID_index) { index_exprt &index_expr = to_index_expr(expr); - clean_expr_address_of(index_expr.array(), dest, mode); - clean_expr(index_expr.index(), dest, mode); + side_effects.add(clean_expr_address_of(index_expr.array(), mode)); + side_effects.add(clean_expr(index_expr.index(), mode)); } else if(expr.id() == ID_dereference) { dereference_exprt &deref_expr = to_dereference_expr(expr); - clean_expr(deref_expr.pointer(), dest, mode); + side_effects.add(clean_expr(deref_expr.pointer(), mode)); } else if(expr.id() == ID_comma) { @@ -492,38 +513,43 @@ void goto_convertt::clean_expr_address_of( result.swap(*it); else { - clean_expr(*it, dest, mode, false); + side_effects.add(clean_expr(*it, mode, false)); // get any side-effects if(it->is_not_nil()) - convert(code_expressiont(*it), dest, mode); + convert(code_expressiont(*it), side_effects.side_effects, mode); } } expr.swap(result); // do again - clean_expr_address_of(expr, dest, mode); + side_effects.add(clean_expr_address_of(expr, mode)); } else if(expr.id() == ID_side_effect) { - remove_side_effect(to_side_effect_expr(expr), dest, mode, true, true); + side_effects.add( + remove_side_effect(to_side_effect_expr(expr), mode, true, true)); } else Forall_operands(it, expr) - clean_expr_address_of(*it, dest, mode); + side_effects.add(clean_expr_address_of(*it, mode)); + + return side_effects; } -void goto_convertt::remove_gcc_conditional_expression( +goto_convertt::clean_expr_resultt +goto_convertt::remove_gcc_conditional_expression( exprt &expr, - goto_programt &dest, const irep_idt &mode) { + clean_expr_resultt side_effects; + { auto &binary_expr = to_binary_expr(expr); // first remove side-effects from condition - clean_expr(to_binary_expr(expr).op0(), dest, mode); + side_effects = clean_expr(to_binary_expr(expr).op0(), mode); // now we can copy op0 safely if_exprt if_expr( @@ -537,5 +563,7 @@ void goto_convertt::remove_gcc_conditional_expression( } // there might still be junk in expr.op2() - clean_expr(expr, dest, mode); + side_effects.add(clean_expr(expr, mode)); + + return side_effects; } diff --git a/src/ansi-c/goto-conversion/goto_convert.cpp b/src/ansi-c/goto-conversion/goto_convert.cpp index 4c2f8960ed8..d8b0db12aa8 100644 --- a/src/ansi-c/goto-conversion/goto_convert.cpp +++ b/src/ansi-c/goto-conversion/goto_convert.cpp @@ -760,7 +760,9 @@ void goto_convertt::convert_expression( } else { - clean_expr(expr, dest, mode, false); // result _not_ used + // result _not_ used + clean_expr_resultt side_effects = clean_expr(expr, mode, false); + dest.destructive_append(side_effects.side_effects); // Any residual expression? // We keep it to add checks later. @@ -771,6 +773,8 @@ void goto_convertt::convert_expression( tmp.add_source_location() = expr.source_location(); copy(tmp, OTHER, dest); } + + destruct_locals(side_effects.temporaries, dest, ns); } } @@ -806,7 +810,8 @@ void goto_convertt::convert_frontend_decl( const auto declaration_iterator = std::prev(dest.instructions.end()); auto initializer_location = initializer.find_source_location(); - clean_expr(initializer, dest, mode); + clean_expr_resultt side_effects = clean_expr(initializer, mode); + dest.destructive_append(side_effects.side_effects); if(initializer.is_not_nil()) { @@ -816,6 +821,8 @@ void goto_convertt::convert_frontend_decl( convert_assign(assign, dest, mode); } + destruct_locals(side_effects.temporaries, dest, ns); + return declaration_iterator; }(); @@ -855,7 +862,8 @@ void goto_convertt::convert_assign( { exprt lhs = code.lhs(), rhs = code.rhs(); - clean_expr(lhs, dest, mode); + clean_expr_resultt side_effects = clean_expr(lhs, mode); + dest.destructive_append(side_effects.side_effects); if(rhs.id() == ID_side_effect && rhs.get(ID_statement) == ID_function_call) { @@ -867,7 +875,10 @@ void goto_convertt::convert_assign( rhs.find_source_location()); Forall_operands(it, rhs) - clean_expr(*it, dest, mode); + { + side_effects.add(clean_expr(*it, mode)); + dest.destructive_append(side_effects.side_effects); + } do_function_call( lhs, @@ -881,7 +892,10 @@ void goto_convertt::convert_assign( rhs.get(ID_statement) == ID_cpp_new_array)) { Forall_operands(it, rhs) - clean_expr(*it, dest, mode); + { + side_effects.add(clean_expr(*it, mode)); + dest.destructive_append(side_effects.side_effects); + } // TODO: This should be done in a separate pass do_cpp_new(lhs, to_side_effect_expr(rhs), dest); @@ -895,7 +909,8 @@ void goto_convertt::convert_assign( rhs.get(ID_statement) == ID_gcc_conditional_expression)) { // handle above side effects - clean_expr(rhs, dest, mode); + side_effects.add(clean_expr(rhs, mode)); + dest.destructive_append(side_effects.side_effects); code_assignt new_assign(code); new_assign.lhs() = lhs; @@ -908,7 +923,10 @@ void goto_convertt::convert_assign( // preserve side effects that will be handled at later stages, // such as allocate, new operators of other languages, e.g. java, etc Forall_operands(it, rhs) - clean_expr(*it, dest, mode); + { + side_effects.add(clean_expr(*it, mode)); + dest.destructive_append(side_effects.side_effects); + } code_assignt new_assign(code); new_assign.lhs() = lhs; @@ -919,7 +937,8 @@ void goto_convertt::convert_assign( else { // do everything else - clean_expr(rhs, dest, mode); + side_effects.add(clean_expr(rhs, mode)); + dest.destructive_append(side_effects.side_effects); code_assignt new_assign(code); new_assign.lhs() = lhs; @@ -927,6 +946,8 @@ void goto_convertt::convert_assign( copy(new_assign, ASSIGN, dest); } + + destruct_locals(side_effects.temporaries, dest, ns); } void goto_convertt::convert_cpp_delete(const codet &code, goto_programt &dest) @@ -938,7 +959,8 @@ void goto_convertt::convert_cpp_delete(const codet &code, goto_programt &dest) exprt tmp_op = code.op0(); - clean_expr(tmp_op, dest, ID_cpp); + clean_expr_resultt side_effects = clean_expr(tmp_op, ID_cpp); + dest.destructive_append(side_effects.side_effects); // we call the destructor, and then free const exprt &destructor = @@ -987,6 +1009,8 @@ void goto_convertt::convert_cpp_delete(const codet &code, goto_programt &dest) delete_call.add_source_location() = code.source_location(); convert(delete_call, dest, ID_cpp); + + destruct_locals(side_effects.temporaries, dest, ns); } void goto_convertt::convert_assert( @@ -996,11 +1020,14 @@ void goto_convertt::convert_assert( { exprt cond = code.assertion(); - clean_expr(cond, dest, mode); + clean_expr_resultt side_effects = clean_expr(cond, mode); + dest.destructive_append(side_effects.side_effects); source_locationt annotated_location = code.source_location(); annotated_location.set("user-provided", true); dest.add(goto_programt::make_assertion(cond, annotated_location)); + + destruct_locals(side_effects.temporaries, dest, ns); } void goto_convertt::convert_skip(const codet &code, goto_programt &dest) @@ -1016,9 +1043,12 @@ void goto_convertt::convert_assume( { exprt op = code.assumption(); - clean_expr(op, dest, mode); + clean_expr_resultt side_effects = clean_expr(op, mode); + dest.destructive_append(side_effects.side_effects); dest.add(goto_programt::make_assumption(op, code.source_location())); + + destruct_locals(side_effects.temporaries, dest, ns); } void goto_convertt::convert_loop_contracts( @@ -1072,10 +1102,12 @@ void goto_convertt::convert_for( //----------------------------- // A; // u: sideeffects in c - // v: if(!c) goto z; + // v: if(!c) goto Z; + // cleanup-loop; // w: P; // x: B; <-- continue target // y: goto u; + // Z: cleanup-out; // z: ; <-- break target // A; @@ -1084,23 +1116,25 @@ void goto_convertt::convert_for( exprt cond = code.cond(); - goto_programt sideeffects; - clean_expr(cond, sideeffects, mode); + clean_expr_resultt side_effects = clean_expr(cond, mode); // save break/continue targets break_continue_targetst old_targets(targets); // do the u label - goto_programt::targett u = sideeffects.instructions.begin(); + goto_programt::targett u = side_effects.side_effects.instructions.begin(); // do the v label goto_programt tmp_v; goto_programt::targett v = tmp_v.add(goto_programt::instructiont()); + destruct_locals(side_effects.temporaries, tmp_v, ns); - // do the z label + // do the z and Z labels goto_programt tmp_z; + destruct_locals(side_effects.temporaries, tmp_z, ns); goto_programt::targett z = tmp_z.add(goto_programt::make_skip(code.source_location())); + goto_programt::targett Z = tmp_z.instructions.begin(); // do the x label goto_programt tmp_x; @@ -1113,23 +1147,25 @@ void goto_convertt::convert_for( { exprt tmp_B = code.iter(); - clean_expr(tmp_B, tmp_x, mode, false); + clean_expr_resultt side_effects_iter = clean_expr(tmp_B, mode, false); + tmp_x.destructive_append(side_effects_iter.side_effects); + destruct_locals(side_effects_iter.temporaries, tmp_x, ns); if(tmp_x.instructions.empty()) tmp_x.add(goto_programt::make_skip(code.source_location())); } // optimize the v label - if(sideeffects.instructions.empty()) + if(side_effects.side_effects.instructions.empty()) u = v; // set the targets targets.set_break(z); targets.set_continue(tmp_x.instructions.begin()); - // v: if(!c) goto z; + // v: if(!c) goto Z; *v = - goto_programt::make_goto(z, boolean_negate(cond), cond.source_location()); + goto_programt::make_goto(Z, boolean_negate(cond), cond.source_location()); // do the w label goto_programt tmp_w; @@ -1143,7 +1179,7 @@ void goto_convertt::convert_for( // assigns clause, loop invariant and decreases clause convert_loop_contracts(code, y); - dest.destructive_append(sideeffects); + dest.destructive_append(side_effects.side_effects); dest.destructive_append(tmp_v); dest.destructive_append(tmp_w); dest.destructive_append(tmp_x); @@ -1225,14 +1261,16 @@ void goto_convertt::convert_dowhile( exprt cond = code.cond(); - goto_programt sideeffects; - clean_expr(cond, sideeffects, mode); + clean_expr_resultt side_effects = clean_expr(cond, mode); // do P while(c); //-------------------- // w: P; // x: sideeffects in c <-- continue target - // y: if(c) goto w; + // y: if(!c) goto C; + // cleanup-loop; + // W: goto w; + // C: cleanup-out; // z: ; <-- break target // save break/continue targets @@ -1240,20 +1278,28 @@ void goto_convertt::convert_dowhile( // do the y label goto_programt tmp_y; - goto_programt::targett y = - tmp_y.add(goto_programt::make_incomplete_goto(cond, condition_location)); + goto_programt::targett y = tmp_y.add(goto_programt::make_incomplete_goto( + boolean_negate(cond), condition_location)); + destruct_locals(side_effects.temporaries, tmp_y, ns); + goto_programt::targett W = tmp_y.add( + goto_programt::make_incomplete_goto(true_exprt{}, condition_location)); - // do the z label + // do the z label and C labels goto_programt tmp_z; + destruct_locals(side_effects.temporaries, tmp_z, ns); goto_programt::targett z = tmp_z.add(goto_programt::make_skip(code.source_location())); + goto_programt::targett C = tmp_z.instructions.begin(); + + // y: if(!c) goto C; + y->complete_goto(C); // do the x label goto_programt::targett x; - if(sideeffects.instructions.empty()) + if(side_effects.side_effects.instructions.empty()) x = y; else - x = sideeffects.instructions.begin(); + x = side_effects.side_effects.instructions.begin(); // set the targets targets.set_break(z); @@ -1264,14 +1310,14 @@ void goto_convertt::convert_dowhile( convert(code.body(), tmp_w, mode); goto_programt::targett w = tmp_w.instructions.begin(); - // y: if(c) goto w; - y->complete_goto(w); + // W: goto w; + W->complete_goto(w); // assigns_clause, loop invariant and decreases clause convert_loop_contracts(code, y); dest.destructive_append(tmp_w); - dest.destructive_append(sideeffects); + dest.destructive_append(side_effects.side_effects); dest.destructive_append(tmp_y); dest.destructive_append(tmp_z); @@ -1343,8 +1389,7 @@ void goto_convertt::convert_switch( // do the value we switch over exprt argument = code.value(); - goto_programt sideeffects; - clean_expr(argument, sideeffects, mode); + clean_expr_resultt side_effects = clean_expr(argument, mode); // Avoid potential performance penalties caused by evaluating the value // multiple times (as the below chain-of-ifs does). "needs_cleaning" isn't @@ -1356,15 +1401,16 @@ void goto_convertt::convert_switch( symbolt &new_symbol = new_tmp_symbol( argument.type(), "switch_value", - sideeffects, + side_effects.side_effects, code.source_location(), mode); code_assignt copy_value{ new_symbol.symbol_expr(), argument, code.source_location()}; - convert(copy_value, sideeffects, mode); + convert(copy_value, side_effects.side_effects, mode); argument = new_symbol.symbol_expr(); + side_effects.add_temporary(to_symbol_expr(argument).get_identifier()); } // save break/default/cases targets @@ -1411,16 +1457,35 @@ void goto_convertt::convert_switch( source_locationt source_location = case_ops.front().find_source_location(); source_location.set_case_number(std::to_string(case_number)); case_number++; - guard_expr.add_source_location() = source_location; - tmp_cases.add(goto_programt::make_goto( - case_pair.first, std::move(guard_expr), source_location)); + if(side_effects.temporaries.empty()) + { + guard_expr.add_source_location() = source_location; + + tmp_cases.add(goto_programt::make_goto( + case_pair.first, std::move(guard_expr), source_location)); + } + else + { + guard_expr = boolean_negate(guard_expr); + guard_expr.add_source_location() = source_location; + + goto_programt::targett try_next = + tmp_cases.add(goto_programt::make_incomplete_goto( + std::move(guard_expr), source_location)); + destruct_locals(side_effects.temporaries, tmp_cases, ns); + tmp_cases.add(goto_programt::make_goto( + case_pair.first, true_exprt{}, source_location)); + goto_programt::targett next_case = + tmp_cases.add(goto_programt::make_skip(source_location)); + try_next->complete_goto(next_case); + } } tmp_cases.add(goto_programt::make_goto( targets.default_target, targets.default_target->source_location())); - dest.destructive_append(sideeffects); + dest.destructive_append(side_effects.side_effects); dest.destructive_append(tmp_cases); dest.destructive_append(tmp); dest.destructive_append(tmp_z); @@ -1463,14 +1528,14 @@ void goto_convertt::convert_return( code.find_source_location()); code_frontend_returnt new_code(code); + clean_expr_resultt side_effects; if(new_code.has_return_value()) { bool result_is_used = new_code.return_value().type().id() != ID_empty; - goto_programt sideeffects; - clean_expr(new_code.return_value(), sideeffects, mode, result_is_used); - dest.destructive_append(sideeffects); + side_effects = clean_expr(new_code.return_value(), mode, result_is_used); + dest.destructive_append(side_effects.side_effects); // remove void-typed return value if(!result_is_used) @@ -1487,6 +1552,7 @@ void goto_convertt::convert_return( // Now add a 'set return value' instruction to set the return value. dest.add(goto_programt::make_set_return_value( new_code.return_value(), new_code.source_location())); + destruct_locals(side_effects.temporaries, dest, ns); } else { @@ -1619,10 +1685,12 @@ void goto_convertt::convert_ifthenelse( } exprt tmp_guard = code.cond(); - clean_expr(tmp_guard, dest, mode); + clean_expr_resultt side_effects = clean_expr(tmp_guard, mode); + dest.destructive_append(side_effects.side_effects); // convert 'then'-branch goto_programt tmp_then; + destruct_locals(side_effects.temporaries, tmp_then, ns); convert(code.then_case(), tmp_then, mode); source_locationt then_end_location = code.then_case().get_statement() == ID_block @@ -1630,6 +1698,7 @@ void goto_convertt::convert_ifthenelse( : code.then_case().source_location(); goto_programt tmp_else; + destruct_locals(side_effects.temporaries, tmp_else, ns); source_locationt else_end_location; if(has_else) @@ -1882,9 +1951,14 @@ void goto_convertt::generate_conditional_branch( { // simple branch exprt cond = guard; - clean_expr(cond, dest, mode); + clean_expr_resultt side_effects = clean_expr(cond, mode); + dest.destructive_append(side_effects.side_effects); dest.add(goto_programt::make_goto(target_true, cond, source_location)); + goto_programt tmp_destruct; + destruct_locals(side_effects.temporaries, tmp_destruct, ns); + dest.insert_before_swap(target_true, tmp_destruct); + destruct_locals(side_effects.temporaries, dest, ns); } } @@ -1954,13 +2028,19 @@ void goto_convertt::generate_conditional_branch( } exprt cond = guard; - clean_expr(cond, dest, mode); + clean_expr_resultt side_effects = clean_expr(cond, mode); + dest.destructive_append(side_effects.side_effects); // true branch dest.add(goto_programt::make_goto(target_true, cond, source_location)); + goto_programt tmp_destruct; + destruct_locals(side_effects.temporaries, tmp_destruct, ns); + dest.insert_before_swap(target_true, tmp_destruct); // false branch dest.add(goto_programt::make_goto(target_false, source_location)); + destruct_locals(side_effects.temporaries, tmp_destruct, ns); + dest.insert_before_swap(target_false, tmp_destruct); } bool goto_convertt::get_string_constant(const exprt &expr, irep_idt &value) @@ -2065,14 +2145,16 @@ symbolt &goto_convertt::new_tmp_symbol( mode, symbol_table); - code_frontend_declt decl(new_symbol.symbol_expr()); - decl.add_source_location() = source_location; - convert_frontend_decl(decl, dest, mode); + if(type.id() != ID_code) + { + dest.add( + goto_programt::make_decl(new_symbol.symbol_expr(), source_location)); + } return new_symbol; } -void goto_convertt::make_temp_symbol( +irep_idt goto_convertt::make_temp_symbol( exprt &expr, const std::string &suffix, goto_programt &dest, @@ -2091,6 +2173,8 @@ void goto_convertt::make_temp_symbol( convert(assignment, dest, mode); expr = new_symbol.symbol_expr(); + + return to_symbol_expr(expr).get_identifier(); } void goto_convert( diff --git a/src/ansi-c/goto-conversion/goto_convert_class.h b/src/ansi-c/goto-conversion/goto_convert_class.h index 1256d10ad41..600938751f3 100644 --- a/src/ansi-c/goto-conversion/goto_convert_class.h +++ b/src/ansi-c/goto-conversion/goto_convert_class.h @@ -56,6 +56,32 @@ class goto_convertt : public messaget std::string tmp_symbol_prefix; lifetimet lifetime = lifetimet::STATIC_GLOBAL; + struct clean_expr_resultt + { + /// Identifiers of temporaries introduced while cleaning an expression. The + /// caller needs to add destructors for these (via `destruct_locals`) on all + /// control-flow paths as soon as the temporaries are no longer needed. + std::list temporaries; + /// Statements implementing side effects of the expression that was subject + /// to cleaning. The caller needs to merge (typically via + /// `destructive_append`) these statements into the destination GOTO + /// program. + goto_programt side_effects; + + clean_expr_resultt() = default; + + void add(clean_expr_resultt &&other) + { + temporaries.splice(temporaries.begin(), other.temporaries); + side_effects.destructive_append(other.side_effects); + } + + void add_temporary(const irep_idt &id) + { + temporaries.push_front(id); + } + }; + void goto_convert_rec( const codet &code, goto_programt &dest, @@ -64,7 +90,7 @@ class goto_convertt : public messaget // // tools for symbols // - symbolt &new_tmp_symbol( + [[nodiscard]] symbolt &new_tmp_symbol( const typet &type, const std::string &suffix, goto_programt &dest, @@ -81,14 +107,11 @@ class goto_convertt : public messaget // into the program logic // - void clean_expr( - exprt &expr, - goto_programt &dest, - const irep_idt &mode, - bool result_is_used = true); + [[nodiscard]] clean_expr_resultt + clean_expr(exprt &expr, const irep_idt &mode, bool result_is_used = true); - void - clean_expr_address_of(exprt &expr, goto_programt &dest, const irep_idt &mode); + [[nodiscard]] clean_expr_resultt + clean_expr_address_of(exprt &expr, const irep_idt &mode); static bool needs_cleaning(const exprt &expr); @@ -101,7 +124,7 @@ class goto_convertt : public messaget return lhs.id() != ID_symbol; } - void make_temp_symbol( + [[nodiscard]] irep_idt make_temp_symbol( exprt &expr, const std::string &suffix, goto_programt &, @@ -109,57 +132,46 @@ class goto_convertt : public messaget void rewrite_boolean(exprt &dest); - void remove_side_effect( + [[nodiscard]] clean_expr_resultt remove_side_effect( side_effect_exprt &expr, - goto_programt &dest, const irep_idt &mode, bool result_is_used, bool address_taken); - void remove_assignment( + [[nodiscard]] clean_expr_resultt remove_assignment( side_effect_exprt &expr, - goto_programt &dest, bool result_is_used, bool address_taken, const irep_idt &mode); - void remove_pre( + [[nodiscard]] clean_expr_resultt remove_pre( side_effect_exprt &expr, - goto_programt &dest, bool result_is_used, bool address_taken, const irep_idt &mode); - void remove_post( + [[nodiscard]] clean_expr_resultt remove_post( side_effect_exprt &expr, - goto_programt &dest, const irep_idt &mode, bool result_is_used); - void remove_function_call( + [[nodiscard]] clean_expr_resultt remove_function_call( side_effect_expr_function_callt &expr, - goto_programt &dest, const irep_idt &mode, bool result_is_used); - void remove_cpp_new( - side_effect_exprt &expr, - goto_programt &dest, - bool result_is_used); - void remove_cpp_delete(side_effect_exprt &expr, goto_programt &dest); - void remove_malloc( + [[nodiscard]] clean_expr_resultt + remove_cpp_new(side_effect_exprt &expr, bool result_is_used); + [[nodiscard]] clean_expr_resultt remove_cpp_delete(side_effect_exprt &expr); + [[nodiscard]] clean_expr_resultt remove_malloc( side_effect_exprt &expr, - goto_programt &dest, const irep_idt &mode, bool result_is_used); - void remove_temporary_object(side_effect_exprt &expr, goto_programt &dest); - void remove_statement_expression( + [[nodiscard]] clean_expr_resultt + remove_temporary_object(side_effect_exprt &expr); + [[nodiscard]] clean_expr_resultt remove_statement_expression( side_effect_exprt &expr, - goto_programt &dest, const irep_idt &mode, bool result_is_used); - void remove_gcc_conditional_expression( - exprt &expr, - goto_programt &dest, - const irep_idt &mode); - void remove_overflow( + [[nodiscard]] clean_expr_resultt + remove_gcc_conditional_expression(exprt &expr, const irep_idt &mode); + [[nodiscard]] clean_expr_resultt remove_overflow( side_effect_expr_overflowt &expr, - goto_programt &dest, bool result_is_used, const irep_idt &mode); diff --git a/src/ansi-c/goto-conversion/goto_convert_function_call.cpp b/src/ansi-c/goto-conversion/goto_convert_function_call.cpp index 062d56a9681..2fdc5c3e616 100644 --- a/src/ansi-c/goto-conversion/goto_convert_function_call.cpp +++ b/src/ansi-c/goto-conversion/goto_convert_function_call.cpp @@ -15,6 +15,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include "destructor.h" + void goto_convertt::convert_function_call( const code_function_callt &function_call, goto_programt &dest, @@ -41,13 +43,17 @@ void goto_convertt::do_function_call( exprt::operandst new_arguments = arguments; + clean_expr_resultt side_effects; + if(!new_lhs.is_nil()) - clean_expr(new_lhs, dest, mode); + side_effects.add(clean_expr(new_lhs, mode)); - clean_expr(new_function, dest, mode); + side_effects.add(clean_expr(new_function, mode)); for(auto &new_argument : new_arguments) - clean_expr(new_argument, dest, mode); + side_effects.add(clean_expr(new_argument, mode)); + + dest.destructive_append(side_effects.side_effects); // split on the function @@ -78,6 +84,8 @@ void goto_convertt::do_function_call( new_function.id(), function.find_source_location()); } + + destruct_locals(side_effects.temporaries, dest, ns); } void goto_convertt::do_function_call_if( diff --git a/src/ansi-c/goto-conversion/goto_convert_side_effect.cpp b/src/ansi-c/goto-conversion/goto_convert_side_effect.cpp index b5720722e68..28943332d12 100644 --- a/src/ansi-c/goto-conversion/goto_convert_side_effect.cpp +++ b/src/ansi-c/goto-conversion/goto_convert_side_effect.cpp @@ -22,9 +22,10 @@ Author: Daniel Kroening, kroening@kroening.com #include -void goto_convertt::remove_assignment( +#include "destructor.h" + +goto_convertt::clean_expr_resultt goto_convertt::remove_assignment( side_effect_exprt &expr, - goto_programt &dest, bool result_is_used, bool address_taken, const irep_idt &mode) @@ -33,6 +34,8 @@ void goto_convertt::remove_assignment( std::optional replacement_expr_opt; + clean_expr_resultt side_effects; + if(statement == ID_assign) { auto &old_assignment = to_side_effect_expr_assign(expr); @@ -43,7 +46,10 @@ void goto_convertt::remove_assignment( assignment_lhs_needs_temporary(old_assignment.lhs())) { if(!old_assignment.rhs().is_constant()) - make_temp_symbol(old_assignment.rhs(), "assign", dest, mode); + { + side_effects.add_temporary(make_temp_symbol( + old_assignment.rhs(), "assign", side_effects.side_effects, mode)); + } replacement_expr_opt = typecast_exprt::conditional_cast(old_assignment.rhs(), new_lhs.type()); @@ -54,7 +60,7 @@ void goto_convertt::remove_assignment( code_assignt new_assignment(std::move(new_lhs), std::move(new_rhs)); new_assignment.add_source_location() = expr.source_location(); - convert_assign(new_assignment, dest, mode); + convert_assign(new_assignment, side_effects.side_effects, mode); } else if( statement == ID_assign_plus || statement == ID_assign_minus || @@ -113,7 +119,8 @@ void goto_convertt::remove_assignment( result_is_used && !address_taken && assignment_lhs_needs_temporary(binary_expr.op0())) { - make_temp_symbol(rhs, "assign", dest, mode); + side_effects.add_temporary( + make_temp_symbol(rhs, "assign", side_effects.side_effects, mode)); replacement_expr_opt = typecast_exprt::conditional_cast(rhs, new_lhs.type()); } @@ -123,7 +130,7 @@ void goto_convertt::remove_assignment( code_assignt assignment(new_lhs, rhs); assignment.add_source_location() = expr.source_location(); - convert(assignment, dest, mode); + convert(assignment, side_effects.side_effects, mode); } else UNREACHABLE; @@ -134,8 +141,14 @@ void goto_convertt::remove_assignment( exprt new_lhs = typecast_exprt::conditional_cast(*replacement_expr_opt, expr.type()); expr.swap(new_lhs); + + return side_effects; } - else if(result_is_used) + + destruct_locals(side_effects.temporaries, side_effects.side_effects, ns); + side_effects.temporaries.clear(); + + if(result_is_used) { exprt lhs = to_binary_expr(expr).op0(); // assign_* statements can have an lhs operand with a different type than @@ -159,11 +172,12 @@ void goto_convertt::remove_assignment( } else expr.make_nil(); + + return side_effects; } -void goto_convertt::remove_pre( +goto_convertt::clean_expr_resultt goto_convertt::remove_pre( side_effect_exprt &expr, - goto_programt &dest, bool result_is_used, bool address_taken, const irep_idt &mode) @@ -227,13 +241,15 @@ void goto_convertt::remove_pre( const bool cannot_use_lhs = result_is_used && !address_taken && assignment_lhs_needs_temporary(lhs); + clean_expr_resultt side_effects; if(cannot_use_lhs) - make_temp_symbol(rhs, "pre", dest, mode); + side_effects.add_temporary( + make_temp_symbol(rhs, "pre", side_effects.side_effects, mode)); code_assignt assignment(lhs, rhs); assignment.add_source_location() = expr.find_source_location(); - convert(assignment, dest, mode); + convert(assignment, side_effects.side_effects, mode); if(result_is_used) { @@ -251,11 +267,12 @@ void goto_convertt::remove_pre( } else expr.make_nil(); + + return side_effects; } -void goto_convertt::remove_post( +goto_convertt::clean_expr_resultt goto_convertt::remove_post( side_effect_exprt &expr, - goto_programt &dest, const irep_idt &mode, bool result_is_used) { @@ -316,6 +333,8 @@ void goto_convertt::remove_post( // fix up the expression, if needed + clean_expr_resultt side_effects; + if(result_is_used) { exprt tmp = op; @@ -326,29 +345,33 @@ void goto_convertt::remove_post( suffix += "_" + id2string(base_name); } - make_temp_symbol(tmp, suffix, dest, mode); + side_effects.add_temporary( + make_temp_symbol(tmp, suffix, side_effects.side_effects, mode)); expr.swap(tmp); } else expr.make_nil(); - dest.destructive_append(tmp1); - dest.destructive_append(tmp2); + side_effects.side_effects.destructive_append(tmp1); + side_effects.side_effects.destructive_append(tmp2); + + return side_effects; } -void goto_convertt::remove_function_call( +goto_convertt::clean_expr_resultt goto_convertt::remove_function_call( side_effect_expr_function_callt &expr, - goto_programt &dest, const irep_idt &mode, bool result_is_used) { + clean_expr_resultt side_effects; + if(!result_is_used) { code_function_callt call(expr.function(), expr.arguments()); call.add_source_location() = expr.source_location(); - convert_function_call(call, dest, mode); + convert_function_call(call, side_effects.side_effects, mode); expr.make_nil(); - return; + return side_effects; } // get name of function, if available @@ -374,21 +397,23 @@ void goto_convertt::remove_function_call( new_symbol_mode, symbol_table); - { - code_frontend_declt decl(new_symbol.symbol_expr()); - decl.add_source_location() = new_symbol.location; - convert_frontend_decl(decl, dest, mode); - } + PRECONDITION(expr.type().id() != ID_code); + side_effects.side_effects.add( + goto_programt::make_decl(new_symbol.symbol_expr(), new_symbol.location)); { goto_programt tmp_program2; code_function_callt call( new_symbol.symbol_expr(), expr.function(), expr.arguments()); call.add_source_location() = new_symbol.location; - convert_function_call(call, dest, mode); + convert_function_call(call, side_effects.side_effects, mode); } static_cast(expr) = new_symbol.symbol_expr(); + + side_effects.add_temporary(to_symbol_expr(expr).get_identifier()); + + return side_effects; } void goto_convertt::replace_new_object(const exprt &object, exprt &dest) @@ -400,10 +425,8 @@ void goto_convertt::replace_new_object(const exprt &object, exprt &dest) replace_new_object(object, *it); } -void goto_convertt::remove_cpp_new( - side_effect_exprt &expr, - goto_programt &dest, - bool result_is_used) +goto_convertt::clean_expr_resultt +goto_convertt::remove_cpp_new(side_effect_exprt &expr, bool result_is_used) { const symbolt &new_symbol = get_fresh_aux_symbol( expr.type(), @@ -413,23 +436,29 @@ void goto_convertt::remove_cpp_new( ID_cpp, symbol_table); - code_frontend_declt decl(new_symbol.symbol_expr()); - decl.add_source_location() = new_symbol.location; - convert_frontend_decl(decl, dest, ID_cpp); + clean_expr_resultt side_effects; + + PRECONDITION(expr.type().id() != ID_code); + side_effects.side_effects.add( + goto_programt::make_decl(new_symbol.symbol_expr(), new_symbol.location)); const code_assignt call(new_symbol.symbol_expr(), expr); + convert(call, side_effects.side_effects, ID_cpp); + if(result_is_used) + { static_cast(expr) = new_symbol.symbol_expr(); + side_effects.add_temporary(to_symbol_expr(expr).get_identifier()); + } else expr.make_nil(); - convert(call, dest, ID_cpp); + return side_effects; } -void goto_convertt::remove_cpp_delete( - side_effect_exprt &expr, - goto_programt &dest) +goto_convertt::clean_expr_resultt +goto_convertt::remove_cpp_delete(side_effect_exprt &expr) { DATA_INVARIANT(expr.operands().size() == 1, "cpp_delete expects one operand"); @@ -438,17 +467,21 @@ void goto_convertt::remove_cpp_delete( tmp.copy_to_operands(to_unary_expr(expr).op()); tmp.set(ID_destructor, expr.find(ID_destructor)); - convert_cpp_delete(tmp, dest); + clean_expr_resultt side_effects; + convert_cpp_delete(tmp, side_effects.side_effects); expr.make_nil(); + + return side_effects; } -void goto_convertt::remove_malloc( +goto_convertt::clean_expr_resultt goto_convertt::remove_malloc( side_effect_exprt &expr, - goto_programt &dest, const irep_idt &mode, bool result_is_used) { + clean_expr_resultt side_effects; + if(result_is_used) { const symbolt &new_symbol = get_fresh_aux_symbol( @@ -461,40 +494,47 @@ void goto_convertt::remove_malloc( code_frontend_declt decl(new_symbol.symbol_expr()); decl.add_source_location() = new_symbol.location; - convert_frontend_decl(decl, dest, mode); + convert_frontend_decl(decl, side_effects.side_effects, mode); code_assignt call(new_symbol.symbol_expr(), expr); call.add_source_location() = expr.source_location(); static_cast(expr) = new_symbol.symbol_expr(); - convert(call, dest, mode); + convert(call, side_effects.side_effects, mode); + + side_effects.add_temporary(to_symbol_expr(expr).get_identifier()); } else - { - convert(code_expressiont(std::move(expr)), dest, mode); - } + convert(code_expressiont(std::move(expr)), side_effects.side_effects, mode); + + return side_effects; } -void goto_convertt::remove_temporary_object( - side_effect_exprt &expr, - goto_programt &dest) +goto_convertt::clean_expr_resultt +goto_convertt::remove_temporary_object(side_effect_exprt &expr) { + clean_expr_resultt side_effects; + const irep_idt &mode = expr.get(ID_mode); INVARIANT_WITH_DIAGNOSTICS( expr.operands().size() <= 1, "temporary_object takes zero or one operands", expr.find_source_location()); - symbolt &new_symbol = - new_tmp_symbol(expr.type(), "obj", dest, expr.find_source_location(), mode); + symbolt &new_symbol = new_tmp_symbol( + expr.type(), + "obj", + side_effects.side_effects, + expr.find_source_location(), + mode); if(expr.operands().size() == 1) { const code_assignt assignment( new_symbol.symbol_expr(), to_unary_expr(expr).op()); - convert(assignment, dest, mode); + convert(assignment, side_effects.side_effects, mode); } if(expr.find(ID_initializer).is_not_nil()) @@ -506,18 +546,23 @@ void goto_convertt::remove_temporary_object( exprt initializer = static_cast(expr.find(ID_initializer)); replace_new_object(new_symbol.symbol_expr(), initializer); - convert(to_code(initializer), dest, mode); + convert(to_code(initializer), side_effects.side_effects, mode); } static_cast(expr) = new_symbol.symbol_expr(); + + side_effects.add_temporary(to_symbol_expr(expr).get_identifier()); + + return side_effects; } -void goto_convertt::remove_statement_expression( +goto_convertt::clean_expr_resultt goto_convertt::remove_statement_expression( side_effect_exprt &expr, - goto_programt &dest, const irep_idt &mode, bool result_is_used) { + clean_expr_resultt side_effects; + // This is a gcc extension of the form ({ ....; expr; }) // The value is that of the final expression. // The expression is copied into a temporary before the @@ -527,9 +572,9 @@ void goto_convertt::remove_statement_expression( if(!result_is_used) { - convert(code, dest, mode); + convert(code, side_effects.side_effects, mode); expr.make_nil(); - return; + return side_effects; } INVARIANT_WITH_DIAGNOSTICS( @@ -548,7 +593,11 @@ void goto_convertt::remove_statement_expression( source_locationt source_location = last.find_source_location(); symbolt &new_symbol = new_tmp_symbol( - expr.type(), "statement_expression", dest, source_location, mode); + expr.type(), + "statement_expression", + side_effects.side_effects, + source_location, + mode); symbol_exprt tmp_symbol_expr(new_symbol.name, new_symbol.type); tmp_symbol_expr.add_source_location() = source_location; @@ -572,18 +621,17 @@ void goto_convertt::remove_statement_expression( UNREACHABLE; } - { - goto_programt tmp; - convert(code, tmp, mode); - dest.destructive_append(tmp); - } + convert(code, side_effects.side_effects, mode); static_cast(expr) = tmp_symbol_expr; + + side_effects.add_temporary(to_symbol_expr(expr).get_identifier()); + + return side_effects; } -void goto_convertt::remove_overflow( +goto_convertt::clean_expr_resultt goto_convertt::remove_overflow( side_effect_expr_overflowt &expr, - goto_programt &dest, bool result_is_used, const irep_idt &mode) { @@ -592,12 +640,14 @@ void goto_convertt::remove_overflow( const exprt &rhs = expr.rhs(); const exprt &result = expr.result(); + clean_expr_resultt side_effects; + if(result.type().id() != ID_pointer) { // result of the arithmetic operation is _not_ used, just evaluate side // effects exprt tmp = result; - clean_expr(tmp, dest, mode, false); + side_effects.add(clean_expr(tmp, mode, false)); // the is-there-an-overflow result may be used if(result_is_used) @@ -627,7 +677,13 @@ void goto_convertt::remove_overflow( overflow_with_result.add_source_location() = expr.source_location(); if(result_is_used) - make_temp_symbol(overflow_with_result, "overflow_result", dest, mode); + { + side_effects.add_temporary(make_temp_symbol( + overflow_with_result, + "overflow_result", + side_effects.side_effects, + mode)); + } const struct_typet::componentst &result_comps = to_struct_type(overflow_with_result.type()).components(); @@ -637,7 +693,7 @@ void goto_convertt::remove_overflow( typecast_exprt::conditional_cast( member_exprt{overflow_with_result, result_comps[0]}, arith_type), expr.source_location()}; - convert_assign(result_assignment, dest, mode); + convert_assign(result_assignment, side_effects.side_effects, mode); if(result_is_used) { @@ -649,11 +705,12 @@ void goto_convertt::remove_overflow( else expr.make_nil(); } + + return side_effects; } -void goto_convertt::remove_side_effect( +goto_convertt::clean_expr_resultt goto_convertt::remove_side_effect( side_effect_exprt &expr, - goto_programt &dest, const irep_idt &mode, bool result_is_used, bool address_taken) @@ -661,8 +718,10 @@ void goto_convertt::remove_side_effect( const irep_idt &statement = expr.get_statement(); if(statement == ID_function_call) - remove_function_call( - to_side_effect_expr_function_call(expr), dest, mode, result_is_used); + { + return remove_function_call( + to_side_effect_expr_function_call(expr), mode, result_is_used); + } else if( statement == ID_assign || statement == ID_assign_plus || statement == ID_assign_minus || statement == ID_assign_mult || @@ -670,47 +729,68 @@ void goto_convertt::remove_side_effect( statement == ID_assign_bitxor || statement == ID_assign_bitand || statement == ID_assign_lshr || statement == ID_assign_ashr || statement == ID_assign_shl || statement == ID_assign_mod) - remove_assignment(expr, dest, result_is_used, address_taken, mode); + { + return remove_assignment(expr, result_is_used, address_taken, mode); + } else if(statement == ID_postincrement || statement == ID_postdecrement) - remove_post(expr, dest, mode, result_is_used); + { + return remove_post(expr, mode, result_is_used); + } else if(statement == ID_preincrement || statement == ID_predecrement) - remove_pre(expr, dest, result_is_used, address_taken, mode); + { + return remove_pre(expr, result_is_used, address_taken, mode); + } else if(statement == ID_cpp_new || statement == ID_cpp_new_array) - remove_cpp_new(expr, dest, result_is_used); + { + return remove_cpp_new(expr, result_is_used); + } else if(statement == ID_cpp_delete || statement == ID_cpp_delete_array) - remove_cpp_delete(expr, dest); + { + return remove_cpp_delete(expr); + } else if(statement == ID_allocate) - remove_malloc(expr, dest, mode, result_is_used); + { + return remove_malloc(expr, mode, result_is_used); + } else if(statement == ID_temporary_object) - remove_temporary_object(expr, dest); + { + return remove_temporary_object(expr); + } else if(statement == ID_statement_expression) - remove_statement_expression(expr, dest, mode, result_is_used); + { + return remove_statement_expression(expr, mode, result_is_used); + } else if(statement == ID_nondet) { // these are fine + return {}; } else if(statement == ID_skip) { expr.make_nil(); + return {}; } else if(statement == ID_throw) { + clean_expr_resultt side_effects; + codet code = code_expressiont(side_effect_expr_throwt( expr.find(ID_exception_list), expr.type(), expr.source_location())); code.op0().operands().swap(expr.operands()); code.add_source_location() = expr.source_location(); - dest.add(goto_programt::instructiont( + side_effects.side_effects.add(goto_programt::instructiont( std::move(code), expr.source_location(), THROW, nil_exprt(), {})); // the result can't be used, these are void expr.make_nil(); + return side_effects; } else if( statement == ID_overflow_plus || statement == ID_overflow_minus || statement == ID_overflow_mult) { - remove_overflow( - to_side_effect_expr_overflow(expr), dest, result_is_used, mode); + return remove_overflow( + to_side_effect_expr_overflow(expr), result_is_used, mode); } else { diff --git a/src/cprover/simplify_state_expr.cpp b/src/cprover/simplify_state_expr.cpp index 44700528df2..d11f031a8b5 100644 --- a/src/cprover/simplify_state_expr.cpp +++ b/src/cprover/simplify_state_expr.cpp @@ -517,6 +517,10 @@ exprt simplify_object_size_expr( { return src.with_state(to_update_state_expr(src.state()).state()); } + else if(src.state().id() == ID_exit_scope_state) + { + return src.with_state(to_exit_scope_state_expr(src.state()).state()); + } return std::move(src); } diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index 36eff629528..15f83a46504 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -581,13 +581,16 @@ static void generate_contract_constraints( goto_programt constraint; if(location.get_property_class() == ID_assume) { - converter.goto_convert(code_assumet(instantiated_clause), constraint, mode); + code_assumet assumption(instantiated_clause); + assumption.add_source_location() = location; + converter.goto_convert(assumption, constraint, mode); } else { - converter.goto_convert(code_assertt(instantiated_clause), constraint, mode); + code_assertt assertion(instantiated_clause); + assertion.add_source_location() = location; + converter.goto_convert(assertion, constraint, mode); } - constraint.instructions.back().source_location_nonconst() = location; is_fresh_update(constraint); throw_on_unsupported(constraint); program.destructive_append(constraint); 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 index 6c0d8baf321..8a97ef48fd0 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp @@ -21,6 +21,7 @@ Date: February 2023 #include #include +#include #include #include @@ -104,8 +105,9 @@ void dfcc_contract_clauses_codegent::encode_assignable_target_group( // clean up side effects from the condition expression if needed cleanert cleaner(goto_model.symbol_table, log.get_message_handler()); exprt condition(group.condition()); + std::list new_vars; if(has_subexpr(condition, ID_side_effect)) - cleaner.clean(condition, dest, language_mode); + new_vars = cleaner.clean(condition, dest, language_mode); // Jump target if condition is false auto goto_instruction = dest.add( @@ -116,6 +118,8 @@ void dfcc_contract_clauses_codegent::encode_assignable_target_group( auto label_instruction = dest.add(goto_programt::make_skip(source_location)); goto_instruction->complete_goto(label_instruction); + + destruct_locals(new_vars, dest, ns); } void dfcc_contract_clauses_codegent::encode_assignable_target( @@ -190,8 +194,9 @@ void dfcc_contract_clauses_codegent::encode_freeable_target_group( // clean up side effects from the condition expression if needed cleanert cleaner(goto_model.symbol_table, log.get_message_handler()); exprt condition(group.condition()); + std::list new_vars; if(has_subexpr(condition, ID_side_effect)) - cleaner.clean(condition, dest, language_mode); + new_vars = cleaner.clean(condition, dest, language_mode); // Jump target if condition is false auto goto_instruction = dest.add( @@ -202,6 +207,8 @@ void dfcc_contract_clauses_codegent::encode_freeable_target_group( auto label_instruction = dest.add(goto_programt::make_skip(source_location)); goto_instruction->complete_goto(label_instruction); + + destruct_locals(new_vars, dest, ns); } void dfcc_contract_clauses_codegent::encode_freeable_target( diff --git a/src/goto-instrument/contracts/instrument_spec_assigns.cpp b/src/goto-instrument/contracts/instrument_spec_assigns.cpp index 5f975e4cbb7..fc273e46259 100644 --- a/src/goto-instrument/contracts/instrument_spec_assigns.cpp +++ b/src/goto-instrument/contracts/instrument_spec_assigns.cpp @@ -23,6 +23,7 @@ Date: January 2022 #include #include +#include #include #include "cfg_info.h" @@ -419,8 +420,9 @@ void instrument_spec_assignst::track_spec_target_group( // clean up side effects from the guard expression if needed cleanert cleaner(st, log.get_message_handler()); exprt condition(group.condition()); + std::list new_vars; if(has_subexpr(condition, ID_side_effect)) - cleaner.clean(condition, dest, mode); + new_vars = cleaner.clean(condition, dest, mode); // create conditional address ranges by distributing the condition for(const auto &target : group.targets()) @@ -434,6 +436,8 @@ void instrument_spec_assignst::track_spec_target_group( // generate snapshot instructions for this target. create_snapshot(car, dest); } + + destruct_locals(new_vars, dest, ns); } void instrument_spec_assignst::track_plain_spec_target( diff --git a/src/goto-instrument/contracts/utils.h b/src/goto-instrument/contracts/utils.h index 0dd802bab18..b6e859c1fdc 100644 --- a/src/goto-instrument/contracts/utils.h +++ b/src/goto-instrument/contracts/utils.h @@ -43,9 +43,12 @@ class cleanert : public goto_convertt { } - void clean(exprt &guard, goto_programt &dest, const irep_idt &mode) + [[nodiscard]] std::list + clean(exprt &guard, goto_programt &dest, const irep_idt &mode) { - goto_convertt::clean_expr(guard, dest, mode, true); + auto clean_result = goto_convertt::clean_expr(guard, mode, true); + dest.destructive_append(clean_result.side_effects); + return clean_result.temporaries; } void do_havoc_slice(