From 8814d6722d9d09a856c29e188eb8ad37279ff59c Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 27 Aug 2024 07:52:02 +0000 Subject: [PATCH] Adjust test patterns so as not to check for trivial properties With diffblue/cbmc#8413, CBMC will no longer create property checks for assigns clauses that are trivially true. --- tests/expected/function-contract/modifies/havoc_pass.expected | 2 +- .../function-contract/modifies/havoc_pass_reordered.expected | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/expected/function-contract/modifies/havoc_pass.expected b/tests/expected/function-contract/modifies/havoc_pass.expected index d5679f71b74c..f7bbb8202c46 100644 --- a/tests/expected/function-contract/modifies/havoc_pass.expected +++ b/tests/expected/function-contract/modifies/havoc_pass.expected @@ -7,7 +7,7 @@ VERIFICATION:- SUCCESSFUL .assigns\ - Status: SUCCESS\ -- Description: "Check that var_4 is assignable"\ +- Description: "Check that *dst is assignable"\ in function copy VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/modifies/havoc_pass_reordered.expected b/tests/expected/function-contract/modifies/havoc_pass_reordered.expected index 2ea601aa26a0..7036111c76bf 100644 --- a/tests/expected/function-contract/modifies/havoc_pass_reordered.expected +++ b/tests/expected/function-contract/modifies/havoc_pass_reordered.expected @@ -7,7 +7,7 @@ VERIFICATION:- SUCCESSFUL copy.assigns\ - Status: SUCCESS\ -- Description: "Check that var_5 is assignable"\ +- Description: "Check that *dst is assignable"\ in function copy VERIFICATION:- SUCCESSFUL