Fix copyright check for expected tests (model-checking#3170)

This PR modifies the pattern used to exclude files from the copyright
check for `expected` files. This ensures we check the copyright in files
under `tests/expected/` while it skips the check for `expected` and
`*.expected` files. It also adds/modifies copyright headers for some
files that weren't being checked until now.

Resolves model-checking#3141

scripts/ci/copyright-exclude

@@ -10,7 +10,7 @@ Cargo.lock
 LICENSE-APACHE
 LICENSE-MIT
 editorconfig
-expected
+expected$
 gitattributes
 gitignore
 gitmodules

tests/expected/coroutines/main.rs

@@ -1,4 +1,4 @@
-// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 #![feature(coroutines, coroutine_trait)]

tests/expected/coroutines/pin/main.rs

@@ -1,4 +1,4 @@
-// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 // Test contains a call to a coroutine via a Pin

tests/expected/function-contract/modifies/refcell_fixme.rs

@@ -1,3 +1,5 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
 use std::cell::RefCell;
 use std::ops::Deref;
 

tests/expected/offset-wraps-around/main.rs

@@ -1,4 +1,4 @@
-// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 // Check that a high offset causes a "wrapping around" behavior in CBMC.

tests/expected/slice_c_str/c_str_fixme.rs

@@ -1,3 +1,5 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
 #![feature(rustc_private)]
 #![feature(c_str_literals)]
 //! FIXME: <https://github.com/rust-lang/rust/issues/113333>