From 1834eeca51b5d6fb17d9be6f5f41e4528a493789 Mon Sep 17 00:00:00 2001 From: esteffin Date: Tue, 19 Dec 2023 19:07:25 +0000 Subject: [PATCH] Fixed goto-synthesizer failing regression test --- regression/goto-synthesizer/array_uf/test.desc | 2 +- .../goto-synthesizer/loop_contracts_synthesis_01/test.desc | 2 +- .../goto-synthesizer/loop_contracts_synthesis_01/test_dump.desc | 2 +- .../goto-synthesizer/loop_contracts_synthesis_02/test.desc | 2 +- .../goto-synthesizer/loop_contracts_synthesis_02/test_dump.desc | 2 +- .../goto-synthesizer/loop_contracts_synthesis_03/test.desc | 2 +- .../loop_contracts_synthesis_03/test_cadical.desc | 2 +- .../goto-synthesizer/loop_contracts_synthesis_03/test_dump.desc | 2 +- .../goto-synthesizer/loop_contracts_synthesis_04/test.desc | 2 +- .../goto-synthesizer/loop_contracts_synthesis_04/test_dump.desc | 2 +- .../goto-synthesizer/loop_contracts_synthesis_08/test.desc | 2 +- 11 files changed, 11 insertions(+), 11 deletions(-) diff --git a/regression/goto-synthesizer/array_uf/test.desc b/regression/goto-synthesizer/array_uf/test.desc index 81f0cc90d5de..bf33d9d629e8 100644 --- a/regression/goto-synthesizer/array_uf/test.desc +++ b/regression/goto-synthesizer/array_uf/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check _ --arrays-uf-always _ --arrays-uf-always +--pointer-check _ --no-malloc-may-fail --arrays-uf-always _ --arrays-uf-always ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/goto-synthesizer/loop_contracts_synthesis_01/test.desc b/regression/goto-synthesizer/loop_contracts_synthesis_01/test.desc index 405303402c77..443ffa43fddf 100644 --- a/regression/goto-synthesizer/loop_contracts_synthesis_01/test.desc +++ b/regression/goto-synthesizer/loop_contracts_synthesis_01/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check +--pointer-check _ --no-malloc-may-fail _ --no-standard-checks ^EXIT=0$ ^SIGNAL=0$ ^\[main\.\d+\] line 10 Check loop invariant before entry: SUCCESS$ diff --git a/regression/goto-synthesizer/loop_contracts_synthesis_01/test_dump.desc b/regression/goto-synthesizer/loop_contracts_synthesis_01/test_dump.desc index 363f91f24e65..8d9ef3ada569 100644 --- a/regression/goto-synthesizer/loop_contracts_synthesis_01/test_dump.desc +++ b/regression/goto-synthesizer/loop_contracts_synthesis_01/test_dump.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check _ --dump-loop-contracts --json-output main.c +--pointer-check _ --no-malloc-may-fail --dump-loop-contracts --json-output main.c ^EXIT=0$ ^SIGNAL=0$ \"sources"\: \[ \"main\.c\" \] diff --git a/regression/goto-synthesizer/loop_contracts_synthesis_02/test.desc b/regression/goto-synthesizer/loop_contracts_synthesis_02/test.desc index 71ecf7106695..a7a3276e65e5 100644 --- a/regression/goto-synthesizer/loop_contracts_synthesis_02/test.desc +++ b/regression/goto-synthesizer/loop_contracts_synthesis_02/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check +--pointer-check _ --no-malloc-may-fail ^EXIT=0$ ^SIGNAL=0$ ^\[main.pointer\_dereference.\d+\] .* SUCCESS$ diff --git a/regression/goto-synthesizer/loop_contracts_synthesis_02/test_dump.desc b/regression/goto-synthesizer/loop_contracts_synthesis_02/test_dump.desc index dd6f4658ccad..8200b32e88e3 100644 --- a/regression/goto-synthesizer/loop_contracts_synthesis_02/test_dump.desc +++ b/regression/goto-synthesizer/loop_contracts_synthesis_02/test_dump.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check _ --dump-loop-contracts +--pointer-check _ --dump-loop-contracts --no-malloc-may-fail ^EXIT=0$ ^SIGNAL=0$ \"sources"\: \[ \"main\.c\" \] diff --git a/regression/goto-synthesizer/loop_contracts_synthesis_03/test.desc b/regression/goto-synthesizer/loop_contracts_synthesis_03/test.desc index 70c75536ac23..195581932abb 100644 --- a/regression/goto-synthesizer/loop_contracts_synthesis_03/test.desc +++ b/regression/goto-synthesizer/loop_contracts_synthesis_03/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check +--pointer-check _ --no-malloc-may-fail _ --no-standard-checks ^EXIT=0$ ^SIGNAL=0$ ^\[main.pointer\_dereference.\d+\] .* SUCCESS$ diff --git a/regression/goto-synthesizer/loop_contracts_synthesis_03/test_cadical.desc b/regression/goto-synthesizer/loop_contracts_synthesis_03/test_cadical.desc index 9b1ab0946342..c7efad193a57 100644 --- a/regression/goto-synthesizer/loop_contracts_synthesis_03/test_cadical.desc +++ b/regression/goto-synthesizer/loop_contracts_synthesis_03/test_cadical.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check _ --sat-solver cadical --verbosity 10 +--pointer-check _ --no-malloc-may-fail --sat-solver cadical --verbosity 10 _ --no-standard-checks ^EXIT=0$ ^SIGNAL=0$ Solving with CaDiCaL|The specified solver, 'cadical', is not available. The default solver will be used instead. diff --git a/regression/goto-synthesizer/loop_contracts_synthesis_03/test_dump.desc b/regression/goto-synthesizer/loop_contracts_synthesis_03/test_dump.desc index 08d4cad81ff7..bfec5782fe80 100644 --- a/regression/goto-synthesizer/loop_contracts_synthesis_03/test_dump.desc +++ b/regression/goto-synthesizer/loop_contracts_synthesis_03/test_dump.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check _ --dump-loop-contracts +--pointer-check _ --no-malloc-may-fail --dump-loop-contracts ^EXIT=0$ ^SIGNAL=0$ \"sources"\: \[ \"main\.c\" \] diff --git a/regression/goto-synthesizer/loop_contracts_synthesis_04/test.desc b/regression/goto-synthesizer/loop_contracts_synthesis_04/test.desc index e7ee10ae51a4..9ebb1913e743 100644 --- a/regression/goto-synthesizer/loop_contracts_synthesis_04/test.desc +++ b/regression/goto-synthesizer/loop_contracts_synthesis_04/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check _ --verbosity 9 +--pointer-check _ --no-malloc-may-fail --verbosity 9 ^EXIT=0$ ^SIGNAL=0$ Quick filter\: 6.* out of 67 candidates were filtered out\. diff --git a/regression/goto-synthesizer/loop_contracts_synthesis_04/test_dump.desc b/regression/goto-synthesizer/loop_contracts_synthesis_04/test_dump.desc index 41399773eff7..a8274ceb1bde 100644 --- a/regression/goto-synthesizer/loop_contracts_synthesis_04/test_dump.desc +++ b/regression/goto-synthesizer/loop_contracts_synthesis_04/test_dump.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check _ --dump-loop-contracts +--pointer-check _ --no-malloc-may-fail --dump-loop-contracts ^EXIT=0$ ^SIGNAL=0$ \"sources"\: \[ \"main\.c\" \] diff --git a/regression/goto-synthesizer/loop_contracts_synthesis_08/test.desc b/regression/goto-synthesizer/loop_contracts_synthesis_08/test.desc index 2b98c115ec74..ecedb4797aab 100644 --- a/regression/goto-synthesizer/loop_contracts_synthesis_08/test.desc +++ b/regression/goto-synthesizer/loop_contracts_synthesis_08/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check +--pointer-check _ --no-malloc-may-fail _ --no-standard-checks ^EXIT=0$ ^SIGNAL=0$ ^\[main.pointer\_dereference.\d+\] .* SUCCESS$