Adjust test patterns so as not to check for trivial properties (#3464)

tautschnig · web-flow · commit d5c1b71c3da1 · 2024-08-27T13:51:33.000Z
With diffblue/cbmc#8413, CBMC will no longer create property checks for assigns clauses that are trivially true. We had CBMC-Nightly failing since August 17th given the CBMC change. This will bring CBMC-Nightly back to a passing state. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
diff --git 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
@@ -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
