diff --git a/jbmc/regression/jbmc/clinit-lifting2/test-goto-functions.desc b/jbmc/regression/jbmc/clinit-lifting2/test-goto-functions.desc index f9d8e26f17a..5359377052e 100644 --- a/jbmc/regression/jbmc/clinit-lifting2/test-goto-functions.desc +++ b/jbmc/regression/jbmc/clinit-lifting2/test-goto-functions.desc @@ -4,7 +4,7 @@ Test activate-multi-line-match ^EXIT=0$ ^SIGNAL=0$ -\s*// 0 no location\n\s*CALL java::Other\.\(\)\s*// 1 no location\s*DECL .*::total +\s*// 26 no location\n\s*CALL java::Other\.\(\)\s*// 27 no location\s*DECL .*::total -- -- This checks that the clinit-wrapper function is called once, even though there are two calls in the source diff --git a/jbmc/regression/jbmc/clinit-lifting3/test-goto-functions.desc b/jbmc/regression/jbmc/clinit-lifting3/test-goto-functions.desc index f3c4410882b..8af9ab4bf47 100644 --- a/jbmc/regression/jbmc/clinit-lifting3/test-goto-functions.desc +++ b/jbmc/regression/jbmc/clinit-lifting3/test-goto-functions.desc @@ -4,7 +4,7 @@ Test activate-multi-line-match ^EXIT=0$ ^SIGNAL=0$ -\s*// 0 no location\n\s*CALL java::Other\.\(\)\s*// 1 no location\s*CALL java::Third\.\(\)\s*// 2 no location\s*DECL .*::total +\s*// 28 no location\n\s*CALL java::Other\.\(\)\s*// 29 no location\s*CALL java::Third\.\(\)\s*// 30 no location\s*DECL .*::total -- -- This checks that the clinit-wrapper function is called once, even though there are two calls in the source diff --git a/regression/cbmc/deterministic-smt-output/main.c b/regression/cbmc/deterministic-smt-output/main.c new file mode 100644 index 00000000000..a621d3a95e8 --- /dev/null +++ b/regression/cbmc/deterministic-smt-output/main.c @@ -0,0 +1,10 @@ +#include + +int main() +{ + int x; + int y; + int z = x + y; + assert(z == x + y); + return 0; +} diff --git a/regression/cbmc/deterministic-smt-output/test.desc b/regression/cbmc/deterministic-smt-output/test.desc new file mode 100644 index 00000000000..83337a751f0 --- /dev/null +++ b/regression/cbmc/deterministic-smt-output/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--smt2 --outfile - +activate-multi-line-match +\(declare-fun \|main::1::x!0@1#1\| \(\) \(_ BitVec 32\)\)(?s:.)*\(declare-fun \|main::1::y!0@1#1\| \(\) \(_ BitVec 32\)\) +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +Tests that x is always declared before y, i.e., in lexicographic order. diff --git a/regression/cprover/function_calls/call_no_body1.desc b/regression/cprover/function_calls/call_no_body1.desc index dc99c1876ad..a2b2967037a 100644 --- a/regression/cprover/function_calls/call_no_body1.desc +++ b/regression/cprover/function_calls/call_no_body1.desc @@ -4,6 +4,6 @@ call_no_body1.c ^EXIT=0$ ^SIGNAL=0$ ^\*\*\*\* WARNING: no body for function function_without_body$ -^\(\d+\) ∀ ς : state, nondet::S18\.2-0 : signedbv\[32\] \. S18\.1\(ς\) ⇒ S18\.2\(ς\[❝main::\$tmp::return_value_function_without_body❞:=nondet::S18\.2-0\]\)$ -^\(\d+\) ∀ ς : state \. S18\.2\(ς\) ⇒ S18\.3\(ς\[❝main::1::x❞:=ς\(❝main::\$tmp::return_value_function_without_body❞\)\]\)$ +^\(\d+\) ∀ ς : state, nondet::S2\.14-0 : signedbv\[32\] \. S2\.13\(ς\) ⇒ S2\.14\(ς\[❝main::\$tmp::return_value_function_without_body❞:=nondet::S2\.14-0\]\)$ +^\(\d+\) ∀ ς : state \. S2\.14\(ς\) ⇒ S2\.15\(ς\[❝main::1::x❞:=ς\(❝main::\$tmp::return_value_function_without_body❞\)\]\)$ -- diff --git a/regression/cprover/function_calls/call_no_body2.desc b/regression/cprover/function_calls/call_no_body2.desc index 9615edec2f8..45571cb3249 100644 --- a/regression/cprover/function_calls/call_no_body2.desc +++ b/regression/cprover/function_calls/call_no_body2.desc @@ -3,5 +3,5 @@ call_no_body2.c --text ^EXIT=0$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state, nondet::S18\.2-0 : signedbv\[32\] \. S18\.1\(ς\) ⇒ S18\.2\(ς\[❝main::\$tmp::return_value_function_without_body❞\.❝x❞:=nondet::S18\.2-0\]\)$ +^\(\d+\) ∀ ς : state, nondet::S2\.14-0 : signedbv\[32\] \. S2\.13\(ς\) ⇒ S2\.14\(ς\[❝main::\$tmp::return_value_function_without_body❞\.❝x❞:=nondet::S2\.14-0\]\)$ -- diff --git a/regression/goto-analyzer/branching-ge/test-always-constants.desc b/regression/goto-analyzer/branching-ge/test-always-constants.desc index 73167c183a9..1cf5f793ec0 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 @ \[23, 25\] -^main::1::p .* TOP @ \[3, 9, 18\] +^main::1::i .* TOP @ \[37, 39\] +^main::1::p .* TOP @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-ge/test-always-intervals.desc b/regression/goto-analyzer/branching-ge/test-always-intervals.desc index e35fdffedda..43357551fa6 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\] @ \[23\] -^main::1::p .* \[0, A\] @ \[3, 9, 18\] +^main::1::i .* \[5, 5\] @ \[37\] +^main::1::p .* \[0, A\] @ \[17, 23, 32\] -- 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 6fa9bae0c29..6117f6ae26f 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 @ \[23\] -^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\] +^main::1::i .* value-set-begin: 5 :value-set-end @ \[37\] +^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-ge/test-indeterminate-constants.desc b/regression/goto-analyzer/branching-ge/test-indeterminate-constants.desc index c23c3655f5f..2b973b66f9b 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 @ \[23, 25\] -^main::1::p .* TOP @ \[3, 9, 18\] +^main::1::i .* TOP @ \[37, 39\] +^main::1::p .* TOP @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-ge/test-indeterminate-intervals.desc b/regression/goto-analyzer/branching-ge/test-indeterminate-intervals.desc index 5313cd50951..34ecb33bd70 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\] @ \[23, 25\] -^main::1::p .* \[0, A\] @ \[3, 9, 18\] +^main::1::i .* \[FFFFFFFB, 5\] @ \[37, 39\] +^main::1::p .* \[0, A\] @ \[17, 23, 32\] -- 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 406cd930231..a73dee0319b 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 @ \[23, 25\] -^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\] +^main::1::i .* value-set-begin: 5, -5 :value-set-end @ \[37, 39\] +^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-ge/test-never-constants.desc b/regression/goto-analyzer/branching-ge/test-never-constants.desc index 2d1d6df13a0..6636668ae53 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 @ \[23, 25\] -^main::1::p .* TOP @ \[3, 9, 18\] +^main::1::i .* TOP @ \[37, 39\] +^main::1::p .* TOP @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-ge/test-never-intervals.desc b/regression/goto-analyzer/branching-ge/test-never-intervals.desc index 9c31600de4f..0547e50930f 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\] @ \[25\] -^main::1::p .* \[0, A\] @ \[3, 9, 18\] +^main::1::i .* \[FFFFFFFB, FFFFFFFB\] @ \[39\] +^main::1::p .* \[0, A\] @ \[17, 23, 32\] -- 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 f8f2a0aa278..b6ad4fe65f7 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 @ \[25\] -^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\] +^main::1::i .* value-set-begin: -5 :value-set-end @ \[39\] +^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-gt/test-always-constants.desc b/regression/goto-analyzer/branching-gt/test-always-constants.desc index 73167c183a9..1cf5f793ec0 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 @ \[23, 25\] -^main::1::p .* TOP @ \[3, 9, 18\] +^main::1::i .* TOP @ \[37, 39\] +^main::1::p .* TOP @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-gt/test-always-intervals.desc b/regression/goto-analyzer/branching-gt/test-always-intervals.desc index e35fdffedda..43357551fa6 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\] @ \[23\] -^main::1::p .* \[0, A\] @ \[3, 9, 18\] +^main::1::i .* \[5, 5\] @ \[37\] +^main::1::p .* \[0, A\] @ \[17, 23, 32\] -- 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 6fa9bae0c29..6117f6ae26f 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 @ \[23\] -^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\] +^main::1::i .* value-set-begin: 5 :value-set-end @ \[37\] +^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-gt/test-indeterminate-constants.desc b/regression/goto-analyzer/branching-gt/test-indeterminate-constants.desc index c23c3655f5f..2b973b66f9b 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 @ \[23, 25\] -^main::1::p .* TOP @ \[3, 9, 18\] +^main::1::i .* TOP @ \[37, 39\] +^main::1::p .* TOP @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-gt/test-indeterminate-intervals.desc b/regression/goto-analyzer/branching-gt/test-indeterminate-intervals.desc index 5313cd50951..34ecb33bd70 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\] @ \[23, 25\] -^main::1::p .* \[0, A\] @ \[3, 9, 18\] +^main::1::i .* \[FFFFFFFB, 5\] @ \[37, 39\] +^main::1::p .* \[0, A\] @ \[17, 23, 32\] -- 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 406cd930231..a73dee0319b 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 @ \[23, 25\] -^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\] +^main::1::i .* value-set-begin: 5, -5 :value-set-end @ \[37, 39\] +^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-gt/test-never-constants.desc b/regression/goto-analyzer/branching-gt/test-never-constants.desc index 2d1d6df13a0..6636668ae53 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 @ \[23, 25\] -^main::1::p .* TOP @ \[3, 9, 18\] +^main::1::i .* TOP @ \[37, 39\] +^main::1::p .* TOP @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-gt/test-never-intervals.desc b/regression/goto-analyzer/branching-gt/test-never-intervals.desc index 9c31600de4f..0547e50930f 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\] @ \[25\] -^main::1::p .* \[0, A\] @ \[3, 9, 18\] +^main::1::i .* \[FFFFFFFB, FFFFFFFB\] @ \[39\] +^main::1::p .* \[0, A\] @ \[17, 23, 32\] -- 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 f8f2a0aa278..b6ad4fe65f7 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 @ \[25\] -^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\] +^main::1::i .* value-set-begin: -5 :value-set-end @ \[39\] +^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-le/test-always-constants.desc b/regression/goto-analyzer/branching-le/test-always-constants.desc index 73167c183a9..1cf5f793ec0 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 @ \[23, 25\] -^main::1::p .* TOP @ \[3, 9, 18\] +^main::1::i .* TOP @ \[37, 39\] +^main::1::p .* TOP @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-le/test-always-intervals.desc b/regression/goto-analyzer/branching-le/test-always-intervals.desc index e35fdffedda..43357551fa6 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\] @ \[23\] -^main::1::p .* \[0, A\] @ \[3, 9, 18\] +^main::1::i .* \[5, 5\] @ \[37\] +^main::1::p .* \[0, A\] @ \[17, 23, 32\] -- 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 6fa9bae0c29..6117f6ae26f 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 @ \[23\] -^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\] +^main::1::i .* value-set-begin: 5 :value-set-end @ \[37\] +^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-le/test-indeterminate-constants.desc b/regression/goto-analyzer/branching-le/test-indeterminate-constants.desc index c23c3655f5f..2b973b66f9b 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 @ \[23, 25\] -^main::1::p .* TOP @ \[3, 9, 18\] +^main::1::i .* TOP @ \[37, 39\] +^main::1::p .* TOP @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-le/test-indeterminate-intervals.desc b/regression/goto-analyzer/branching-le/test-indeterminate-intervals.desc index 5313cd50951..34ecb33bd70 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\] @ \[23, 25\] -^main::1::p .* \[0, A\] @ \[3, 9, 18\] +^main::1::i .* \[FFFFFFFB, 5\] @ \[37, 39\] +^main::1::p .* \[0, A\] @ \[17, 23, 32\] -- 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 406cd930231..a73dee0319b 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 @ \[23, 25\] -^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\] +^main::1::i .* value-set-begin: 5, -5 :value-set-end @ \[37, 39\] +^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-le/test-never-constants.desc b/regression/goto-analyzer/branching-le/test-never-constants.desc index 2d1d6df13a0..6636668ae53 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 @ \[23, 25\] -^main::1::p .* TOP @ \[3, 9, 18\] +^main::1::i .* TOP @ \[37, 39\] +^main::1::p .* TOP @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-le/test-never-intervals.desc b/regression/goto-analyzer/branching-le/test-never-intervals.desc index 9c31600de4f..0547e50930f 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\] @ \[25\] -^main::1::p .* \[0, A\] @ \[3, 9, 18\] +^main::1::i .* \[FFFFFFFB, FFFFFFFB\] @ \[39\] +^main::1::p .* \[0, A\] @ \[17, 23, 32\] -- 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 f8f2a0aa278..b6ad4fe65f7 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 @ \[25\] -^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\] +^main::1::i .* value-set-begin: -5 :value-set-end @ \[39\] +^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-lt/test-always-constants.desc b/regression/goto-analyzer/branching-lt/test-always-constants.desc index 73167c183a9..1cf5f793ec0 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 @ \[23, 25\] -^main::1::p .* TOP @ \[3, 9, 18\] +^main::1::i .* TOP @ \[37, 39\] +^main::1::p .* TOP @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-lt/test-always-intervals.desc b/regression/goto-analyzer/branching-lt/test-always-intervals.desc index e35fdffedda..43357551fa6 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\] @ \[23\] -^main::1::p .* \[0, A\] @ \[3, 9, 18\] +^main::1::i .* \[5, 5\] @ \[37\] +^main::1::p .* \[0, A\] @ \[17, 23, 32\] -- 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 6fa9bae0c29..6117f6ae26f 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 @ \[23\] -^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\] +^main::1::i .* value-set-begin: 5 :value-set-end @ \[37\] +^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-lt/test-indeterminate-constants.desc b/regression/goto-analyzer/branching-lt/test-indeterminate-constants.desc index c23c3655f5f..2b973b66f9b 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 @ \[23, 25\] -^main::1::p .* TOP @ \[3, 9, 18\] +^main::1::i .* TOP @ \[37, 39\] +^main::1::p .* TOP @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-lt/test-indeterminate-intervals.desc b/regression/goto-analyzer/branching-lt/test-indeterminate-intervals.desc index 5313cd50951..34ecb33bd70 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\] @ \[23, 25\] -^main::1::p .* \[0, A\] @ \[3, 9, 18\] +^main::1::i .* \[FFFFFFFB, 5\] @ \[37, 39\] +^main::1::p .* \[0, A\] @ \[17, 23, 32\] -- 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 406cd930231..a73dee0319b 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 @ \[23, 25\] -^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\] +^main::1::i .* value-set-begin: 5, -5 :value-set-end @ \[37, 39\] +^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-lt/test-never-constants.desc b/regression/goto-analyzer/branching-lt/test-never-constants.desc index 2d1d6df13a0..6636668ae53 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 @ \[23, 25\] -^main::1::p .* TOP @ \[3, 9, 18\] +^main::1::i .* TOP @ \[37, 39\] +^main::1::p .* TOP @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/branching-lt/test-never-intervals.desc b/regression/goto-analyzer/branching-lt/test-never-intervals.desc index 9c31600de4f..0547e50930f 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\] @ \[25\] -^main::1::p .* \[0, A\] @ \[3, 9, 18\] +^main::1::i .* \[FFFFFFFB, FFFFFFFB\] @ \[39\] +^main::1::p .* \[0, A\] @ \[17, 23, 32\] -- 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 f8f2a0aa278..b6ad4fe65f7 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 @ \[25\] -^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 9, 18\] +^main::1::i .* value-set-begin: -5 :value-set-end @ \[39\] +^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[17, 23, 32\] -- diff --git a/regression/goto-analyzer/liveness-array/test-liveness.desc b/regression/goto-analyzer/liveness-array/test-liveness.desc index 8c5d381893a..c356511fad2 100644 --- a/regression/goto-analyzer/liveness-array/test-liveness.desc +++ b/regression/goto-analyzer/liveness-array/test-liveness.desc @@ -3,7 +3,7 @@ main.c --no-standard-checks --variable-sensitivity --vsd-arrays every-element --vsd-values intervals --vsd-liveness --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::x .* TOP @ \[1\] -^main::1::x .* \{\[0\] = \[0, 0\] @ \[2\] -^main::1::x .* \{\[0\] = \[2, 3\] @ \[7\] +^main::1::x .* TOP @ \[15\] +^main::1::x .* \{\[0\] = \[0, 0\] @ \[16\] +^main::1::x .* \{\[0\] = \[2, 3\] @ \[21\] -- diff --git a/regression/goto-analyzer/liveness-array/test-write-location.desc b/regression/goto-analyzer/liveness-array/test-write-location.desc index 03a3569f0a5..eb67687fca6 100644 --- a/regression/goto-analyzer/liveness-array/test-write-location.desc +++ b/regression/goto-analyzer/liveness-array/test-write-location.desc @@ -3,7 +3,7 @@ main.c --no-standard-checks --variable-sensitivity --vsd-arrays every-element --vsd-values intervals --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::x .* TOP @ \[1\] -^main::1::x .* \{\[0\] = \[0, 0\] @ \[2\] -^main::1::x .* \{\[0\] = \[2, 3\] @ \[4, 6\] +^main::1::x .* TOP @ \[15\] +^main::1::x .* \{\[0\] = \[0, 0\] @ \[16\] +^main::1::x .* \{\[0\] = \[2, 3\] @ \[18, 20\] -- diff --git a/regression/goto-analyzer/liveness-function-call/test-liveness-show.desc b/regression/goto-analyzer/liveness-function-call/test-liveness-show.desc index c1501370247..3543c73dac6 100644 --- a/regression/goto-analyzer/liveness-function-call/test-liveness-show.desc +++ b/regression/goto-analyzer/liveness-function-call/test-liveness-show.desc @@ -3,8 +3,8 @@ main.c --variable-sensitivity --vsd-liveness --show ^EXIT=0$ ^SIGNAL=0$ -globalX .* 0 @ \[15\] -globalX .* 1 @ \[0\] -globalX .* 2 @ \[3\] -globalX .* TOP @ \[18\] +globalX .* 0 @ \[13\] +globalX .* 1 @ \[17\] +globalX .* 2 @ \[20\] +globalX .* TOP @ \[16\] -- diff --git a/regression/goto-analyzer/liveness-function-call/test-liveness-three-way-show.desc b/regression/goto-analyzer/liveness-function-call/test-liveness-three-way-show.desc index 2c13d44ae4b..dfb3fa6c91a 100644 --- a/regression/goto-analyzer/liveness-function-call/test-liveness-three-way-show.desc +++ b/regression/goto-analyzer/liveness-function-call/test-liveness-three-way-show.desc @@ -3,8 +3,8 @@ main.c --variable-sensitivity --vsd-liveness --three-way-merge --show ^EXIT=0$ ^SIGNAL=0$ -globalX .* 0 @ \[15\] -globalX .* 1 @ \[0\] -globalX .* 2 @ \[3\] -globalX .* TOP @ \[18\] +globalX .* 0 @ \[13\] +globalX .* 1 @ \[17\] +globalX .* 2 @ \[20\] +globalX .* TOP @ \[16\] -- diff --git a/regression/goto-analyzer/liveness-function-call/test-write-location-show.desc b/regression/goto-analyzer/liveness-function-call/test-write-location-show.desc index f3fd23e0665..2cb7e0cad8e 100644 --- a/regression/goto-analyzer/liveness-function-call/test-write-location-show.desc +++ b/regression/goto-analyzer/liveness-function-call/test-write-location-show.desc @@ -3,7 +3,7 @@ main.c --variable-sensitivity --show ^EXIT=0$ ^SIGNAL=0$ -globalX .* 0 @ \[15\] -globalX .* 1 @ \[0\] -globalX .* TOP @ \[0, 3\] +globalX .* 0 @ \[13\] +globalX .* 1 @ \[17\] +globalX .* TOP @ \[17, 20\] -- diff --git a/regression/goto-analyzer/liveness-function-call/test-write-location-three-way-show.desc b/regression/goto-analyzer/liveness-function-call/test-write-location-three-way-show.desc index 242a87dda34..ec74cea9f1a 100644 --- a/regression/goto-analyzer/liveness-function-call/test-write-location-three-way-show.desc +++ b/regression/goto-analyzer/liveness-function-call/test-write-location-three-way-show.desc @@ -3,7 +3,7 @@ main.c --variable-sensitivity --three-way-merge --show ^EXIT=0$ ^SIGNAL=0$ -globalX .* 0 @ \[15\] -globalX .* 1 @ \[0\] -globalX .* 2 @ \[3\] +globalX .* 0 @ \[13\] +globalX .* 1 @ \[17\] +globalX .* 2 @ \[20\] -- diff --git a/regression/goto-analyzer/liveness-loop/test-liveness.desc b/regression/goto-analyzer/liveness-loop/test-liveness.desc index b50010b61f9..53df8cce673 100644 --- a/regression/goto-analyzer/liveness-loop/test-liveness.desc +++ b/regression/goto-analyzer/liveness-loop/test-liveness.desc @@ -3,8 +3,8 @@ main.c --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --vsd-liveness --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::x .* TOP @ \[1\] -^main::1::x .* value-set-begin: 0 :value-set-end @ \[2\] -^main::1::x .* value-set-begin: 1, 2, 3, 4, 5 :value-set-end @ \[9\] -^main::1::x .* value-set-begin: 0, 1, 2, 3, 4, 5 :value-set-end @ \[5\] +^main::1::x .* TOP @ \[15\] +^main::1::x .* value-set-begin: 0 :value-set-end @ \[16\] +^main::1::x .* value-set-begin: 1, 2, 3, 4, 5 :value-set-end @ \[23\] +^main::1::x .* value-set-begin: 0, 1, 2, 3, 4, 5 :value-set-end @ \[19\] -- diff --git a/regression/goto-analyzer/liveness-loop/test-write-location.desc b/regression/goto-analyzer/liveness-loop/test-write-location.desc index cab664fd94b..d8a36a9bc7a 100644 --- a/regression/goto-analyzer/liveness-loop/test-write-location.desc +++ b/regression/goto-analyzer/liveness-loop/test-write-location.desc @@ -3,8 +3,8 @@ main.c --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::x .* TOP @ \[1\] -^main::1::x .* value-set-begin: 0 :value-set-end @ \[2\] -^main::1::x .* value-set-begin: 1, 2, 3, 4, 5 :value-set-end @ \[8\] -^main::1::x .* value-set-begin: 0, 1, 2, 3, 4, 5 :value-set-end @ \[2, 8\] +^main::1::x .* TOP @ \[15\] +^main::1::x .* value-set-begin: 0 :value-set-end @ \[16\] +^main::1::x .* value-set-begin: 1, 2, 3, 4, 5 :value-set-end @ \[22\] +^main::1::x .* value-set-begin: 0, 1, 2, 3, 4, 5 :value-set-end @ \[16, 22\] -- diff --git a/regression/goto-analyzer/liveness-pointer-write-through/test-liveness.desc b/regression/goto-analyzer/liveness-pointer-write-through/test-liveness.desc index ec4dcc87fb0..9c3b45e8d05 100644 --- a/regression/goto-analyzer/liveness-pointer-write-through/test-liveness.desc +++ b/regression/goto-analyzer/liveness-pointer-write-through/test-liveness.desc @@ -3,9 +3,9 @@ main.c --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --vsd-pointers constants --vsd-liveness --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::x .* TOP @ \[1\] -^main::1::x .* value-set-begin: 0 :value-set-end @ \[2\] -^main::1::x .* value-set-begin: 2, 3 :value-set-end @ \[9\] -^main::1::p .* TOP @ \[3\] -^main::1::p .*\(main::1::x\) @ \[4\] +^main::1::x .* TOP @ \[15\] +^main::1::x .* value-set-begin: 0 :value-set-end @ \[16\] +^main::1::x .* value-set-begin: 2, 3 :value-set-end @ \[23\] +^main::1::p .* TOP @ \[17\] +^main::1::p .*\(main::1::x\) @ \[18\] -- diff --git a/regression/goto-analyzer/liveness-pointer-write-through/test-write-location.desc b/regression/goto-analyzer/liveness-pointer-write-through/test-write-location.desc index 31c65e49a13..51bfdd976c3 100644 --- a/regression/goto-analyzer/liveness-pointer-write-through/test-write-location.desc +++ b/regression/goto-analyzer/liveness-pointer-write-through/test-write-location.desc @@ -3,9 +3,9 @@ main.c --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --vsd-pointers constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::x .* TOP @ \[1\] -^main::1::x .* value-set-begin: 0 :value-set-end @ \[2\] -^main::1::x .* value-set-begin: 2, 3 :value-set-end @ \[6, 8\] -^main::1::p .* TOP @ \[3\] -^main::1::p .*\(main::1::x\) @ \[4\] +^main::1::x .* TOP @ \[15\] +^main::1::x .* value-set-begin: 0 :value-set-end @ \[16\] +^main::1::x .* value-set-begin: 2, 3 :value-set-end @ \[20, 22\] +^main::1::p .* TOP @ \[17\] +^main::1::p .*\(main::1::x\) @ \[18\] -- diff --git a/regression/goto-analyzer/liveness-struct/test-liveness.desc b/regression/goto-analyzer/liveness-struct/test-liveness.desc index 79deb6fb562..0088b407a97 100644 --- a/regression/goto-analyzer/liveness-struct/test-liveness.desc +++ b/regression/goto-analyzer/liveness-struct/test-liveness.desc @@ -3,7 +3,7 @@ main.c --variable-sensitivity --vsd-structs every-field --vsd-values intervals --vsd-liveness --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::s .* \{\} @ \[1\] -^main::1::s .* \{.x=\[1, 1\] @ \[2\], .y=\[3, 3\] @ \[2\]\} @ \[2\] -^main::1::s .* \{.x=\[2, 3\] @ \[7\], .y=\[3, 3\] @ \[2\]\} @ \[7\] +^main::1::s .* \{\} @ \[15\] +^main::1::s .* \{.x=\[1, 1\] @ \[16\], .y=\[3, 3\] @ \[16\]\} @ \[16\] +^main::1::s .* \{.x=\[2, 3\] @ \[21\], .y=\[3, 3\] @ \[16\]\} @ \[21\] -- diff --git a/regression/goto-analyzer/liveness-struct/test-write-location.desc b/regression/goto-analyzer/liveness-struct/test-write-location.desc index 4341cf79a66..e624ee1fd59 100644 --- a/regression/goto-analyzer/liveness-struct/test-write-location.desc +++ b/regression/goto-analyzer/liveness-struct/test-write-location.desc @@ -3,7 +3,7 @@ main.c --variable-sensitivity --vsd-structs every-field --vsd-values intervals --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::s .* \{\} @ \[1\] -^main::1::s .* \{.x=\[1, 1\] @ \[2\], .y=\[3, 3\] @ \[2\]\} @ \[2\] -^main::1::s .* \{.x=\[2, 3\] @ \[4, 6\], .y=\[3, 3\] @ \[2\]\} @ \[4, 6\] +^main::1::s .* \{\} @ \[15\] +^main::1::s .* \{.x=\[1, 1\] @ \[16\], .y=\[3, 3\] @ \[16\]\} @ \[16\] +^main::1::s .* \{.x=\[2, 3\] @ \[18, 20\], .y=\[3, 3\] @ \[16\]\} @ \[18, 20\] -- diff --git a/regression/goto-analyzer/liveness/test-liveness.desc b/regression/goto-analyzer/liveness/test-liveness.desc index 116a242f851..453acaaf0d2 100644 --- a/regression/goto-analyzer/liveness/test-liveness.desc +++ b/regression/goto-analyzer/liveness/test-liveness.desc @@ -3,7 +3,7 @@ main.c --variable-sensitivity --vsd-values set-of-constants --vsd-liveness --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::x .* TOP @ \[1\] -^main::1::x .* value-set-begin: 0 :value-set-end @ \[2\] -^main::1::x .* value-set-begin: 2, 3 :value-set-end @ \[7\] +^main::1::x .* TOP @ \[15\] +^main::1::x .* value-set-begin: 0 :value-set-end @ \[16\] +^main::1::x .* value-set-begin: 2, 3 :value-set-end @ \[21\] -- diff --git a/regression/goto-analyzer/liveness/test-write-location.desc b/regression/goto-analyzer/liveness/test-write-location.desc index 9c4c2614cf6..da12efeab53 100644 --- a/regression/goto-analyzer/liveness/test-write-location.desc +++ b/regression/goto-analyzer/liveness/test-write-location.desc @@ -3,7 +3,7 @@ main.c --variable-sensitivity --vsd-values set-of-constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::x .* TOP @ \[1\] -^main::1::x .* value-set-begin: 0 :value-set-end @ \[2\] -^main::1::x .* value-set-begin: 2, 3 :value-set-end @ \[4, 6\] +^main::1::x .* TOP @ \[15\] +^main::1::x .* value-set-begin: 0 :value-set-end @ \[16\] +^main::1::x .* value-set-begin: 2, 3 :value-set-end @ \[18, 20\] -- diff --git a/regression/goto-analyzer/loop-termination-eq/test-constants.desc b/regression/goto-analyzer/loop-termination-eq/test-constants.desc index cd1436ce709..65f75a7ea6d 100644 --- a/regression/goto-analyzer/loop-termination-eq/test-constants.desc +++ b/regression/goto-analyzer/loop-termination-eq/test-constants.desc @@ -3,6 +3,6 @@ main.c --no-standard-checks --variable-sensitivity --vsd-values constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::1::i .* TOP @ \[3, 6\] -^main::1::p .* TOP @ \[1, 5\] +^main::1::1::i .* TOP @ \[17, 20\] +^main::1::p .* TOP @ \[15, 19\] -- diff --git a/regression/goto-analyzer/loop-termination-eq/test-intervals.desc b/regression/goto-analyzer/loop-termination-eq/test-intervals.desc index a9b65006620..dec8c221280 100644 --- a/regression/goto-analyzer/loop-termination-eq/test-intervals.desc +++ b/regression/goto-analyzer/loop-termination-eq/test-intervals.desc @@ -3,6 +3,6 @@ main.c --no-standard-checks --variable-sensitivity --vsd-values intervals --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::1::i .* \[0, 5\] @ \[3, 6\] -^main::1::p .* \[1, 20\] @ \[1, 5\] +^main::1::1::i .* \[0, 5\] @ \[17, 20\] +^main::1::p .* \[1, 20\] @ \[15, 19\] -- diff --git a/regression/goto-analyzer/loop-termination-eq/test-value-sets.desc b/regression/goto-analyzer/loop-termination-eq/test-value-sets.desc index 3a55e2428c3..61883081e16 100644 --- a/regression/goto-analyzer/loop-termination-eq/test-value-sets.desc +++ b/regression/goto-analyzer/loop-termination-eq/test-value-sets.desc @@ -3,6 +3,6 @@ main.c --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::1::i .* value-set-begin: 0, 1, 2, 3, 4, 5 :value-set-end @ \[3, 6\] -^main::1::p .* @ \[1, 5\] +^main::1::1::i .* value-set-begin: 0, 1, 2, 3, 4, 5 :value-set-end @ \[17, 20\] +^main::1::p .* @ \[15, 19\] -- diff --git a/regression/goto-analyzer/loop-termination-ne/test-constants.desc b/regression/goto-analyzer/loop-termination-ne/test-constants.desc index cd1436ce709..65f75a7ea6d 100644 --- a/regression/goto-analyzer/loop-termination-ne/test-constants.desc +++ b/regression/goto-analyzer/loop-termination-ne/test-constants.desc @@ -3,6 +3,6 @@ main.c --no-standard-checks --variable-sensitivity --vsd-values constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::1::i .* TOP @ \[3, 6\] -^main::1::p .* TOP @ \[1, 5\] +^main::1::1::i .* TOP @ \[17, 20\] +^main::1::p .* TOP @ \[15, 19\] -- diff --git a/regression/goto-analyzer/loop-termination-ne/test-intervals.desc b/regression/goto-analyzer/loop-termination-ne/test-intervals.desc index a9b65006620..dec8c221280 100644 --- a/regression/goto-analyzer/loop-termination-ne/test-intervals.desc +++ b/regression/goto-analyzer/loop-termination-ne/test-intervals.desc @@ -3,6 +3,6 @@ main.c --no-standard-checks --variable-sensitivity --vsd-values intervals --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::1::i .* \[0, 5\] @ \[3, 6\] -^main::1::p .* \[1, 20\] @ \[1, 5\] +^main::1::1::i .* \[0, 5\] @ \[17, 20\] +^main::1::p .* \[1, 20\] @ \[15, 19\] -- diff --git a/regression/goto-analyzer/loop-termination-ne/test-unwind-10-constants.desc b/regression/goto-analyzer/loop-termination-ne/test-unwind-10-constants.desc index b9cebc9217d..01fc39c1a50 100644 --- a/regression/goto-analyzer/loop-termination-ne/test-unwind-10-constants.desc +++ b/regression/goto-analyzer/loop-termination-ne/test-unwind-10-constants.desc @@ -3,6 +3,6 @@ main.c --no-standard-checks --variable-sensitivity --vsd-values constants --loop-unwind 10 --three-way-merge --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::1::i .* 5 @ \[6\] -^main::1::p .* 32 @ \[5\] +^main::1::1::i .* 5 @ \[20\] +^main::1::p .* 32 @ \[19\] -- diff --git a/regression/goto-analyzer/loop-termination-ne/test-unwind-10-intervals.desc b/regression/goto-analyzer/loop-termination-ne/test-unwind-10-intervals.desc index d8ad7291409..168380bf40a 100644 --- a/regression/goto-analyzer/loop-termination-ne/test-unwind-10-intervals.desc +++ b/regression/goto-analyzer/loop-termination-ne/test-unwind-10-intervals.desc @@ -3,6 +3,6 @@ main.c --no-standard-checks --variable-sensitivity --vsd-values intervals --loop-unwind 10 --three-way-merge --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::1::i .* \[5, 5\] @ \[6\] -^main::1::p .* \[20, 20\] @ \[5\] +^main::1::1::i .* \[5, 5\] @ \[20\] +^main::1::p .* \[20, 20\] @ \[19\] -- diff --git a/regression/goto-analyzer/loop-termination-ne/test-unwind-10-value-sets.desc b/regression/goto-analyzer/loop-termination-ne/test-unwind-10-value-sets.desc index c5f08aa4a9f..d323bda32ff 100644 --- a/regression/goto-analyzer/loop-termination-ne/test-unwind-10-value-sets.desc +++ b/regression/goto-analyzer/loop-termination-ne/test-unwind-10-value-sets.desc @@ -3,6 +3,6 @@ main.c --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --loop-unwind 10 --three-way-merge --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::1::i .* value-set-begin: 5 :value-set-end @ \[6\] -^main::1::p .* value-set-begin: 32 :value-set-end @ \[5\] +^main::1::1::i .* value-set-begin: 5 :value-set-end @ \[20\] +^main::1::p .* value-set-begin: 32 :value-set-end @ \[19\] -- diff --git a/regression/goto-analyzer/loop-termination-ne/test-unwind-5-constants.desc b/regression/goto-analyzer/loop-termination-ne/test-unwind-5-constants.desc index 139bc112faf..f44f0c5f14f 100644 --- a/regression/goto-analyzer/loop-termination-ne/test-unwind-5-constants.desc +++ b/regression/goto-analyzer/loop-termination-ne/test-unwind-5-constants.desc @@ -3,6 +3,6 @@ main.c --no-standard-checks --variable-sensitivity --vsd-values constants --loop-unwind 5 --three-way-merge --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::1::i .* TOP @ \[3, 6\] -^main::1::p .* TOP @ \[1, 5\] +^main::1::1::i .* TOP @ \[17, 20\] +^main::1::p .* TOP @ \[15, 19\] -- diff --git a/regression/goto-analyzer/loop-termination-ne/test-unwind-5-intervals.desc b/regression/goto-analyzer/loop-termination-ne/test-unwind-5-intervals.desc index 764b37add8b..819a482ca92 100644 --- a/regression/goto-analyzer/loop-termination-ne/test-unwind-5-intervals.desc +++ b/regression/goto-analyzer/loop-termination-ne/test-unwind-5-intervals.desc @@ -3,6 +3,6 @@ main.c --no-standard-checks --variable-sensitivity --vsd-values intervals --loop-unwind 5 --three-way-merge --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::1::i .* \[5, 5\] @ \[6\] -^main::1::p .* \[2, 1F9\] @ \[5\] +^main::1::1::i .* \[5, 5\] @ \[20\] +^main::1::p .* \[2, 1F9\] @ \[19\] -- diff --git a/regression/goto-analyzer/loop-termination-ne/test-unwind-5-value-sets.desc b/regression/goto-analyzer/loop-termination-ne/test-unwind-5-value-sets.desc index e21b91feec0..ebbbb404bfd 100644 --- a/regression/goto-analyzer/loop-termination-ne/test-unwind-5-value-sets.desc +++ b/regression/goto-analyzer/loop-termination-ne/test-unwind-5-value-sets.desc @@ -3,6 +3,6 @@ main.c --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --loop-unwind 5 --three-way-merge --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::1::i .* value-set-begin: 5 :value-set-end @ \[6\] -^main::1::p .* value-set-begin: 2, \[11, 21\], \[20, 1F9\] :value-set-end @ \[5\] +^main::1::1::i .* value-set-begin: 5 :value-set-end @ \[20\] +^main::1::p .* value-set-begin: 2, \[11, 21\], \[20, 1F9\] :value-set-end @ \[19\] -- diff --git a/regression/goto-analyzer/loop-termination-ne/test-value-sets.desc b/regression/goto-analyzer/loop-termination-ne/test-value-sets.desc index 3a55e2428c3..61883081e16 100644 --- a/regression/goto-analyzer/loop-termination-ne/test-value-sets.desc +++ b/regression/goto-analyzer/loop-termination-ne/test-value-sets.desc @@ -3,6 +3,6 @@ main.c --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show ^EXIT=0$ ^SIGNAL=0$ -^main::1::1::i .* value-set-begin: 0, 1, 2, 3, 4, 5 :value-set-end @ \[3, 6\] -^main::1::p .* @ \[1, 5\] +^main::1::1::i .* value-set-begin: 0, 1, 2, 3, 4, 5 :value-set-end @ \[17, 20\] +^main::1::p .* @ \[15, 19\] -- diff --git a/regression/goto-analyzer/sensitivity-last-written-locations-arrays/test.desc b/regression/goto-analyzer/sensitivity-last-written-locations-arrays/test.desc index 76ce8dc8e74..add83bfdbde 100644 --- a/regression/goto-analyzer/sensitivity-last-written-locations-arrays/test.desc +++ b/regression/goto-analyzer/sensitivity-last-written-locations-arrays/test.desc @@ -5,27 +5,27 @@ sensitivity_dependency_arrays.c activate-multi-line-match ^EXIT=0$ ^SIGNAL=0$ -main#return_value \(\) -> TOP @ \[1\] -__CPROVER_dead_object \(\) -> TOP @ \[4\] -__CPROVER_deallocated \(\) -> TOP @ \[5\] -__CPROVER_memory_leak \(\) -> TOP @ \[7\] -__CPROVER_rounding_mode \(\) -> 0 @ \[8\] -do_arrays::1::bool_ \(\) -> TOP @ \[10\] -do_arrays::1::bool_1 \(\) -> TOP @ \[11\] -do_arrays::1::bool_2 \(\) -> TOP @ \[12\] -do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[14\]\n\} @ \[14\] -do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[14\]\n\[1\] = 20 @ \[15\]\n\} @ \[15\] -do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[16\]\n\[1\] = 20 @ \[15\]\n\} @ \[16\] -do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[16\]\n\[1\] = 40 @ \[17\]\n\} @ \[17\] -do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[16\]\n\[1\] = 30 @ \[18\]\n\} @ \[18\] -do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[19\]\n\[1\] = 30 @ \[18\]\n\} @ \[19\] -do_arrays::1::x \(\) -> \{\[0\] = 5 @ \[20\]\n\[1\] = 30 @ \[18\]\n\} @ \[20\] -do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[21\]\n\[1\] = 30 @ \[18\]\n\} @ \[21\] -do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[21\]\n\[1\] = 10 @ \[22\]\n\} @ \[22\] -do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[24\]\n\[1\] = 10 @ \[22\]\n\} @ \[24\] -do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[24\, 26\]\n\[1\] = 10 @ \[22\]\n\} @ \[24\, 26\] -do_arrays::1::x \(\) -> \{\[0\] = 0 @ \[28]\n\[1\] = 10 @ \[22\]\n\} @ \[28\] -do_arrays::1::x \(\) -> \{\[0\] = 3 @ \[30]\n\[1\] = 10 @ \[22\]\n\} @ \[30\] -do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[30\, 32]\n\[1\] = 10 @ \[22\]\n\} @ \[30\, 32\] -do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[30\, 32\, 35]\n\[1\] = 10 @ \[37\]\n\} @ \[37\] -do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[38]\n\[1\] = 10 @ \[37\]\n\} @ \[38\] +main#return_value \(\) -> TOP @ \[49\] +__CPROVER_dead_object \(\) -> TOP @ \[8\] +__CPROVER_deallocated \(\) -> TOP @ \[9\] +__CPROVER_memory_leak \(\) -> TOP @ \[11\] +__CPROVER_rounding_mode \(\) -> 0 @ \[12\] +do_arrays::1::bool_ \(\) -> TOP @ \[14\] +do_arrays::1::bool_1 \(\) -> TOP @ \[15\] +do_arrays::1::bool_2 \(\) -> TOP @ \[16\] +do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[18\]\n\} @ \[18\] +do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[18\]\n\[1\] = 20 @ \[19\]\n\} @ \[19\] +do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[20\]\n\[1\] = 20 @ \[19\]\n\} @ \[20\] +do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[20\]\n\[1\] = 40 @ \[21\]\n\} @ \[21\] +do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[20\]\n\[1\] = 30 @ \[22\]\n\} @ \[22\] +do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[23\]\n\[1\] = 30 @ \[22\]\n\} @ \[23\] +do_arrays::1::x \(\) -> \{\[0\] = 5 @ \[24\]\n\[1\] = 30 @ \[22\]\n\} @ \[24\] +do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[25\]\n\[1\] = 30 @ \[22\]\n\} @ \[25\] +do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[25\]\n\[1\] = 10 @ \[26\]\n\} @ \[26\] +do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[28\]\n\[1\] = 10 @ \[26\]\n\} @ \[28\] +do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[28\, 30\]\n\[1\] = 10 @ \[26\]\n\} @ \[28\, 30\] +do_arrays::1::x \(\) -> \{\[0\] = 0 @ \[32]\n\[1\] = 10 @ \[26\]\n\} @ \[32\] +do_arrays::1::x \(\) -> \{\[0\] = 3 @ \[34]\n\[1\] = 10 @ \[26\]\n\} @ \[34\] +do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[34\, 36]\n\[1\] = 10 @ \[26\]\n\} @ \[34\, 36\] +do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[34\, 36\, 39]\n\[1\] = 10 @ \[41\]\n\} @ \[41\] +do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[42]\n\[1\] = 10 @ \[41\]\n\} @ \[42\] diff --git a/regression/goto-analyzer/sensitivity-last-written-locations-pointers/test.desc b/regression/goto-analyzer/sensitivity-last-written-locations-pointers/test.desc index a721884d5bc..76dee873c3a 100644 --- a/regression/goto-analyzer/sensitivity-last-written-locations-pointers/test.desc +++ b/regression/goto-analyzer/sensitivity-last-written-locations-pointers/test.desc @@ -5,26 +5,26 @@ sensitivity_dependency_pointers.c activate-multi-line-match ^EXIT=0$ ^SIGNAL=0$ -main#return_value \(\) -> TOP @ \[1\] -__CPROVER_dead_object \(\) -> TOP @ \[4\] -__CPROVER_deallocated \(\) -> TOP @ \[5\] -__CPROVER_memory_leak \(\) -> TOP @ \[7\] -__CPROVER_rounding_mode \(\) -> 0 @ \[8\] -do_pointers::1::bool_ \(\) -> TOP @ \[10\] -do_pointers::1::bool_1 \(\) -> TOP @ \[11\] -do_pointers::1::bool_2 \(\) -> TOP @ \[12\] -do_pointers::1::x \(\) -> TOP @ \[13\] -do_pointers::1::x \(\) -> 10 @ \[14\] -do_pointers::1::x_p \(\) -> TOP @ \[15\] -do_pointers::1::y \(\) -> TOP @ \[16\] -do_pointers::1::y \(\) -> 20 @ \[17\] -do_pointers::1::y_p \(\) -> TOP @ \[18\] -do_pointers::1::x_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[19\] -do_pointers::1::x \(\) -> 30 @ \[20\] -do_pointers::1::x \(\) -> 40 @ \[21\] -do_pointers::1::x \(\) -> TOP @ \[22\] -do_pointers::1::x \(\) -> 50 @ \[23\] -do_pointers::1::y_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[24\] -do_pointers::1::x \(\) -> 60 @ \[25\] -do_pointers::1::j \(\) -> TOP @ \[26\] -do_pointers::1::j \(\) -> 60 @ \[27\] +main#return_value \(\) -> TOP @ \[42\] +__CPROVER_dead_object \(\) -> TOP @ \[8\] +__CPROVER_deallocated \(\) -> TOP @ \[9\] +__CPROVER_memory_leak \(\) -> TOP @ \[11\] +__CPROVER_rounding_mode \(\) -> 0 @ \[12\] +do_pointers::1::bool_ \(\) -> TOP @ \[14\] +do_pointers::1::bool_1 \(\) -> TOP @ \[15\] +do_pointers::1::bool_2 \(\) -> TOP @ \[16\] +do_pointers::1::x \(\) -> TOP @ \[17\] +do_pointers::1::x \(\) -> 10 @ \[18\] +do_pointers::1::x_p \(\) -> TOP @ \[19\] +do_pointers::1::y \(\) -> TOP @ \[20\] +do_pointers::1::y \(\) -> 20 @ \[21\] +do_pointers::1::y_p \(\) -> TOP @ \[22\] +do_pointers::1::x_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[23\] +do_pointers::1::x \(\) -> 30 @ \[24\] +do_pointers::1::x \(\) -> 40 @ \[25\] +do_pointers::1::x \(\) -> TOP @ \[26\] +do_pointers::1::x \(\) -> 50 @ \[27\] +do_pointers::1::y_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[28\] +do_pointers::1::x \(\) -> 60 @ \[29\] +do_pointers::1::j \(\) -> TOP @ \[30\] +do_pointers::1::j \(\) -> 60 @ \[31\] diff --git a/regression/goto-analyzer/sensitivity-last-written-locations-structs/test.desc b/regression/goto-analyzer/sensitivity-last-written-locations-structs/test.desc index 6dbe225f070..2f466a90036 100644 --- a/regression/goto-analyzer/sensitivity-last-written-locations-structs/test.desc +++ b/regression/goto-analyzer/sensitivity-last-written-locations-structs/test.desc @@ -5,32 +5,32 @@ sensitivity_dependency_structs.c activate-multi-line-match ^EXIT=0$ ^SIGNAL=0$ -main#return_value \(\) -> TOP @ \[1\] -__CPROVER_dead_object \(\) -> TOP @ \[4\] -__CPROVER_deallocated \(\) -> TOP @ \[5\] -__CPROVER_memory_leak \(\) -> TOP @ \[7\] -__CPROVER_rounding_mode \(\) -> 0 @ \[8\] -do_structs::1::bool_ \(\) -> TOP @ \[10\] -do_structs::1::bool_1 \(\) -> TOP @ \[11\] -do_structs::1::bool_2 \(\) -> TOP @ \[12\] -do_structs::1::st \(\) -> \{\} @ \[13\] -do_structs::1::st \(\) -> \{.x=10 @ \[14\]\} @ \[14\] -do_structs::1::st \(\) -> \{.x=10 @ \[14\]\, .y=20 @ \[15\]\} @ \[15\] -do_structs::1::st \(\) -> \{.x=30 @ \[16\]\, .y=20 @ \[15\]\} @ \[16\] -do_structs::1::st \(\) -> \{.x=30 @ \[16\]\, .y=40 @ \[17\]\} @ \[17\] -do_structs::1::st \(\) -> \{.x=30 @ \[16\]\, .y=30 @ \[18\]\} @ \[18\] -do_structs::1::st \(\) -> \{.x=30 @ \[19\]\, .y=30 @ \[18\]\} @ \[19\] -do_structs::1::st \(\) -> \{.x=5 @ \[20\]\, .y=30 @ \[18\]\} @ \[20\] -do_structs::1::st \(\) -> \{.x=15 @ \[21\]\, .y=30 @ \[18\]\} @ \[21\] -do_structs::1::st \(\) -> \{.x=15 @ \[21\]\, .y=10 @ \[22\]\} @ \[22\] -do_structs::1::st \(\) -> \{.x=20 @ \[24\]\, .y=10 @ \[22\]\} @ \[24\] -do_structs::1::st \(\) -> \{.x=20 @ \[24\, 26\]\, .y=10 @ \[22\]\} @ \[24\, 26\] -do_structs::1::st \(\) -> \{.x=0 @ \[28\]\, .y=10 @ \[22\]\} @ \[28\] -do_structs::1::st \(\) -> \{.x=3 @ \[30\]\, .y=10 @ \[22\]\} @ \[30\] -do_structs::1::st \(\) -> \{.x=TOP @ \[30\, 32\]\, .y=10 @ \[22\]\} @ \[30\, 32\] -do_structs::1::st \(\) -> \{.x=TOP @ \[30\, 32\, 35\]\, .y=10 @ \[22\]\} @ \[30\, 32\, 35\] -do_structs::1::st \(\) -> \{.x=TOP @ \[30\, 32\, 35\]\, .y=10 @ \[37\]\} @ \[37\] -do_structs::1::st \(\) -> \{.x=20 @ \[38\]\, .y=10 @ \[37\]\} @ \[38\] -do_structs::1::new_age \(\) -> \{\} @ \[39\] -do_structs::1::new_age \(\) -> \{.x=20 @ \[40\]\, .y=10 @ \[40\]\} @ \[40\] +main#return_value \(\) -> TOP @ \[52\] +__CPROVER_dead_object \(\) -> TOP @ \[8\] +__CPROVER_deallocated \(\) -> TOP @ \[9\] +__CPROVER_memory_leak \(\) -> TOP @ \[11\] +__CPROVER_rounding_mode \(\) -> 0 @ \[12\] +do_structs::1::bool_ \(\) -> TOP @ \[14\] +do_structs::1::bool_1 \(\) -> TOP @ \[15\] +do_structs::1::bool_2 \(\) -> TOP @ \[16\] +do_structs::1::st \(\) -> \{\} @ \[17\] +do_structs::1::st \(\) -> \{.x=10 @ \[18\]\} @ \[18\] +do_structs::1::st \(\) -> \{.x=10 @ \[18\]\, .y=20 @ \[19\]\} @ \[19\] +do_structs::1::st \(\) -> \{.x=30 @ \[20\]\, .y=20 @ \[19\]\} @ \[20\] +do_structs::1::st \(\) -> \{.x=30 @ \[20\]\, .y=40 @ \[21\]\} @ \[21\] +do_structs::1::st \(\) -> \{.x=30 @ \[20\]\, .y=30 @ \[22\]\} @ \[22\] +do_structs::1::st \(\) -> \{.x=30 @ \[23\]\, .y=30 @ \[22\]\} @ \[23\] +do_structs::1::st \(\) -> \{.x=5 @ \[24\]\, .y=30 @ \[22\]\} @ \[24\] +do_structs::1::st \(\) -> \{.x=15 @ \[25\]\, .y=30 @ \[22\]\} @ \[25\] +do_structs::1::st \(\) -> \{.x=15 @ \[25\]\, .y=10 @ \[26\]\} @ \[26\] +do_structs::1::st \(\) -> \{.x=20 @ \[28\]\, .y=10 @ \[26\]\} @ \[28\] +do_structs::1::st \(\) -> \{.x=20 @ \[28\, 30\]\, .y=10 @ \[26\]\} @ \[28\, 30\] +do_structs::1::st \(\) -> \{.x=0 @ \[32\]\, .y=10 @ \[26\]\} @ \[32\] +do_structs::1::st \(\) -> \{.x=3 @ \[34\]\, .y=10 @ \[26\]\} @ \[34\] +do_structs::1::st \(\) -> \{.x=TOP @ \[34\, 36\]\, .y=10 @ \[26\]\} @ \[34\, 36\] +do_structs::1::st \(\) -> \{.x=TOP @ \[34\, 36\, 39\]\, .y=10 @ \[26\]\} @ \[34\, 36\, 39\] +do_structs::1::st \(\) -> \{.x=TOP @ \[34\, 36\, 39\]\, .y=10 @ \[41\]\} @ \[41\] +do_structs::1::st \(\) -> \{.x=20 @ \[42\]\, .y=10 @ \[41\]\} @ \[42\] +do_structs::1::new_age \(\) -> \{\} @ \[43\] +do_structs::1::new_age \(\) -> \{.x=20 @ \[44\]\, .y=10 @ \[44\]\} @ \[44\] -- diff --git a/regression/goto-analyzer/sensitivity-last-written-locations-variables/test.desc b/regression/goto-analyzer/sensitivity-last-written-locations-variables/test.desc index 4247d96b87e..52b0ea6107a 100644 --- a/regression/goto-analyzer/sensitivity-last-written-locations-variables/test.desc +++ b/regression/goto-analyzer/sensitivity-last-written-locations-variables/test.desc @@ -3,36 +3,36 @@ sensitivity_dependency_variables.c --no-standard-checks --variable-sensitivity --vsd-arrays every-element --vsd-pointers constants --vsd-structs every-field --show ^EXIT=0$ ^SIGNAL=0$ -main#return_value \(\) -> TOP @ \[1\] -__CPROVER_dead_object \(\) -> TOP @ \[4\] -__CPROVER_deallocated \(\) -> TOP @ \[5\] -__CPROVER_memory_leak \(\) -> TOP @ \[7\] -__CPROVER_rounding_mode \(\) -> 0 @ \[8\] -global_x \(\) -> 0 @ \[9\] -do_variables::1::bool_ \(\) -> TOP @ \[11\] -do_variables::1::bool_1 \(\) -> TOP @ \[12\] -do_variables::1::bool_2 \(\) -> TOP @ \[13\] -global_x \(\) -> 5 @ \[14\] -do_variables::1::x \(\) -> TOP @ \[15\] -do_variables::1::x \(\) -> 10 @ \[16\] -do_variables::1::y \(\) -> TOP @ \[17\] -do_variables::1::y \(\) -> 20 @ \[18\] -do_variables::1::x \(\) -> 30 @ \[19\] -do_variables::1::y \(\) -> 40 @ \[20\] -do_variables::1::y \(\) -> 30 @ \[21\] -do_variables::1::x \(\) -> 30 @ \[22\] -do_variables::1::x \(\) -> 5 @ \[23\] -do_variables::1::x \(\) -> 15 @ \[24\] -do_variables::1::y \(\) -> 10 @ \[25\] -do_variables::1::x \(\) -> 20 @ \[27\] -do_variables::1::x \(\) -> 20 @ \[27\, 29\] -do_variables::1::x \(\) -> 50 @ \[31\] -do_variables::1::x \(\) -> 20 @ \[33\] -do_variables::1::x \(\) -> TOP @ \[33\, 35\] -do_variables::1::x \(\) -> 0 @ \[37\] -do_variables::1::x \(\) -> 3 @ \[39\] -do_variables::1::x \(\) -> TOP @ \[39\, 41\] -do_variables::1::x \(\) -> TOP @ \[39\, 41\, 44\] -do_variables::1::y \(\) -> 10 @ \[46\] -do_variables::1::x \(\) -> 20 @ \[47\] +main#return_value \(\) -> TOP @ \[59\] +__CPROVER_dead_object \(\) -> TOP @ \[8\] +__CPROVER_deallocated \(\) -> TOP @ \[9\] +__CPROVER_memory_leak \(\) -> TOP @ \[11\] +__CPROVER_rounding_mode \(\) -> 0 @ \[12\] +global_x \(\) -> 0 @ \[13\] +do_variables::1::bool_ \(\) -> TOP @ \[15\] +do_variables::1::bool_1 \(\) -> TOP @ \[16\] +do_variables::1::bool_2 \(\) -> TOP @ \[17\] +global_x \(\) -> 5 @ \[18\] +do_variables::1::x \(\) -> TOP @ \[19\] +do_variables::1::x \(\) -> 10 @ \[20\] +do_variables::1::y \(\) -> TOP @ \[21\] +do_variables::1::y \(\) -> 20 @ \[22\] +do_variables::1::x \(\) -> 30 @ \[23\] +do_variables::1::y \(\) -> 40 @ \[24\] +do_variables::1::y \(\) -> 30 @ \[25\] +do_variables::1::x \(\) -> 30 @ \[26\] +do_variables::1::x \(\) -> 5 @ \[27\] +do_variables::1::x \(\) -> 15 @ \[28\] +do_variables::1::y \(\) -> 10 @ \[29\] +do_variables::1::x \(\) -> 20 @ \[31\] +do_variables::1::x \(\) -> 20 @ \[31\, 33\] +do_variables::1::x \(\) -> 50 @ \[35\] +do_variables::1::x \(\) -> 20 @ \[37\] +do_variables::1::x \(\) -> TOP @ \[37\, 39\] +do_variables::1::x \(\) -> 0 @ \[41\] +do_variables::1::x \(\) -> 3 @ \[43\] +do_variables::1::x \(\) -> TOP @ \[43\, 45\] +do_variables::1::x \(\) -> TOP @ \[43\, 45\, 48\] +do_variables::1::y \(\) -> 10 @ \[50\] +do_variables::1::x \(\) -> 20 @ \[51\] -- diff --git a/regression/goto-analyzer/sensitivity-test-data-dependency-context/test.desc b/regression/goto-analyzer/sensitivity-test-data-dependency-context/test.desc index dbb5f0664f5..1b0cf764239 100644 --- a/regression/goto-analyzer/sensitivity-test-data-dependency-context/test.desc +++ b/regression/goto-analyzer/sensitivity-test-data-dependency-context/test.desc @@ -5,8 +5,8 @@ data-dependency-context.c activate-multi-line-match ^EXIT=0$ ^SIGNAL=0$ -st \(\) -> \{.a=.* @ \[2, 42\]\[Data dependencies: 42, 2\]\[Data dominators: \], .b=.* @ \[5, 42\]\[Data dependencies: 42, 5\]\[Data dominators: \]\} @ \[2, 5, 42\]\[Data dependencies: 42, 5, 2\]\[Data dominators: 42\] -ar \(\) -> \{\[0\] = TOP @ \[11\, 36\]\[Data dependencies: 36\, 11\]\[Data dominators: \]\n\[1\] = TOP @ \[14\, 36\]\[Data dependencies: 36\, 14\]\[Data dominators: \]\n\} @ \[11\, 14\, 36\]\[Data dependencies: 36\, 14\, 11\]\[Data dominators: 36\] -arr \(\) -> \{\[0\] = 1 @ \[19\]\[Data dependencies: 19\]\[Data dominators: 19\]\n\[1\] = 2 @ \[20\]\[Data dependencies: 20\]\[Data dominators: 20\]\n\[2\] = TOP @ \[21, 23\]\[Data dependencies: 23, 21\]\[Data dominators: \]\n\} @ \[21, 23\]\[Data dependencies: 23, 21\]\[Data dominators: 37\] +st \(\) -> \{.a=.* @ \[16, 20\]\[Data dependencies: 20, 16\]\[Data dominators: \], .b=.* @ \[16, 23\]\[Data dependencies: 23, 16\]\[Data dominators: \]\} @ \[16, 20, 23\]\[Data dependencies: 23, 20, 16\]\[Data dominators: 16\] +ar \(\) -> \{\[0\] = TOP @ \[10, 29\]\[Data dependencies: 29, 10\]\[Data dominators: \]\n\[1\] = TOP @ \[10, 32\]\[Data dependencies: 32, 10\]\[Data dominators: \]\n\} @ \[10, 29, 32]\[Data dependencies: 32, 29, 10]\[Data dominators: 10\] +arr \(\) -> \{\[0\] = 1 @ \[37\]\[Data dependencies: 37\]\[Data dominators: 37\]\n\[1\] = 2 @ \[38\]\[Data dependencies: 38\]\[Data dominators: 38\]\n\[2\] = TOP @ \[39, 41\]\[Data dependencies: 41, 39\]\[Data dominators: \]\n\} @ \[39, 41\]\[Data dependencies: 41, 39\]\[Data dominators: 11\] -- ^warning: ignoring diff --git a/regression/goto-analyzer/ternary-operator/test-constants.desc b/regression/goto-analyzer/ternary-operator/test-constants.desc index e1066c6b418..9b82ccbfe11 100644 --- a/regression/goto-analyzer/ternary-operator/test-constants.desc +++ b/regression/goto-analyzer/ternary-operator/test-constants.desc @@ -3,10 +3,10 @@ main.c --variable-sensitivity --vsd-values constants --show ^EXIT=0$ ^SIGNAL=0$ -main::1::b1 \(\) -> TRUE @ \[2\] -main::1::b2 \(\) -> FALSE @ \[3\] -main::1::b3 \(\) -> TOP @ \[5\] -main::1::i \(\) -> 10 @ \[7\] -main::1::j \(\) -> 20 @ \[9\] -main::1::k \(\) -> TOP @ \[11\] +main::1::b1 \(\) -> TRUE @ \[17\] +main::1::b2 \(\) -> FALSE @ \[18\] +main::1::b3 \(\) -> TOP @ \[20\] +main::1::i \(\) -> 10 @ \[22\] +main::1::j \(\) -> 20 @ \[24\] +main::1::k \(\) -> TOP @ \[26\] -- diff --git a/regression/goto-analyzer/ternary-operator/test-intervals.desc b/regression/goto-analyzer/ternary-operator/test-intervals.desc index 03e52dd051d..e5fe50abe6d 100644 --- a/regression/goto-analyzer/ternary-operator/test-intervals.desc +++ b/regression/goto-analyzer/ternary-operator/test-intervals.desc @@ -3,10 +3,10 @@ main.c --variable-sensitivity --vsd-values intervals --show ^EXIT=0$ ^SIGNAL=0$ -main::1::b1 \(\) -> \[1, 1\] @ \[2\] -main::1::b2 \(\) -> \[0, 0\] @ \[3\] -main::1::b3 \(\) -> TOP @ \[5\] -main::1::i \(\) -> \[A, A\] @ \[7\] -main::1::j \(\) -> \[14, 14\] @ \[9\] -main::1::k \(\) -> \[A, 14\] @ \[11\] +main::1::b1 \(\) -> \[1, 1\] @ \[17\] +main::1::b2 \(\) -> \[0, 0\] @ \[18\] +main::1::b3 \(\) -> TOP @ \[20\] +main::1::i \(\) -> \[A, A\] @ \[22\] +main::1::j \(\) -> \[14, 14\] @ \[24\] +main::1::k \(\) -> \[A, 14\] @ \[26\] -- diff --git a/regression/goto-analyzer/ternary-operator/test-value-sets.desc b/regression/goto-analyzer/ternary-operator/test-value-sets.desc index be593b76d7e..2befe2d6e77 100644 --- a/regression/goto-analyzer/ternary-operator/test-value-sets.desc +++ b/regression/goto-analyzer/ternary-operator/test-value-sets.desc @@ -5,7 +5,7 @@ main.c ^SIGNAL=0$ main::1::b1 \(\) -> value-set-begin: TRUE :value-set-end main::1::b2 \(\) -> value-set-begin: FALSE :value-set-end -main::1::b3 \(\) -> TOP @ \[5\] +main::1::b3 \(\) -> TOP @ \[20\] main::1::i \(\) -> value-set-begin: 10 :value-set-end main::1::j \(\) -> value-set-begin: 20 :value-set-end main::1::k \(\) -> value-set-begin: 10, 20 :value-set-end diff --git a/regression/goto-analyzer/value-set-compact-01/test.desc b/regression/goto-analyzer/value-set-compact-01/test.desc index b1b03936035..76629deaacf 100644 --- a/regression/goto-analyzer/value-set-compact-01/test.desc +++ b/regression/goto-analyzer/value-set-compact-01/test.desc @@ -3,7 +3,7 @@ main.c --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --show ^EXIT=0$ ^SIGNAL=0$ -main::1::a .* value-set-begin: 0, 1, 2, 3, 4, 5, 6 :value-set-end @ \[1, 12, 15, 18, 21, 24, 26\] -main::1::b .* value-set-begin: 20, 21, 22, 23, 24 :value-set-end @ \[3, 13, 16, 19, 22\] -main::1::c .* value-set-begin: 24, 25, 26, \[14, 17\], \[1B, 1E\] :value-set-end @ \[30\] +main::1::a .* value-set-begin: 0, 1, 2, 3, 4, 5, 6 :value-set-end @ \[16, 27, 30, 33, 36, 39, 41\] +main::1::b .* value-set-begin: 20, 21, 22, 23, 24 :value-set-end @ \[18, 28, 31, 34, 37\] +main::1::c .* value-set-begin: 24, 25, 26, \[14, 17\], \[1B, 1E\] :value-set-end @ \[45\] -- diff --git a/regression/goto-analyzer/value-set-compact-02/test.desc b/regression/goto-analyzer/value-set-compact-02/test.desc index c5100073360..e0c0827a1f7 100644 --- a/regression/goto-analyzer/value-set-compact-02/test.desc +++ b/regression/goto-analyzer/value-set-compact-02/test.desc @@ -3,5 +3,5 @@ main.c --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --vsd-arrays every-element --show ^EXIT=0$ ^SIGNAL=0$ -main::1::a .* value-set-begin: 4, 5, 6, 11, 12, \[0, 3\], \[7, A\] :value-set-end @ \[1, 16, 18, 20, 22, 24, 26, 28, 30, 32, 34, 36, 38\] +main::1::a .* value-set-begin: 4, 5, 6, 11, 12, \[0, 3\], \[7, A\] :value-set-end @ \[16, 31, 33, 35, 37, 39, 41, 43, 45, 47, 49, 51, 53\] -- diff --git a/regression/goto-analyzer/value-set-compact-03/test.desc b/regression/goto-analyzer/value-set-compact-03/test.desc index 64f922f90a4..b25b0d32b00 100644 --- a/regression/goto-analyzer/value-set-compact-03/test.desc +++ b/regression/goto-analyzer/value-set-compact-03/test.desc @@ -3,5 +3,5 @@ main.c --variable-sensitivity --vsd-values set-of-constants --vsd-structs every-field --show ^EXIT=0$ ^SIGNAL=0$ -main::1::a .* \{.a=value-set-begin: 4, 5, 6, 11, 12, \[0, 3\], \[7, A\] :value-set-end @ \[1, 16, 18, 20, 22, 24, 26, 28, 30, 32, 34, 36, 38\]\} .* +main::1::a .* \{.a=value-set-begin: 4, 5, 6, 11, 12, \[0, 3\], \[7, A\] :value-set-end @ \[16, 31, 33, 35, 37, 39, 41, 43, 45, 47, 49, 51, 53\]\} .* -- diff --git a/regression/goto-analyzer/value-set-function-pointers-structs/test.desc b/regression/goto-analyzer/value-set-function-pointers-structs/test.desc index 67de292e3c8..139377efe1a 100644 --- a/regression/goto-analyzer/value-set-function-pointers-structs/test.desc +++ b/regression/goto-analyzer/value-set-function-pointers-structs/test.desc @@ -5,7 +5,7 @@ main.c ^file main.c line 46 function main: replacing function pointer by 2 possible targets$ ^file main.c line 54 function main: replacing function pointer by 2 possible targets$ ^main::1::fun1 \(\) -> value-set-begin: ptr ->\(f\), ptr ->\(g\) :value-set-end -^main::1::s2 \(\) -> \{\.fptr=value-set-begin: ptr ->\(f\), ptr ->\(g\) :value-set-end @ \[29, 31\]} @ \[29, 31\] +^main::1::s2 \(\) -> \{\.fptr=value-set-begin: ptr ->\(f\), ptr ->\(g\) :value-set-end @ \[49, 51\]} @ \[49, 51\] ^main::1::fun2 \(\) -> value-set-begin: ptr ->\(g\) :value-set-end ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-analyzer/value-set-structs/test_show.desc b/regression/goto-analyzer/value-set-structs/test_show.desc index 6af0a82da4b..4fa75995671 100644 --- a/regression/goto-analyzer/value-set-structs/test_show.desc +++ b/regression/goto-analyzer/value-set-structs/test_show.desc @@ -2,7 +2,7 @@ CORE main.c --no-standard-checks --variable-sensitivity --vsd-values set-of-constants --vsd-structs every-field --vsd-arrays every-element --vsd-pointers value-set --show --pointer-check activate-multi-line-match -main::1::s_show \(\) -> \{\.d=value-set-begin: 1\.0, 2\.0 :value-set-end @ \[16\], \.str=\{\[0\] = value-set-begin: 'x', 'y' :value-set-end @ \[16\]\n\[1\] = value-set-begin: '\\n' :value-set-end +main::1::s_show \(\) -> \{\.d=value-set-begin: 1\.0, 2\.0 :value-set-end @ \[30\], \.str=\{\[0\] = value-set-begin: 'x', 'y' :value-set-end @ \[30\]\n\[1\] = value-set-begin: '\\n' :value-set-end main::1::u_show \(\) -> \{\.d=value-set-begin: 1\.0, 2\.0, 3\.0 :value-set-end @ \[..\], \.str=\{\[0\] = value-set-begin: 'x', 'y', 'z' :value-set-end @ \[..\]\n\[1\] = value-set-begin: '\\n' :value-set-end @ \[..\]\n} @ \[..\]} @ \[..\] ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-constants-every-element.desc b/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-constants-every-element.desc index b2af6dc12d1..282c0eb459d 100644 --- a/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-constants-every-element.desc +++ b/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-constants-every-element.desc @@ -3,9 +3,9 @@ main.c --no-standard-checks --show --variable-sensitivity --vsd-values constants --vsd-arrays every-element ^EXIT=0$ ^SIGNAL=0$ -main::1::arr_at_ix \(\) -> TOP @ \[9\] -main::1::arr_0_after_write \(\) -> TOP @ \[18\] -main::1::arr_1_after_write \(\) -> TOP @ \[20\] -main::1::arr_2_after_write \(\) -> TOP @ \[22\] -main::1::arr_3_after_write \(\) -> TOP @ \[24\] -main::1::arr_4_after_write \(\) -> TOP @ \[26\] +main::1::arr_at_ix \(\) -> TOP @ \[23\] +main::1::arr_0_after_write \(\) -> TOP @ \[32\] +main::1::arr_1_after_write \(\) -> TOP @ \[34\] +main::1::arr_2_after_write \(\) -> TOP @ \[36\] +main::1::arr_3_after_write \(\) -> TOP @ \[38\] +main::1::arr_4_after_write \(\) -> TOP @ \[40\] diff --git a/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-constants-smash.desc b/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-constants-smash.desc index e3dad3c4c5b..055d7108600 100644 --- a/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-constants-smash.desc +++ b/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-constants-smash.desc @@ -3,7 +3,7 @@ main.c --no-standard-checks --show --variable-sensitivity --vsd-values constants --vsd-arrays smash ^EXIT=0$ ^SIGNAL=0$ -main::1::arr_at_ix \(\) -> TOP @ \[9\] +main::1::arr_at_ix \(\) -> TOP @ \[23\] main::1::arr_0_after_write \(\) -> TOP main::1::arr_1_after_write \(\) -> TOP main::1::arr_2_after_write \(\) -> TOP diff --git a/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-constants-up-to-3-elements.desc b/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-constants-up-to-3-elements.desc index 13608b5a3bb..0fb28b7339e 100644 --- a/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-constants-up-to-3-elements.desc +++ b/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-constants-up-to-3-elements.desc @@ -3,7 +3,7 @@ main.c --no-standard-checks --show --variable-sensitivity --vsd-values constants --vsd-arrays up-to-n-elements --vsd-array-max-elements 3 ^EXIT=0$ ^SIGNAL=0$ -main::1::arr_at_ix \(\) -> TOP @ \[9\] +main::1::arr_at_ix \(\) -> TOP @ \[23\] main::1::arr_0_after_write \(\) -> TOP main::1::arr_1_after_write \(\) -> TOP main::1::arr_2_after_write \(\) -> TOP diff --git a/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-intervals-every-element.desc b/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-intervals-every-element.desc index 546c92749d6..0d2e9979e50 100644 --- a/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-intervals-every-element.desc +++ b/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-intervals-every-element.desc @@ -3,9 +3,9 @@ main.c --no-standard-checks --show --variable-sensitivity --vsd-values intervals --vsd-arrays every-element ^EXIT=0$ ^SIGNAL=0$ -main::1::arr_at_ix \(\) -> \[1, 3\] @ \[9\] -main::1::arr_0_after_write \(\) -> \[1, 63\] @ \[18\] -main::1::arr_1_after_write \(\) -> \[2, 63\] @ \[20\] -main::1::arr_2_after_write \(\) -> \[3, 63\] @ \[22\] -main::1::arr_3_after_write \(\) -> \[4, 63\] @ \[24\] -main::1::arr_4_after_write \(\) -> \[5, 63\] @ \[26\] +main::1::arr_at_ix \(\) -> \[1, 3\] @ \[23\] +main::1::arr_0_after_write \(\) -> \[1, 63\] @ \[32\] +main::1::arr_1_after_write \(\) -> \[2, 63\] @ \[34\] +main::1::arr_2_after_write \(\) -> \[3, 63\] @ \[36\] +main::1::arr_3_after_write \(\) -> \[4, 63\] @ \[38\] +main::1::arr_4_after_write \(\) -> \[5, 63\] @ \[40\] diff --git a/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-intervals-smash.desc b/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-intervals-smash.desc index 229799ca354..5c04a453736 100644 --- a/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-intervals-smash.desc +++ b/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-intervals-smash.desc @@ -3,7 +3,7 @@ main.c --no-standard-checks --show --variable-sensitivity --vsd-values intervals --vsd-arrays smash ^EXIT=0$ ^SIGNAL=0$ -main::1::arr_at_ix \(\) -> \[1, 5\] @ \[9\] +main::1::arr_at_ix \(\) -> \[1, 5\] @ \[23\] main::1::arr_0_after_write \(\) -> \[1, 63\] main::1::arr_1_after_write \(\) -> \[1, 63\] main::1::arr_2_after_write \(\) -> \[1, 63\] diff --git a/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-intervals-up-to-3-elements.desc b/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-intervals-up-to-3-elements.desc index 3076e43a8eb..77a130481b7 100644 --- a/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-intervals-up-to-3-elements.desc +++ b/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-intervals-up-to-3-elements.desc @@ -3,7 +3,7 @@ main.c --no-standard-checks --show --variable-sensitivity --vsd-values intervals --vsd-arrays up-to-n-elements --vsd-array-max-elements 3 ^EXIT=0$ ^SIGNAL=0$ -main::1::arr_at_ix \(\) -> \[1, 5\] @ \[9\] +main::1::arr_at_ix \(\) -> \[1, 5\] @ \[23\] main::1::arr_0_after_write \(\) -> \[1, 63\] main::1::arr_1_after_write \(\) -> \[2, 63\] main::1::arr_2_after_write \(\) -> \[3, 63\] diff --git a/regression/goto-analyzer/variable-sensitivity-dependence-graph-simplified/test-eq.desc b/regression/goto-analyzer/variable-sensitivity-dependence-graph-simplified/test-eq.desc index 723c56de0f2..5f3509be976 100644 --- a/regression/goto-analyzer/variable-sensitivity-dependence-graph-simplified/test-eq.desc +++ b/regression/goto-analyzer/variable-sensitivity-dependence-graph-simplified/test-eq.desc @@ -3,8 +3,8 @@ main.c --dependence-graph-vs --show ^EXIT=0$ ^SIGNAL=0$ -^Data dependencies: 0 \[in\]$ -^Data dependencies: 2 \[a\]$ -^Data dependencies: 2 \[a\], 9 \[a\]$ +^Data dependencies: 14 \[in\]$ +^Data dependencies: 16 \[a\]$ +^Data dependencies: 16 \[a\], 23 \[a\]$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/variable-sensitivity-dependence-graph-simplified/test-gt.desc b/regression/goto-analyzer/variable-sensitivity-dependence-graph-simplified/test-gt.desc index 7eea9330446..a31862b882b 100644 --- a/regression/goto-analyzer/variable-sensitivity-dependence-graph-simplified/test-gt.desc +++ b/regression/goto-analyzer/variable-sensitivity-dependence-graph-simplified/test-gt.desc @@ -3,8 +3,8 @@ main.c --dependence-graph-vs --show -DINEQ ^EXIT=0$ ^SIGNAL=0$ -^Data dependencies: 0 \[in\]$ -^Data dependencies: 2 \[a\]$ -^Data dependencies: 2 \[a\], 9 \[a\]$ +^Data dependencies: 14 \[in\]$ +^Data dependencies: 16 \[a\]$ +^Data dependencies: 16 \[a\], 23 \[a\]$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/variable-sensitivity-dependence-graph-toyota/test.desc b/regression/goto-analyzer/variable-sensitivity-dependence-graph-toyota/test.desc index dbbefa74c2e..9ad3be927ed 100644 --- a/regression/goto-analyzer/variable-sensitivity-dependence-graph-toyota/test.desc +++ b/regression/goto-analyzer/variable-sensitivity-dependence-graph-toyota/test.desc @@ -3,24 +3,24 @@ main.c --no-standard-checks file1.c file2.c --dependence-graph-vs --vsd-structs every-field --vsd-arrays every-element --show ^EXIT=0$ ^SIGNAL=0$ -^Data dependencies: 48 \[st.a\]$ -^Data dependencies: 48 \[st.b\]$ -^Data dependencies: 1 \[st.a\], 48 \[st.a\]$ -^Data dependencies: 4 \[st.b\], 48 \[st.b\]$ -^Data dependencies: 1 \[st.a\], 4 \[st.b\], 48 \[st.a, st.b\]$ -^Data dependencies: 42 \[ar\[(\([^)]*\))?0\]\]$ -^Data dependencies: 42 \[ar\[(\([^)]*\))?1\]\]$ -^Data dependencies: 10 \[ar\[(\([^)]*\))?0\]\], 42 \[ar\[(\([^)]*\))?0\]\]$ -^Data dependencies: 13 \[ar\[(\([^)]*\))?1\]\], 42 \[ar\[(\([^)]*\))?1\]\]$ -^Data dependencies: 10 \[ar\[(\([^)]*\))?0\]\], 13 \[ar\[(\([^)]*\))?1\]\], 42 \[ar\[(\([^)]*\))?0\], ar\[(\([^)]*\))?1\]\]$ -^Data dependencies: 19 \[arr\[(\([^)]*\))?1\]\]$ -^Data dependencies: 18 \[arr\[(\([^)]*\))?0\]\]$ -^Data dependencies: 20 \[arr\[(\([^)]*\))?2\]\], 22 \[arr\[(\([^)]*\))?2\]\]$ -^Data dependencies: 1 \[st.a\], 48 \[st.a\], 52 \[st.a\]$ -^Data dependencies: 4 \[st.b\], 48 \[st.b\], 55 \[st.b\]$ -^Data dependencies: 1 \[st.a\], 4 \[st.b\], 48 \[st.a, st.b\], 52 \[st.a\], 55 \[st.b\]$ -^Data dependencies: 10 \[ar\[(\([^)]*\))?0\]\], 42 \[ar\[(\([^)]*\))?0\]\], 63 \[ar\[(\([^)]*\))?0\]\]$ -^Data dependencies: 13 \[ar\[(\([^)]*\))?1\]\], 42 \[ar\[(\([^)]*\))?1\]\], 66 \[ar\[(\([^)]*\))?1\]\]$ -^Data dependencies: 10 \[ar\[(\([^)]*\))?0\]\], 13 \[ar\[(\([^)]*\))?1\]\], 42 \[ar\[(\([^)]*\))?0\], ar\[(\([^)]*\))?1\]\], 63 \[ar\[(\([^)]*\))?0\]\], 66 \[ar\[(\([^)]*\))?1\]\]$ +^Data dependencies: 16 \[st.a\]$ +^Data dependencies: 16 \[st.b\]$ +^Data dependencies: 16 \[st.a\], 29 \[st.a\]$ +^Data dependencies: 16 \[st.b\], 32 \[st.b\]$ +^Data dependencies: 16 \[st.a, st.b\], 29 \[st.a\], 32 \[st.b\]$ +^Data dependencies: 10 \[ar\[(\([^)]*\))?0\]\]$ +^Data dependencies: 10 \[ar\[(\([^)]*\))?1\]\]$ +^Data dependencies: 10 \[ar\[(\([^)]*\))?0\]\], 38 \[ar\[(\([^)]*\))?0\]\]$ +^Data dependencies: 10 \[ar\[(\([^)]*\))?1\]\], 41 \[ar\[(\([^)]*\))?1\]\]$ +^Data dependencies: 10 \[ar\[(\([^)]*\))?0\], ar\[(\([^)]*\))?1\]\], 38 \[ar\[(\([^)]*\))?0\]\], 41 \[ar\[(\([^)]*\))?1\]\]$ +^Data dependencies: 47 \[arr\[(\([^)]*\))?1\]\]$ +^Data dependencies: 46 \[arr\[(\([^)]*\))?0\]\]$ +^Data dependencies: 48 \[arr\[(\([^)]*\))?2\]\], 50 \[arr\[(\([^)]*\))?2\]\]$ +^Data dependencies: 16 \[st.a\], 29 \[st.a\], 66 \[st.a\]$ +^Data dependencies: 16 \[st.b\], 32 \[st.b\], 69 \[st.b\]$ +^Data dependencies: 16 \[st.a, st.b\], 29 \[st.a\], 32 \[st.b\], 66 \[st.a\], 69 \[st.b\]$ +^Data dependencies: 10 \[ar\[(\([^)]*\))?0\]\], 19 \[ar\[(\([^)]*\))?0\]\], 38 \[ar\[(\([^)]*\))?0\]\]$ +^Data dependencies: 10 \[ar\[(\([^)]*\))?1\]\], 22 \[ar\[(\([^)]*\))?1\]\], 41 \[ar\[(\([^)]*\))?1\]\]$ +^Data dependencies: 10 \[ar\[(\([^)]*\))?0\], ar\[(\([^)]*\))?1\]\], 19 \[ar\[(\([^)]*\))?0\]\], 22 \[ar\[(\([^)]*\))?1\]\], 38 \[ar\[(\([^)]*\))?0\]\], 41 \[ar\[(\([^)]*\))?1\]\]$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/variable-sensitivity-dependence-graph/test.desc b/regression/goto-analyzer/variable-sensitivity-dependence-graph/test.desc index 25369297c5f..6ff74a15be4 100644 --- a/regression/goto-analyzer/variable-sensitivity-dependence-graph/test.desc +++ b/regression/goto-analyzer/variable-sensitivity-dependence-graph/test.desc @@ -3,25 +3,25 @@ main.c --no-standard-checks file1.c file2.c --dependence-graph-vs --vsd-structs every-field --vsd-arrays every-element --show ^EXIT=0$ ^SIGNAL=0$ -^Data dependencies: 48 \[st.a\]$ -^Data dependencies: 48 \[st.b\]$ -^Data dependencies: 1 \[st.a\], 48 \[st.a\]$ -^Data dependencies: 4 \[st.b\], 48 \[st.b\]$ -^Data dependencies: 1 \[st.a\], 4 \[st.b\], 48 \[st.a, st.b\]$ -^Data dependencies: 42 \[ar\[(\([^)]*\))?0\]\]$ -^Data dependencies: 6 \[out1\]$ -^Data dependencies: 42 \[ar\[(\([^)]*\))?1\]\]$ -^Data dependencies: 10 \[ar\[(\([^)]*\))?0\]\], 42 \[ar\[(\([^)]*\))?0\]\]$ -^Data dependencies: 13 \[ar\[(\([^)]*\))?1\]\], 42 \[ar\[(\([^)]*\))?1\]\]$ -^Data dependencies: 10 \[ar\[(\([^)]*\))?0\]\], 13 \[ar\[(\([^)]*\))?1\]\], 42 \[ar\[(\([^)]*\))?0\], ar\[(\([^)]*\))?1\]\]$ -^Data dependencies: 19 \[arr\[(\([^)]*\))?1\]\]$ -^Data dependencies: 18 \[arr\[(\([^)]*\))?0\]\]$ -^Data dependencies: 20 \[arr\[(\([^)]*\))?2\]\], 22 \[arr\[(\([^)]*\))?2\]\]$ -^Data dependencies: 1 \[st.a\], 48 \[st.a\], 52 \[st.a\]$ -^Data dependencies: 4 \[st.b\], 48 \[st.b\], 55 \[st.b\]$ -^Data dependencies: 1 \[st.a\], 4 \[st.b\], 48 \[st.a, st.b\], 52 \[st.a\], 55 \[st.b\]$ -^Data dependencies: 10 \[ar\[(\([^)]*\))?0\]\], 42 \[ar\[(\([^)]*\))?0\]\], 63 \[ar\[(\([^)]*\))?0\]\]$ -^Data dependencies: 13 \[ar\[(\([^)]*\))?1\]\], 42 \[ar\[(\([^)]*\))?1\]\], 66 \[ar\[(\([^)]*\))?1\]\]$ -^Data dependencies: 10 \[ar\[(\([^)]*\))?0\]\], 13 \[ar\[(\([^)]*\))?1\]\], 42 \[ar\[(\([^)]*\))?0\], ar\[(\([^)]*\))?1\]\], 63 \[ar\[(\([^)]*\))?0\]\], 66 \[ar\[(\([^)]*\))?1\]\]$ +^Data dependencies: 16 \[st.a\]$ +^Data dependencies: 16 \[st.b\]$ +^Data dependencies: 16 \[st.a\], 29 \[st.a\]$ +^Data dependencies: 16 \[st.b\], 32 \[st.b\]$ +^Data dependencies: 16 \[st.a, st.b\], 29 \[st.a\], 32 \[st.b\]$ +^Data dependencies: 10 \[ar\[(\([^)]*\))?0\]\]$ +^Data dependencies: 34 \[out1\]$ +^Data dependencies: 10 \[ar\[(\([^)]*\))?1\]\]$ +^Data dependencies: 10 \[ar\[(\([^)]*\))?0\]\], 38 \[ar\[(\([^)]*\))?0\]\]$ +^Data dependencies: 10 \[ar\[(\([^)]*\))?1\]\], 41 \[ar\[(\([^)]*\))?1\]\]$ +^Data dependencies: 10 \[ar\[(\([^)]*\))?0\], ar\[(\([^)]*\))?1\]\], 38 \[ar\[(\([^)]*\))?0\]\], 41 \[ar\[(\([^)]*\))?1\]\]$ +^Data dependencies: 47 \[arr\[(\([^)]*\))?1\]\]$ +^Data dependencies: 46 \[arr\[(\([^)]*\))?0\]\]$ +^Data dependencies: 48 \[arr\[(\([^)]*\))?2\]\], 50 \[arr\[(\([^)]*\))?2\]\]$ +^Data dependencies: 16 \[st.a\], 29 \[st.a\], 66 \[st.a\]$ +^Data dependencies: 16 \[st.b\], 32 \[st.b\], 69 \[st.b\]$ +^Data dependencies: 16 \[st.a, st.b\], 29 \[st.a\], 32 \[st.b\], 66 \[st.a\], 69 \[st.b\]$ +^Data dependencies: 10 \[ar\[(\([^)]*\))?0\]\], 19 \[ar\[(\([^)]*\))?0\]\], 38 \[ar\[(\([^)]*\))?0\]\]$ +^Data dependencies: 10 \[ar\[(\([^)]*\))?1\]\], 22 \[ar\[(\([^)]*\))?1\]\], 41 \[ar\[(\([^)]*\))?1\]\]$ +^Data dependencies: 10 \[ar\[(\([^)]*\))?0\], ar\[(\([^)]*\))?1\]\], 19 \[ar\[(\([^)]*\))?0\]\], 22 \[ar\[(\([^)]*\))?1\]\], 38 \[ar\[(\([^)]*\))?0\]\], 41 \[ar\[(\([^)]*\))?1\]\]$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/variable-sensitivity-dependence-graph16/test.desc b/regression/goto-analyzer/variable-sensitivity-dependence-graph16/test.desc index 1132fa4e2c1..969b8209866 100644 --- a/regression/goto-analyzer/variable-sensitivity-dependence-graph16/test.desc +++ b/regression/goto-analyzer/variable-sensitivity-dependence-graph16/test.desc @@ -6,5 +6,5 @@ activate-multi-line-match ^SIGNAL=0$ // Assignment from the result of a function call to a function with no body // should have a data dependency on the function -^Data dependencies: 3 \[f2\]\n(.*\n).*\/\/ 4 file .*main.c line 15 function main\n.*t2 := .*nondet.* +^Data dependencies: 18 \[f2\]\n(.*\n).*\/\/ 19 file .*main.c line 15 function main\n.*t2 := .*nondet.* -- diff --git a/regression/goto-analyzer/variable-sensitivity-dependence-graph17/test.desc b/regression/goto-analyzer/variable-sensitivity-dependence-graph17/test.desc index 0894cc0c9a5..a7244ea42d9 100644 --- a/regression/goto-analyzer/variable-sensitivity-dependence-graph17/test.desc +++ b/regression/goto-analyzer/variable-sensitivity-dependence-graph17/test.desc @@ -4,5 +4,5 @@ main.c activate-multi-line-match ^EXIT=0$ ^SIGNAL=0$ -\*\*\*\* 9 file .*main\.c line 22 function main\nControl dependencies: 24 \[UNCONDITIONAL\]\nData dependencies: 1 \[g_a\[(\([^)]*\))?i\]\], 2 \[g_a\[(\([^)]*\))?i\]\], 3 \[g_a\[(\([^)]*\))?i\]\], 7 \[g_a\[(\([^)]*\))?i\]\] +\*\*\*\* 23 file .*main\.c line 22 function main\nControl dependencies: 2 \[UNCONDITIONAL\]\nData dependencies: 15 \[g_a\[(\([^)]*\))?i\]\], 16 \[g_a\[(\([^)]*\))?i\]\], 17 \[g_a\[(\([^)]*\))?i\]\], 21 \[g_a\[(\([^)]*\))?i\]\] -- diff --git a/regression/goto-analyzer/variable-sensitivity-interval-values-arith-01/test.desc b/regression/goto-analyzer/variable-sensitivity-interval-values-arith-01/test.desc index 6c77e6b6ad1..cd3b92417a2 100644 --- a/regression/goto-analyzer/variable-sensitivity-interval-values-arith-01/test.desc +++ b/regression/goto-analyzer/variable-sensitivity-interval-values-arith-01/test.desc @@ -3,5 +3,5 @@ main.c --no-standard-checks --variable-sensitivity --vsd-values intervals --show ^EXIT=0$ ^SIGNAL=0$ -main::1::z \(\) -> \[3, 3\] @ \[5\] +main::1::z \(\) -> \[3, 3\] @ \[19\] -- diff --git a/regression/goto-analyzer/variable-sensitivity-interval-values-arith-02/test.desc b/regression/goto-analyzer/variable-sensitivity-interval-values-arith-02/test.desc index e9a42883da9..0251020135a 100644 --- a/regression/goto-analyzer/variable-sensitivity-interval-values-arith-02/test.desc +++ b/regression/goto-analyzer/variable-sensitivity-interval-values-arith-02/test.desc @@ -3,5 +3,5 @@ main.c --variable-sensitivity --vsd-values intervals --show ^EXIT=0$ ^SIGNAL=0$ -main::1::z \(\) -> \[3, 4\] @ \[9\] +main::1::z \(\) -> \[3, 4\] @ \[23\] -- diff --git a/regression/goto-analyzer/variable-sensitivity-interval-values-arith-03/test.desc b/regression/goto-analyzer/variable-sensitivity-interval-values-arith-03/test.desc index b72154af257..b43d9f59178 100644 --- a/regression/goto-analyzer/variable-sensitivity-interval-values-arith-03/test.desc +++ b/regression/goto-analyzer/variable-sensitivity-interval-values-arith-03/test.desc @@ -3,5 +3,5 @@ main.c --no-standard-checks --variable-sensitivity --vsd-values intervals --show ^EXIT=0$ ^SIGNAL=0$ -main::1::a \(\) -> \[6, 6\] @ \[7\] +main::1::a \(\) -> \[6, 6\] @ \[21\] -- diff --git a/regression/goto-analyzer/variable-sensitivity-interval-values-complex-structures/main.c b/regression/goto-analyzer/variable-sensitivity-interval-values-complex-structures/main.c index ab08a8125a1..602efb00786 100644 --- a/regression/goto-analyzer/variable-sensitivity-interval-values-complex-structures/main.c +++ b/regression/goto-analyzer/variable-sensitivity-interval-values-complex-structures/main.c @@ -1,6 +1,3 @@ -#include -#include - struct Vec2 { int x; diff --git a/regression/goto-analyzer/variable-sensitivity-interval-values-complex-structures/test.desc b/regression/goto-analyzer/variable-sensitivity-interval-values-complex-structures/test.desc index 3550f5d1dc2..9250bb41e2c 100644 --- a/regression/goto-analyzer/variable-sensitivity-interval-values-complex-structures/test.desc +++ b/regression/goto-analyzer/variable-sensitivity-interval-values-complex-structures/test.desc @@ -3,9 +3,9 @@ main.c --no-standard-checks --variable-sensitivity --vsd-values intervals --vsd-structs every-field --vsd-pointers constants --show ^EXIT=0$ ^SIGNAL=0$ -main::1::vecMinusTenAndTen \(\) -> \{.x=\[FFFFFFF6, FFFFFFF6\] \@ \[3\], .y=\[A, A\] \@ \[3\]\} @ \[3\] -main::1::1::vecZero \(\) -> \{.x=\[0, 0\] \@ \[8\], .y=\[0, 0\] \@ \[8\]\} \@ \[8\] -main::1::2::vecOne \(\) -> \{.x=\[1, 1\] \@ \[13\], .y=\[1, 1\] \@ \[13\]\} \@ \[13\] -main::1::vecZeroOrOne \(\) -> \{.x=\[0, 1\] \@ \[17\], .y=\[0, 1\] \@ \[17\]\} \@ \[17\] -main::1::vecThirteenAndFourtyTwo \(\) -> \{.x=\[D, D\] \@ \[21\], .y=\[2A, 2A\] \@ \[21\]\} \@ \[21\] +main::1::vecMinusTenAndTen \(\) -> \{.x=\[FFFFFFF6, FFFFFFF6\] \@ \[23\], .y=\[A, A\] \@ \[23\]\} @ \[23\] +main::1::1::vecZero \(\) -> \{.x=\[0, 0\] \@ \[28\], .y=\[0, 0\] \@ \[28\]\} \@ \[28\] +main::1::2::vecOne \(\) -> \{.x=\[1, 1\] \@ \[33\], .y=\[1, 1\] \@ \[33\]\} \@ \[33\] +main::1::vecZeroOrOne \(\) -> \{.x=\[0, 1\] \@ \[37\], .y=\[0, 1\] \@ \[37\]\} \@ \[37\] +main::1::vecThirteenAndFourtyTwo \(\) -> \{.x=\[D, D\] \@ \[41\], .y=\[2A, 2A\] \@ \[41\]\} \@ \[41\] -- diff --git a/regression/goto-analyzer/variable-sensitivity-interval-values-logical-01/test.desc b/regression/goto-analyzer/variable-sensitivity-interval-values-logical-01/test.desc index d57a6fc8571..db77d203e2d 100644 --- a/regression/goto-analyzer/variable-sensitivity-interval-values-logical-01/test.desc +++ b/regression/goto-analyzer/variable-sensitivity-interval-values-logical-01/test.desc @@ -3,7 +3,7 @@ main.c --variable-sensitivity --vsd-values intervals --show ^EXIT=0$ ^SIGNAL=0$ -main::1::b1 \(\) -> \[1, 1\] @ \[2\] -main::1::b2 \(\) -> \[0, 0\] @ \[3\] -main::1::i \(\) -> \[A\, 14\] @ \[11\] +main::1::b1 \(\) -> \[1, 1\] @ \[17\] +main::1::b2 \(\) -> \[0, 0\] @ \[18\] +main::1::i \(\) -> \[A\, 14\] @ \[26\] -- diff --git a/regression/goto-analyzer/variable-sensitivity-interval-values-multiplication-01/test.desc b/regression/goto-analyzer/variable-sensitivity-interval-values-multiplication-01/test.desc index 3698a50632e..3b1bf2db873 100644 --- a/regression/goto-analyzer/variable-sensitivity-interval-values-multiplication-01/test.desc +++ b/regression/goto-analyzer/variable-sensitivity-interval-values-multiplication-01/test.desc @@ -3,5 +3,5 @@ main.c --no-standard-checks --variable-sensitivity --vsd-values intervals --show ^EXIT=0$ ^SIGNAL=0$ -main::1::r \(\) -> TOP @ \[1\] -main::1::s \(\) -> \[0, 0\] @ \[3\] +main::1::r \(\) -> TOP @ \[13\] +main::1::s \(\) -> \[0, 0\] @ \[15\] diff --git a/regression/goto-analyzer/variable-sensitivity-interval-values-multiplication-02/test.desc b/regression/goto-analyzer/variable-sensitivity-interval-values-multiplication-02/test.desc index b648080c3a6..51673e04be8 100644 --- a/regression/goto-analyzer/variable-sensitivity-interval-values-multiplication-02/test.desc +++ b/regression/goto-analyzer/variable-sensitivity-interval-values-multiplication-02/test.desc @@ -3,9 +3,9 @@ main.c --no-standard-checks --variable-sensitivity --vsd-values intervals --show ^EXIT=0$ ^SIGNAL=0$ -main::1::r \(\) -> \[2, 2\] @ \[1\] -main::1::s \(\) -> \[3, 3\] @ \[3\] -main::1::t \(\) -> \[4, 4\] @ \[5\] -main::1::x \(\) -> \[9, 9\] @ \[7\] -main::1::y \(\) -> \[C, C\] @ \[9\] -main::1::z \(\) -> \[18, 18\] @ \[11\] +main::1::r \(\) -> \[2, 2\] @ \[12\] +main::1::s \(\) -> \[3, 3\] @ \[14\] +main::1::t \(\) -> \[4, 4\] @ \[16\] +main::1::x \(\) -> \[9, 9\] @ \[18\] +main::1::y \(\) -> \[C, C\] @ \[20\] +main::1::z \(\) -> \[18, 18\] @ \[22\] diff --git a/regression/goto-analyzer/variable-sensitivity-interval-values/test.desc b/regression/goto-analyzer/variable-sensitivity-interval-values/test.desc index 7fdf22da114..b4dcf5cd19d 100644 --- a/regression/goto-analyzer/variable-sensitivity-interval-values/test.desc +++ b/regression/goto-analyzer/variable-sensitivity-interval-values/test.desc @@ -3,9 +3,9 @@ main.c --no-standard-checks --variable-sensitivity --vsd-values intervals --show ^EXIT=0$ ^SIGNAL=0$ -main::1::zero \(\) -> \[0, 0\] @ \[3\] -main::1::1::one \(\) -> \[1, 1\] @ \[8\] -main::1::2::minus_one \(\) -> \[FFFFFFFF, FFFFFFFF\] @ \[13\] -main::1::between_minus_one_and_one \(\) -> \[FFFFFFFF, 1\] @ \[17\] -main::1::thirteen \(\) -> \[D, D\] @ \[20\] +main::1::zero \(\) -> \[0, 0\] @ \[17\] +main::1::1::one \(\) -> \[1, 1\] @ \[22\] +main::1::2::minus_one \(\) -> \[FFFFFFFF, FFFFFFFF\] @ \[27\] +main::1::between_minus_one_and_one \(\) -> \[FFFFFFFF, 1\] @ \[31\] +main::1::thirteen \(\) -> \[D, D\] @ \[34\] -- diff --git a/regression/goto-harness/havoc-global-int-01/test.desc b/regression/goto-harness/havoc-global-int-01/test.desc index 5f817b5fb71..4d773713b38 100644 --- a/regression/goto-harness/havoc-global-int-01/test.desc +++ b/regression/goto-harness/havoc-global-int-01/test.desc @@ -1,6 +1,6 @@ CORE main.c ---harness-type initialize-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:0 --havoc-variables x +--harness-type initialize-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:13 --havoc-variables x ^EXIT=10$ ^SIGNAL=0$ \[main.assertion.1\] line [0-9]+ assertion x == 1: FAILURE diff --git a/regression/goto-harness/havoc-global-int-02/test.desc b/regression/goto-harness/havoc-global-int-02/test.desc index fe3abf4614d..8665faa2ddc 100644 --- a/regression/goto-harness/havoc-global-int-02/test.desc +++ b/regression/goto-harness/havoc-global-int-02/test.desc @@ -1,6 +1,6 @@ CORE main.c -harness.gb --harness-type initialize-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-y-snapshot.json --initial-goto-location main:7 --havoc-variables y +harness.gb --harness-type initialize-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-y-snapshot.json --initial-goto-location main:70 --havoc-variables y ^\[main.assertion.1\] line \d+ assertion y \+ 2 > y: FAILURE$ ^\[main.assertion.2\] line \d+ assertion 0: FAILURE$ ^EXIT=10$ diff --git a/regression/goto-harness/havoc-global-struct/test.desc b/regression/goto-harness/havoc-global-struct/test.desc index acea3f2c367..bed2dded6de 100644 --- a/regression/goto-harness/havoc-global-struct/test.desc +++ b/regression/goto-harness/havoc-global-struct/test.desc @@ -1,6 +1,6 @@ CORE main.c -harness.gb --harness-type initialize-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-struct-snapshot.json --initial-goto-location main:3 --havoc-variables simple +harness.gb --harness-type initialize-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-struct-snapshot.json --initial-goto-location main:18 --havoc-variables simple ^EXIT=10$ ^SIGNAL=0$ ^\[main.assertion.1\] line \d+ assertion simple.j > simple.i: FAILURE$ diff --git a/regression/goto-harness/load-snapshot-recursive-static-global-int-01/test.desc b/regression/goto-harness/load-snapshot-recursive-static-global-int-01/test.desc index aabcd925525..af82f5acc82 100644 --- a/regression/goto-harness/load-snapshot-recursive-static-global-int-01/test.desc +++ b/regression/goto-harness/load-snapshot-recursive-static-global-int-01/test.desc @@ -1,6 +1,6 @@ CORE main.c -harness.gb --harness-type initialize-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:1 +harness.gb --harness-type initialize-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:15 ^EXIT=0$ ^SIGNAL=0$ VERIFICATION SUCCESSFUL diff --git a/regression/goto-harness/load-snapshot-static-global-array-01/test.desc b/regression/goto-harness/load-snapshot-static-global-array-01/test.desc index b9be03e032d..03ab6a5fcc2 100644 --- a/regression/goto-harness/load-snapshot-static-global-array-01/test.desc +++ b/regression/goto-harness/load-snapshot-static-global-array-01/test.desc @@ -1,6 +1,6 @@ CORE main.c -harness.gb --harness-type initialize-with-memory-snapshot --memory-snapshot snapshot.json --initial-goto-location main:0 +harness.gb --harness-type initialize-with-memory-snapshot --memory-snapshot snapshot.json --initial-goto-location main:13 ^EXIT=0$ ^SIGNAL=0$ VERIFICATION SUCCESSFUL diff --git a/regression/goto-harness/load-snapshot-static-global-int-01/test.desc b/regression/goto-harness/load-snapshot-static-global-int-01/test.desc index cbfab21c496..8b7ec7ceb12 100644 --- a/regression/goto-harness/load-snapshot-static-global-int-01/test.desc +++ b/regression/goto-harness/load-snapshot-static-global-int-01/test.desc @@ -1,6 +1,6 @@ CORE main.c -harness.gb --harness-type initialize-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:0 +harness.gb --harness-type initialize-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:13 ^EXIT=0$ ^SIGNAL=0$ VERIFICATION SUCCESSFUL diff --git a/regression/goto-harness/load-snapshot-static-global-int-02/test.desc b/regression/goto-harness/load-snapshot-static-global-int-02/test.desc index 255126954dc..8ca8647dbf1 100644 --- a/regression/goto-harness/load-snapshot-static-global-int-02/test.desc +++ b/regression/goto-harness/load-snapshot-static-global-int-02/test.desc @@ -1,6 +1,6 @@ CORE main.c -harness.gb --harness-type initialize-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:0 +harness.gb --harness-type initialize-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:14 ^EXIT=10$ ^SIGNAL=0$ \[main.assertion.1\] line [0-9]+ assertion x == 1: SUCCESS diff --git a/regression/goto-harness/load-snapshot-static-global-int-03/test.desc b/regression/goto-harness/load-snapshot-static-global-int-03/test.desc index cbfab21c496..af82f5acc82 100644 --- a/regression/goto-harness/load-snapshot-static-global-int-03/test.desc +++ b/regression/goto-harness/load-snapshot-static-global-int-03/test.desc @@ -1,6 +1,6 @@ CORE main.c -harness.gb --harness-type initialize-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:0 +harness.gb --harness-type initialize-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:15 ^EXIT=0$ ^SIGNAL=0$ VERIFICATION SUCCESSFUL diff --git a/regression/goto-harness/load-snapshot-static-global-int-04/test.desc b/regression/goto-harness/load-snapshot-static-global-int-04/test.desc index aabcd925525..de661b408a0 100644 --- a/regression/goto-harness/load-snapshot-static-global-int-04/test.desc +++ b/regression/goto-harness/load-snapshot-static-global-int-04/test.desc @@ -1,6 +1,6 @@ CORE main.c -harness.gb --harness-type initialize-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:1 +harness.gb --harness-type initialize-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:14 ^EXIT=0$ ^SIGNAL=0$ VERIFICATION SUCCESSFUL diff --git a/regression/goto-harness/load-snapshot-static-global-pointer-01/test.desc b/regression/goto-harness/load-snapshot-static-global-pointer-01/test.desc index db09a8df0fb..83b8203e471 100644 --- a/regression/goto-harness/load-snapshot-static-global-pointer-01/test.desc +++ b/regression/goto-harness/load-snapshot-static-global-pointer-01/test.desc @@ -1,6 +1,6 @@ CORE main.c -harness.gb --harness-type initialize-with-memory-snapshot --memory-snapshot snapshot.json --initial-goto-location main:0 _ --no-standard-checks +harness.gb --harness-type initialize-with-memory-snapshot --memory-snapshot snapshot.json --initial-goto-location main:14 _ --no-standard-checks ^EXIT=0$ ^SIGNAL=0$ VERIFICATION SUCCESSFUL diff --git a/regression/goto-instrument/ensure-one-backedge-per-target-do-while-loop/test.c b/regression/goto-instrument/ensure-one-backedge-per-target-do-while-loop/test.c index 4f09cb9f5a9..1271e86e789 100644 --- a/regression/goto-instrument/ensure-one-backedge-per-target-do-while-loop/test.c +++ b/regression/goto-instrument/ensure-one-backedge-per-target-do-while-loop/test.c @@ -1,4 +1,4 @@ -int main(int argc, char **argv) +int main() { int i = 0; do diff --git a/regression/goto-instrument/ensure-one-backedge-per-target-do-while-loop/with-transform.desc b/regression/goto-instrument/ensure-one-backedge-per-target-do-while-loop/with-transform.desc index 66901d97a73..171ee41aef1 100644 --- a/regression/goto-instrument/ensure-one-backedge-per-target-do-while-loop/with-transform.desc +++ b/regression/goto-instrument/ensure-one-backedge-per-target-do-while-loop/with-transform.desc @@ -1,6 +1,6 @@ CORE test.c --ensure-one-backedge-per-target --show-natural-loops -^2 is head of \{ 2, 3, 4, 5, 6, 7 \(backedge\) \}$ +^14 is head of \{ 14, 15, 16, 17, 18, 19 \(backedge\) \}$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/ensure-one-backedge-per-target-do-while-loop/without-transform.desc b/regression/goto-instrument/ensure-one-backedge-per-target-do-while-loop/without-transform.desc index 35461234741..709ed590b4e 100644 --- a/regression/goto-instrument/ensure-one-backedge-per-target-do-while-loop/without-transform.desc +++ b/regression/goto-instrument/ensure-one-backedge-per-target-do-while-loop/without-transform.desc @@ -1,6 +1,6 @@ CORE test.c --show-natural-loops -^2 is head of \{ 2, 3, 4, 5, 6, 7 \(backedge\) \}$ +^14 is head of \{ 14, 15, 16, 17, 18, 19 \(backedge\) \}$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/ensure-one-backedge-per-target-for-loop/test.c b/regression/goto-instrument/ensure-one-backedge-per-target-for-loop/test.c index 4650b9eb088..75bfa7d20a9 100644 --- a/regression/goto-instrument/ensure-one-backedge-per-target-for-loop/test.c +++ b/regression/goto-instrument/ensure-one-backedge-per-target-for-loop/test.c @@ -1,4 +1,4 @@ -int main(int argc, char **argv) +int main() { for(int i = 0; i < 10; ++i) { diff --git a/regression/goto-instrument/ensure-one-backedge-per-target-for-loop/with-transform.desc b/regression/goto-instrument/ensure-one-backedge-per-target-for-loop/with-transform.desc index 6a1ece48341..b3724408c07 100644 --- a/regression/goto-instrument/ensure-one-backedge-per-target-for-loop/with-transform.desc +++ b/regression/goto-instrument/ensure-one-backedge-per-target-for-loop/with-transform.desc @@ -1,6 +1,6 @@ CORE test.c --ensure-one-backedge-per-target --show-natural-loops -^2 is head of \{ 2, 3, 4, 5, 6, 7, 8, 9 \(backedge\) \}$ +^14 is head of \{ 14, 15, 16, 17, 18, 19, 20, 21 \(backedge\) \}$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/ensure-one-backedge-per-target-for-loop/without-transform.desc b/regression/goto-instrument/ensure-one-backedge-per-target-for-loop/without-transform.desc index 2e65bcfde15..d391b71b2fd 100644 --- a/regression/goto-instrument/ensure-one-backedge-per-target-for-loop/without-transform.desc +++ b/regression/goto-instrument/ensure-one-backedge-per-target-for-loop/without-transform.desc @@ -1,6 +1,6 @@ CORE test.c --show-natural-loops -^2 is head of \{ 2, 3, 4, 5, 6, 7, 8, 9 \(backedge\) \}$ +^14 is head of \{ 14, 15, 16, 17, 18, 19, 20, 21 \(backedge\) \}$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-multiple-loops/test.c b/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-multiple-loops/test.c index 317add397f5..15da3bcef76 100644 --- a/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-multiple-loops/test.c +++ b/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-multiple-loops/test.c @@ -1,4 +1,4 @@ -int main(int argc, char **argv) +int main() { int i = 0; top: diff --git a/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-multiple-loops/with-transform.desc b/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-multiple-loops/with-transform.desc index ed29c69fe63..9ddcaa4c5af 100644 --- a/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-multiple-loops/with-transform.desc +++ b/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-multiple-loops/with-transform.desc @@ -1,7 +1,7 @@ CORE test.c --ensure-one-backedge-per-target --show-natural-loops -^2 is head of \{ 2, 3, 4, 5, 6, 7, 8 \(backedge\) \} -^12 is head of \{ 12, 13, 14, 15, 16, 17, 18 \(backedge\) \} +^14 is head of \{ 14, 15, 16, 17, 18, 19, 20 \(backedge\) \} +^24 is head of \{ 24, 25, 26, 27, 28, 29, 30 \(backedge\) \} ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-multiple-loops/without-transform.desc b/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-multiple-loops/without-transform.desc index 2c0f0be7f8c..9fe26dbb479 100644 --- a/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-multiple-loops/without-transform.desc +++ b/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-multiple-loops/without-transform.desc @@ -1,7 +1,7 @@ CORE test.c --show-natural-loops -^2 is head of \{ 2, 3 \(backedge\), 4, 5, 6, 7 \(backedge\) \} -^11 is head of \{ 11, 12 \(backedge\), 13, 14, 15, 16 \(backedge\) \} +^14 is head of \{ 14, 15 \(backedge\), 16, 17, 18, 19 \(backedge\) \} +^23 is head of \{ 23, 24 \(backedge\), 25, 26, 27, 28 \(backedge\) \} ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-multiple/test.c b/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-multiple/test.c index 3351d7924f9..cf909c7aa2c 100644 --- a/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-multiple/test.c +++ b/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-multiple/test.c @@ -1,4 +1,4 @@ -int main(int argc, char **argv) +int main() { int i = 0; top: diff --git a/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-multiple/with-transform.desc b/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-multiple/with-transform.desc index 42c1a2014e2..f8e2f26be19 100644 --- a/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-multiple/with-transform.desc +++ b/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-multiple/with-transform.desc @@ -1,6 +1,6 @@ CORE test.c --ensure-one-backedge-per-target --show-natural-loops -^2 is head of \{ 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17 \(backedge\) \}$ +^14 is head of \{ 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29 \(backedge\) \}$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-multiple/without-transform.desc b/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-multiple/without-transform.desc index bda65fab1af..75c18d0c4d7 100644 --- a/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-multiple/without-transform.desc +++ b/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-multiple/without-transform.desc @@ -1,6 +1,6 @@ CORE test.c --show-natural-loops -^2 is head of \{ 2, 3 \(backedge\), 4, 5, 6 \(backedge\), 7, 8, 9 \(backedge\), 10, 11, 12 \(backedge\), 13, 14, 15, 16 \(backedge\) \}$ +^14 is head of \{ 14, 15 \(backedge\), 16, 17, 18 \(backedge\), 19, 20, 21 \(backedge\), 22, 23, 24 \(backedge\), 25, 26, 27, 28 \(backedge\) \}$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-unconditional/test.c b/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-unconditional/test.c index c789a6e7959..46daaca17a6 100644 --- a/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-unconditional/test.c +++ b/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-unconditional/test.c @@ -1,4 +1,4 @@ -int main(int argc, char **argv) +int main() { int i = 0; top: diff --git a/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-unconditional/with-transform.desc b/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-unconditional/with-transform.desc index a3b48510cc8..a69cd7fffdd 100644 --- a/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-unconditional/with-transform.desc +++ b/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-unconditional/with-transform.desc @@ -1,6 +1,6 @@ CORE test.c --ensure-one-backedge-per-target --show-natural-loops -^2 is head of \{ 2, 3, 4, 5, 6, 10, 11, 12 \(backedge\) \}$ +^14 is head of \{ 14, 15, 16, 17, 18, 22, 23, 24 \(backedge\) \}$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-unconditional/without-transform.desc b/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-unconditional/without-transform.desc index 7c5191bd44c..aa813b94a4c 100644 --- a/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-unconditional/without-transform.desc +++ b/regression/goto-instrument/ensure-one-backedge-per-target-goto-top-unconditional/without-transform.desc @@ -1,6 +1,6 @@ CORE test.c --show-natural-loops -^2 is head of \{ 2, 3 \(backedge\), 4, 5, 6, 10, 11, 12 \(backedge\) \}$ +^14 is head of \{ 14, 15 \(backedge\), 16, 17, 18, 22, 23, 24 \(backedge\) \}$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/ensure-one-backedge-per-target-goto-top/test.c b/regression/goto-instrument/ensure-one-backedge-per-target-goto-top/test.c index 0e261f47c6e..19a11836944 100644 --- a/regression/goto-instrument/ensure-one-backedge-per-target-goto-top/test.c +++ b/regression/goto-instrument/ensure-one-backedge-per-target-goto-top/test.c @@ -1,4 +1,4 @@ -int main(int argc, char **argv) +int main() { int i = 0; top: diff --git a/regression/goto-instrument/ensure-one-backedge-per-target-goto-top/with-transform.desc b/regression/goto-instrument/ensure-one-backedge-per-target-goto-top/with-transform.desc index 45ff24304fe..e41e7c63275 100644 --- a/regression/goto-instrument/ensure-one-backedge-per-target-goto-top/with-transform.desc +++ b/regression/goto-instrument/ensure-one-backedge-per-target-goto-top/with-transform.desc @@ -1,6 +1,6 @@ CORE test.c --ensure-one-backedge-per-target --show-natural-loops -^2 is head of \{ 2, 3, 4, 5, 6, 7, 8 \(backedge\) \}$ +^14 is head of \{ 14, 15, 16, 17, 18, 19, 20 \(backedge\) \}$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/ensure-one-backedge-per-target-goto-top/without-transform.desc b/regression/goto-instrument/ensure-one-backedge-per-target-goto-top/without-transform.desc index 43ded7de7dd..54bb29d40aa 100644 --- a/regression/goto-instrument/ensure-one-backedge-per-target-goto-top/without-transform.desc +++ b/regression/goto-instrument/ensure-one-backedge-per-target-goto-top/without-transform.desc @@ -1,6 +1,6 @@ CORE test.c --show-natural-loops -^2 is head of \{ 2, 3 \(backedge\), 4, 5, 6, 7 \(backedge\) \}$ +^14 is head of \{ 14, 15 \(backedge\), 16, 17, 18, 19 \(backedge\) \}$ ^EXIT=0$ ^SIGNAL=0$ 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 4df83b91759..61c85917287 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 @@ -1,7 +1,7 @@ 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\) \}$ -^17 is head of \{ 17, 18, 22, 23, 24, 25 \(backedge\) \}$ +^15 is head of \{ 15, 16, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38 \(backedge\) \}$ +^29 is head of \{ 29, 30, 34, 35, 36, 37 \(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 3c75bba4947..818f705f11e 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 -^17 is head of \{ 17, 18, 22, 23, 24, 25 \(backedge\) \}$ +^29 is head of \{ 29, 30, 34, 35, 36, 37 \(backedge\) \}$ Note not all loops were in lexical loop form ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/ensure-one-backedge-per-target-while-loop/test.c b/regression/goto-instrument/ensure-one-backedge-per-target-while-loop/test.c index 53e212b6d25..868704603a3 100644 --- a/regression/goto-instrument/ensure-one-backedge-per-target-while-loop/test.c +++ b/regression/goto-instrument/ensure-one-backedge-per-target-while-loop/test.c @@ -1,4 +1,4 @@ -int main(int argc, char **argv) +int main() { int i = 0; while(i < 10) diff --git a/regression/goto-instrument/ensure-one-backedge-per-target-while-loop/with-transform.desc b/regression/goto-instrument/ensure-one-backedge-per-target-while-loop/with-transform.desc index 45ff24304fe..e41e7c63275 100644 --- a/regression/goto-instrument/ensure-one-backedge-per-target-while-loop/with-transform.desc +++ b/regression/goto-instrument/ensure-one-backedge-per-target-while-loop/with-transform.desc @@ -1,6 +1,6 @@ CORE test.c --ensure-one-backedge-per-target --show-natural-loops -^2 is head of \{ 2, 3, 4, 5, 6, 7, 8 \(backedge\) \}$ +^14 is head of \{ 14, 15, 16, 17, 18, 19, 20 \(backedge\) \}$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/ensure-one-backedge-per-target-while-loop/without-transform.desc b/regression/goto-instrument/ensure-one-backedge-per-target-while-loop/without-transform.desc index 484ed113649..8605e4e0670 100644 --- a/regression/goto-instrument/ensure-one-backedge-per-target-while-loop/without-transform.desc +++ b/regression/goto-instrument/ensure-one-backedge-per-target-while-loop/without-transform.desc @@ -1,6 +1,6 @@ CORE test.c --show-natural-loops -^2 is head of \{ 2, 3, 4, 5, 6, 7, 8 \(backedge\) \}$ +^14 is head of \{ 14, 15, 16, 17, 18, 19, 20 \(backedge\) \}$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/lexical-loops1/test.c b/regression/goto-instrument/lexical-loops1/test.c index 9b775114782..0fd0838cfbb 100644 --- a/regression/goto-instrument/lexical-loops1/test.c +++ b/regression/goto-instrument/lexical-loops1/test.c @@ -1,10 +1,10 @@ - -int main(int argc, char **argv) +int main() { + int count; for(int i = 0; i < 10; ++i) { - ++argc; + ++count; } - return argc; + return count; } diff --git a/regression/goto-instrument/lexical-loops1/test.desc b/regression/goto-instrument/lexical-loops1/test.desc index 583dfadccd5..c92f53ec835 100644 --- a/regression/goto-instrument/lexical-loops1/test.desc +++ b/regression/goto-instrument/lexical-loops1/test.desc @@ -1,7 +1,7 @@ CORE test.c --show-lexical-loops _ --no-standard-checks -2 is head of \{ 2, 3, 4, 5 \(backedge\) \} +15 is head of \{ 15, 16, 17, 18 \(backedge\) \} ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-instrument/lexical-loops2/test.c b/regression/goto-instrument/lexical-loops2/test.c index ec4744ac62b..2bf3d08de6e 100644 --- a/regression/goto-instrument/lexical-loops2/test.c +++ b/regression/goto-instrument/lexical-loops2/test.c @@ -1,13 +1,14 @@ - -int main(int argc, char **argv) +int main() { int i = 0; + int count; + __CPROVER_assume(count > 10); while(i < 10) { ++i; - argc--; + count--; } - return argc; + return count; } diff --git a/regression/goto-instrument/lexical-loops2/test.desc b/regression/goto-instrument/lexical-loops2/test.desc index 17557991dc3..77fb1102f40 100644 --- a/regression/goto-instrument/lexical-loops2/test.desc +++ b/regression/goto-instrument/lexical-loops2/test.desc @@ -1,7 +1,7 @@ CORE test.c --show-lexical-loops -2 is head of \{ 2, 3, 4, 5 \(backedge\) \} +16 is head of \{ 16, 17, 18, 19 \(backedge\) \} ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-instrument/lexical-loops3/test.c b/regression/goto-instrument/lexical-loops3/test.c index 56cfe344e48..9c340cdddf7 100644 --- a/regression/goto-instrument/lexical-loops3/test.c +++ b/regression/goto-instrument/lexical-loops3/test.c @@ -1,13 +1,14 @@ - -int main(int argc, char **argv) +int main() { int i = 0; + int count; + __CPROVER_assume(count > 10); do { ++i; - argc--; + count--; } while(i < 10); - return argc; + return count; } diff --git a/regression/goto-instrument/lexical-loops3/test.desc b/regression/goto-instrument/lexical-loops3/test.desc index 424b8612b7e..94be50cd2c7 100644 --- a/regression/goto-instrument/lexical-loops3/test.desc +++ b/regression/goto-instrument/lexical-loops3/test.desc @@ -1,7 +1,7 @@ CORE test.c --show-lexical-loops -2 is head of \{ 2, 3, 4 \(backedge\) \} +16 is head of \{ 16, 17, 18 \(backedge\) \} ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-instrument/lexical-loops4/test.c b/regression/goto-instrument/lexical-loops4/test.c index 46299288377..820ce39a9b1 100644 --- a/regression/goto-instrument/lexical-loops4/test.c +++ b/regression/goto-instrument/lexical-loops4/test.c @@ -1,13 +1,14 @@ - -int main(int argc, char **argv) +int main() { int i = 0; + int count; + __CPROVER_assume(count > 10); head: ++i; - argc--; + count--; if(i < 10) goto head; - return argc; + return count; } diff --git a/regression/goto-instrument/lexical-loops4/test.desc b/regression/goto-instrument/lexical-loops4/test.desc index 424b8612b7e..94be50cd2c7 100644 --- a/regression/goto-instrument/lexical-loops4/test.desc +++ b/regression/goto-instrument/lexical-loops4/test.desc @@ -1,7 +1,7 @@ CORE test.c --show-lexical-loops -2 is head of \{ 2, 3, 4 \(backedge\) \} +16 is head of \{ 16, 17, 18 \(backedge\) \} ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-instrument/lexical-loops5/test.c b/regression/goto-instrument/lexical-loops5/test.c index f9bb65549e2..07af6f1f598 100644 --- a/regression/goto-instrument/lexical-loops5/test.c +++ b/regression/goto-instrument/lexical-loops5/test.c @@ -1,13 +1,14 @@ - -int main(int argc, char **argv) +int main() { + int count; + for(int i = 0; i < 5; ++i) { for(int j = 0; j < 5; ++j) { - argc++; + count++; } } - return argc; + return count; } diff --git a/regression/goto-instrument/lexical-loops5/test.desc b/regression/goto-instrument/lexical-loops5/test.desc index 8e2895aa5f1..dd3828d77ee 100644 --- a/regression/goto-instrument/lexical-loops5/test.desc +++ b/regression/goto-instrument/lexical-loops5/test.desc @@ -1,8 +1,8 @@ CORE test.c --show-lexical-loops _ --no-standard-checks -2 is head of \{ 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12 \(backedge\) \} -5 is head of \{ 5, 6, 7, 8 \(backedge\) \} +15 is head of \{ 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25 \(backedge\) \} +18 is head of \{ 18, 19, 20, 21 \(backedge\) \} ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-instrument/lexical-loops6/test.c b/regression/goto-instrument/lexical-loops6/test.c index bdb466108da..7c90c44467f 100644 --- a/regression/goto-instrument/lexical-loops6/test.c +++ b/regression/goto-instrument/lexical-loops6/test.c @@ -1,17 +1,18 @@ - -int main(int argc, char **argv) +int main() { int i = 0; + int count; + __CPROVER_assume(count > 10); - if(argc % 2) + if(count % 2) goto head2; head: - argc--; + count--; head2: ++i; if(i < 10) goto head; - return argc; + return count; } diff --git a/regression/goto-instrument/lexical-loops7/test.c b/regression/goto-instrument/lexical-loops7/test.c index 7332dcf7d88..ea1ea7e722c 100644 --- a/regression/goto-instrument/lexical-loops7/test.c +++ b/regression/goto-instrument/lexical-loops7/test.c @@ -1,15 +1,16 @@ - -int main(int argc, char **argv) +int main() { int i = 0; + int count; + __CPROVER_assume(count > 10); head: - argc--; + count--; ++i; if(i < 10 && i % 2) goto head; else if(i < 10) goto head; - return argc; + return count; } diff --git a/regression/goto-instrument/lexical-loops7/test.desc b/regression/goto-instrument/lexical-loops7/test.desc index f2facf040b6..a83e70cf31a 100644 --- a/regression/goto-instrument/lexical-loops7/test.desc +++ b/regression/goto-instrument/lexical-loops7/test.desc @@ -2,7 +2,7 @@ CORE test.c --show-lexical-loops ^Note not all loops were in lexical loop form$ -^2 is head of \{ 2, 3, 4, 5 \(backedge\) \} +^16 is head of \{ 16, 17, 18, 19 \(backedge\) \} ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-instrument/lexical-loops8/test.c b/regression/goto-instrument/lexical-loops8/test.c index d7a4a1159ad..9fd38163fdb 100644 --- a/regression/goto-instrument/lexical-loops8/test.c +++ b/regression/goto-instrument/lexical-loops8/test.c @@ -1,17 +1,17 @@ - -int main(int argc, char **argv) +int main() { int i = 0; + int count; while(i < 10) { - if(argc == 5) + if(count == 5) break; ++i; - if(argc % 7) + if(count % 7) continue; - argc--; + count--; } - return argc; + return count; } diff --git a/regression/goto-instrument/lexical-loops8/test.desc b/regression/goto-instrument/lexical-loops8/test.desc index b7e69cb2d8f..15c773844bd 100644 --- a/regression/goto-instrument/lexical-loops8/test.desc +++ b/regression/goto-instrument/lexical-loops8/test.desc @@ -1,7 +1,7 @@ CORE test.c --show-lexical-loops -^2 is head of \{ 2, 3, 4, 5, 6, 7, 8, 9, 10, 11 \(backedge\) \}$ +^15 is head of \{ 15, 16, 17, 18, 19, 20, 21, 22, 23, 24 \(backedge\) \}$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-instrument/lexical-loops9/test.c b/regression/goto-instrument/lexical-loops9/test.c index 96ba286ae01..7eded758356 100644 --- a/regression/goto-instrument/lexical-loops9/test.c +++ b/regression/goto-instrument/lexical-loops9/test.c @@ -1,18 +1,19 @@ - -int main(int argc, char **argv) +int main() { int i = 0; + int count; + __CPROVER_assume(count > 5); while(i < 10) { ++i; - if(argc == 5) + if(count == 5) { ++i; break; } - argc--; + count--; } - return argc; + return count; } diff --git a/regression/goto-instrument/lexical-loops9/test.desc b/regression/goto-instrument/lexical-loops9/test.desc index 34316088040..1ab01bc9a98 100644 --- a/regression/goto-instrument/lexical-loops9/test.desc +++ b/regression/goto-instrument/lexical-loops9/test.desc @@ -1,7 +1,7 @@ CORE test.c --show-lexical-loops -^2 is head of \{ 2, 3, 4, 7, 8, 9 \(backedge\) \}$ +^16 is head of \{ 16, 17, 18, 21, 22, 23 \(backedge\) \}$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-instrument/natural-loops-multiple-backedges/main.c b/regression/goto-instrument/natural-loops-multiple-backedges/main.c index d78adfa9ae5..e70523e0688 100644 --- a/regression/goto-instrument/natural-loops-multiple-backedges/main.c +++ b/regression/goto-instrument/natural-loops-multiple-backedges/main.c @@ -1,10 +1,12 @@ -int main(int argc, char **argv) +int main() { + int count; + __CPROVER_assume(count > 0); loop_header: - --argc; - if(argc == 1) + --count; + if(count == 1) goto loop_header; - else if(argc == 2) + else if(count == 2) goto loop_header; - return argc; + return count; } diff --git a/regression/goto-instrument/natural-loops-multiple-backedges/test.desc b/regression/goto-instrument/natural-loops-multiple-backedges/test.desc index 93c1bd15961..19f0f3ba402 100644 --- a/regression/goto-instrument/natural-loops-multiple-backedges/test.desc +++ b/regression/goto-instrument/natural-loops-multiple-backedges/test.desc @@ -1,11 +1,11 @@ CORE main.c --show-natural-loops -0 is head of \{ 0, 1, 2 \(backedge\), 4 \(backedge\) \} +14 is head of \{ 14, 15, 16 \(backedge\), 18 \(backedge\) \} ^EXIT=0$ ^SIGNAL=0$ -- ^warning: ignoring -- -In the line beginning "0 is head of" we expect to get 0, 1, 2 and 4 in some -order +In the line beginning "14 is head of" we expect to get 14, 15, 16 and 18 in some +order. diff --git a/regression/validate-trace-xml-schema/check.py b/regression/validate-trace-xml-schema/check.py index 4dabf069c3c..c6bda7b4f4f 100644 --- a/regression/validate-trace-xml-schema/check.py +++ b/regression/validate-trace-xml-schema/check.py @@ -14,6 +14,7 @@ ExcludedTests = list(map(lambda s: os.path.join(test_base_dir, s[0], s[1]), [ # these tests dump the raw SMT2 output (using --outfile) ['array_of_bool_as_bitvec', 'test-smt2-outfile.desc'], + ['deterministic-smt-output', 'test.desc'], # these tests expect input from stdin ['json-interface1', 'test_wrong_option.desc'], ['json-interface1', 'test.desc'], diff --git a/src/ansi-c/goto-conversion/goto_convert_class.h b/src/ansi-c/goto-conversion/goto_convert_class.h index 600938751f3..6ea485eeb59 100644 --- a/src/ansi-c/goto-conversion/goto_convert_class.h +++ b/src/ansi-c/goto-conversion/goto_convert_class.h @@ -50,6 +50,11 @@ class goto_convertt : public messaget { } + void set_prefix(const std::string &prefix) + { + tmp_symbol_prefix = prefix; + } + protected: symbol_table_baset &symbol_table; namespacet ns; diff --git a/src/goto-checker/goto_symex_property_decider.cpp b/src/goto-checker/goto_symex_property_decider.cpp index 51bcd5575c3..fdec0b18c19 100644 --- a/src/goto-checker/goto_symex_property_decider.cpp +++ b/src/goto-checker/goto_symex_property_decider.cpp @@ -63,7 +63,7 @@ void goto_symex_property_decidert:: { // it's going to be checked, but we don't know the status yet property_pair_it->second.status |= property_statust::UNKNOWN; - goal_map[property_id].instances.push_back(it); + goal_map[id2string(property_id)].instances.push_back(it); } } } diff --git a/src/goto-checker/goto_symex_property_decider.h b/src/goto-checker/goto_symex_property_decider.h index 21b4036b65d..368416763b2 100644 --- a/src/goto-checker/goto_symex_property_decider.h +++ b/src/goto-checker/goto_symex_property_decider.h @@ -82,10 +82,11 @@ class goto_symex_property_decidert exprt as_expr() const; }; - /// Maintains the relation between a property ID and - /// the corresponding goal variable that encodes - /// the negation of the conjunction of the instances of the property - std::map goal_map; + /// Maintains the relation between a property ID and the corresponding goal + /// variable that encodes the negation of the conjunction of the instances of + /// the property. Uses `std::string` to maintain consistent (lexicographic) + /// ordering as we iterate over this map to produce constraints. + std::map goal_map; }; #endif // CPROVER_GOTO_CHECKER_GOTO_SYMEX_PROPERTY_DECIDER_H diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp index 881d16ddcb1..314890a5ca0 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp @@ -138,6 +138,7 @@ void dfcc_instrument_loopt::operator()( exprt invariant(loop.invariant); const auto history_var_map = add_prehead_instructions( loop_id, + function_id, goto_function, symbol_table, head, @@ -172,6 +173,7 @@ void dfcc_instrument_loopt::operator()( add_body_instructions( loop_id, cbmc_loop_id, + function_id, goto_function, symbol_table, head, @@ -205,6 +207,7 @@ void dfcc_instrument_loopt::operator()( std::unordered_map dfcc_instrument_loopt::add_prehead_instructions( const std::size_t loop_id, + const irep_idt &function_id, goto_functionst::goto_functiont &goto_function, symbol_table_baset &symbol_table, goto_programt::targett loop_head, @@ -266,6 +269,7 @@ dfcc_instrument_loopt::add_prehead_instructions( code_frontend_assignt initial_invariant_assignment{ initial_invariant, invariant, loop_head_location}; goto_convertt converter(symbol_table, log.get_message_handler()); + converter.set_prefix(id2string(function_id) + "::$tmp"); converter.goto_convert( initial_invariant_assignment, pre_loop_head_instrs, language_mode); } @@ -425,6 +429,7 @@ dfcc_instrument_loopt::add_step_instructions( } goto_convertt converter(symbol_table, log.get_message_handler()); + converter.set_prefix(id2string(function_id) + "::$tmp"); const irep_idt &language_mode = dfcc_utilst::get_function_symbol(symbol_table, function_id).mode; { @@ -468,6 +473,7 @@ dfcc_instrument_loopt::add_step_instructions( void dfcc_instrument_loopt::add_body_instructions( const std::size_t loop_id, const std::size_t cbmc_loop_id, + const irep_idt &function_id, goto_functionst::goto_functiont &goto_function, symbol_table_baset &symbol_table, goto_programt::targett loop_head, @@ -513,6 +519,7 @@ void dfcc_instrument_loopt::add_body_instructions( } goto_convertt converter(symbol_table, log.get_message_handler()); + converter.set_prefix(id2string(function_id) + "::$tmp"); { // Because of the unconditional jump above the following code is only // reachable in the step case. Generate the inductive invariant check diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.h index 8e624e016ae..0db2bb5889c 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.h @@ -178,6 +178,7 @@ class dfcc_instrument_loopt /// ``` /// /// \param[in] loop_id Id of the loop to transform. + /// \param[in] function_id Id of the function. /// \param[inout] goto_function The function containing the loop. /// \param[inout] symbol_table Symbol table of the model. /// \param[inout] loop_head Head node of the loop. @@ -195,6 +196,7 @@ class dfcc_instrument_loopt /// \return `history_var_map` that maps variables to loop_entry variables. std::unordered_map add_prehead_instructions( const std::size_t loop_id, + const irep_idt &function_id, goto_functionst::goto_functiont &goto_function, symbol_table_baset &symbol_table, goto_programt::targett loop_head, @@ -277,6 +279,7 @@ class dfcc_instrument_loopt /// /// \param[in] loop_id Id assigned to the loop by the `cfg_info` numbering. /// \param[in] cbmc_loop_id Id assigned to the loop by CBMC's numbering. + /// \param[in] function_id Id of the function. /// \param[inout] goto_function The function containing the loop. /// \param[inout] symbol_table Symbol table of the model. /// \param[in] loop_head Head node of the loop. @@ -292,6 +295,7 @@ class dfcc_instrument_loopt void add_body_instructions( const std::size_t loop_id, const std::size_t cbmc_loop_id, + const irep_idt &function_id, goto_functionst::goto_functiont &goto_function, symbol_table_baset &symbol_table, goto_programt::targett loop_head, diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp index 028893f05d9..3c4809a79b7 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp @@ -548,7 +548,11 @@ void dfcc_libraryt::add_instrumented_functions_map_init_instructions( auto instrumented_functions_map = get_instrumented_functions_map_symbol().symbol_expr(); - for(auto &function_id : instrumented_functions) + std::map sorted_instrumented_functions; + for(const auto &function_id : instrumented_functions) + sorted_instrumented_functions.insert({id2string(function_id), function_id}); + + for(const auto &[_, function_id] : sorted_instrumented_functions) { auto object_id = pointer_object(address_of_exprt( dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id) diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp index 9124f954e8d..9889951f5f4 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp @@ -203,6 +203,8 @@ dfcc_wrapper_programt::dfcc_wrapper_programt( ns(goto_model.symbol_table), converter(goto_model.symbol_table, log.get_message_handler()) { + converter.set_prefix(id2string(wrapper_symbol.name) + "::$tmp"); + // generate a return value symbol (needed to instantiate all contract lambdas) if(contract_code_type.return_type().id() != ID_empty) { diff --git a/src/goto-programs/goto_functions.cpp b/src/goto-programs/goto_functions.cpp index f4ac42e6d4a..1a53300f444 100644 --- a/src/goto-programs/goto_functions.cpp +++ b/src/goto-programs/goto_functions.cpp @@ -21,10 +21,11 @@ Date: June 2003 void goto_functionst::compute_location_numbers() { unused_location_number = 0; - for(auto &func : function_map) + auto sorted_funcs = sorted(); + for(auto &it : sorted_funcs) { // Side-effect: bumps unused_location_number. - func.second.body.compute_location_numbers(unused_location_number); + it->second.body.compute_location_numbers(unused_location_number); } } diff --git a/src/goto-programs/set_properties.cpp b/src/goto-programs/set_properties.cpp index 49a5d18dfbe..6c122801668 100644 --- a/src/goto-programs/set_properties.cpp +++ b/src/goto-programs/set_properties.cpp @@ -131,9 +131,7 @@ void label_properties(goto_functionst &goto_functions) { std::map property_counters; - for(goto_functionst::function_mapt::iterator - it=goto_functions.function_map.begin(); - it!=goto_functions.function_map.end(); - it++) + auto sorted = goto_functions.sorted(); + for(auto &it : sorted) label_properties(it->first, it->second.body, property_counters); } diff --git a/src/goto-programs/show_properties.cpp b/src/goto-programs/show_properties.cpp index c3e94c26600..38e46131f50 100644 --- a/src/goto-programs/show_properties.cpp +++ b/src/goto-programs/show_properties.cpp @@ -180,8 +180,10 @@ void show_properties_json( messaget msg(message_handler); json_arrayt json_properties; - for(const auto &fct : goto_functions.function_map) - convert_properties_json(json_properties, ns, fct.first, fct.second.body); + // sort alphabetically + const auto sorted = goto_functions.sorted(); + for(const auto &it : sorted) + convert_properties_json(json_properties, ns, it->first, it->second.body); json_objectt json_result{{"properties", json_properties}}; msg.result() << json_result; @@ -196,8 +198,12 @@ void show_properties( if(ui == ui_message_handlert::uit::JSON_UI) show_properties_json(ns, ui_message_handler, goto_functions); else - for(const auto &fct : goto_functions.function_map) - show_properties(ns, fct.first, ui_message_handler, ui, fct.second.body); + { + // sort alphabetically + const auto sorted = goto_functions.sorted(); + for(const auto &it : sorted) + show_properties(ns, it->first, ui_message_handler, ui, it->second.body); + } } void show_properties( diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index 3bde290706b..b61e48f36a5 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -23,6 +23,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "simplify_expr_with_value_set.h" #include +#include void goto_symext::apply_goto_condition( goto_symex_statet ¤t_state, @@ -715,8 +716,20 @@ void goto_symext::phi_function( goto_state.get_level2().current_names.get_delta_view( dest_state.get_level2().current_names, delta_view, false); - for(const auto &delta_item : delta_view) + std::map + ordered_names_to_merge; + for(auto it = delta_view.begin(); it != delta_view.end(); ++it) { + const ssa_exprt &ssa = it->m.first; + bool inserted = + ordered_names_to_merge.insert({id2string(ssa.get_identifier()), it}) + .second; + CHECK_RETURN(inserted); + } + + for(const auto &ordered_entry : ordered_names_to_merge) + { + const auto &delta_item = *ordered_entry.second; const ssa_exprt &ssa = delta_item.m.first; std::size_t goto_count = delta_item.m.second; std::size_t dest_count = !delta_item.is_in_both_maps() @@ -741,11 +754,22 @@ void goto_symext::phi_function( dest_state.get_level2().current_names.get_delta_view( goto_state.get_level2().current_names, delta_view, false); - for(const auto &delta_item : delta_view) + ordered_names_to_merge.clear(); + for(auto it = delta_view.begin(); it != delta_view.end(); ++it) { - if(delta_item.is_in_both_maps()) + if(it->is_in_both_maps()) continue; + const ssa_exprt &ssa = it->m.first; + bool inserted = + ordered_names_to_merge.insert({id2string(ssa.get_identifier()), it}) + .second; + CHECK_RETURN(inserted); + } + + for(const auto &ordered_entry : ordered_names_to_merge) + { + const auto &delta_item = *ordered_entry.second; const ssa_exprt &ssa = delta_item.m.first; std::size_t goto_count = 0; std::size_t dest_count = delta_item.m.second; diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index e00becc56e9..6e1903359d3 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -209,7 +209,9 @@ void smt2_convt::write_footer() { out << "\n"; - // fix up the object sizes + // Output object size definitions + // Note: object_sizes is std::map, so iteration is deterministic (sorted by + // key) for(const auto &object : object_sizes) define_object_size(object.second, object.first); @@ -243,6 +245,9 @@ void smt2_convt::write_footer() if(solver!=solvert::BOOLECTOR) { + // Output get-value commands for all identifiers + // Note: smt2_identifiers is std::set, so iteration is deterministic + // (sorted) for(const auto &id : smt2_identifiers) out << "(get-value (" << id << "))" << "\n"; @@ -5281,6 +5286,15 @@ exprt smt2_convt::prepare_for_convert_expr(const exprt &expr) return lowered_expr; } +/// Find and declare symbols used in an expression +/// This function traverses the expression tree and creates SMT2 declarations +/// for all symbols (variables) found. Symbols are added to identifier_map to +/// avoid duplication declarations. +/// +/// Determinism: The traversal of expression trees is deterministic, and solely +/// depends on syntactic expression structure, not expression hash codes. +/// +/// \param expr: expression to scan for symbols void smt2_convt::find_symbols(const exprt &expr) { if(is_zero_width(expr.type(), ns)) diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 8670a17b974..283022f02a6 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -1012,6 +1012,45 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr) } } + // Push a pointer typecast into pointer arithmetic + // (T)(ptr + int) ---> (T)ptr + sizeof(inner-st)/sizeof(outer-st)*int + // when the inner subtype's size is a multiple of the outer subtype's size + if( + expr_type.id() == ID_pointer && op_type.id() == ID_pointer && + expr.op().id() == ID_plus) + { + const auto step = + pointer_offset_size(to_pointer_type(op_type).base_type(), ns); + const auto new_step = + pointer_offset_size(to_pointer_type(expr_type).base_type(), ns); + + if( + step.has_value() && *step != 0 && new_step.has_value() && + *new_step != 0 && *step >= *new_step && *step % *new_step == 0) + { + const typet size_t_type(size_type()); + auto new_expr = expr.op(); + new_expr.type() = expr.type(); + + for(auto &op : new_expr.operands()) + { + if(op.type().id() == ID_pointer) + { + exprt new_op = simplify_typecast(typecast_exprt{op, expr.type()}); + op = std::move(new_op); + } + else if(*step > *new_step) + { + exprt new_op = simplify_mult( + mult_exprt{from_integer(*step / *new_step, op.type()), op}); + op = std::move(new_op); + } + } + + return changed(simplify_plus(to_plus_expr(new_expr))); + } + } + const irep_idt &expr_type_id=expr_type.id(); const exprt &operand = expr.op(); const irep_idt &op_type_id=op_type.id();