Update copyright blob (model-checking#1144)

* Update copyright check script

We are changing Kani's copyright from Amazon to "Kani Contributors"

* Update Kani copyright blob Amazon -> Kani Contributors

I used the following command to update the blob:

git ls-files | xargs -d "\n" -L 1 sed -i "0,/Copyright Amazon.com/{s/Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved./Copyright Kani Contributors/}"

.github/CODEOWNERS

@@ -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
 
 *   @model-checking/kani-devs

.github/actions/setup/action.yml

@@ -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
 name: Setup Kani Dependencies
 inputs:

.github/workflows/audit.yml

@@ -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
 
 # A temporary, non-required workflow to notify us when cargo-audit has things to say.

.github/workflows/format-check.yml

@@ -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
 name: Kani Format Check
 on: pull_request

.github/workflows/kani.yml

@@ -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
 name: Kani CI
 on: [push, pull_request]

.github/workflows/release.yml

@@ -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
 name: Release
 on:

Cargo.toml

@@ -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
 
 [package]

build.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
 
 use std::env::var;

cprover_bindings/Cargo.toml

@@ -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
 
 [package]

cprover_bindings/src/cbmc_string.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
 
 use lazy_static::lazy_static;

cprover_bindings/src/env.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
 //! Find mod.rs for centralized documentation
 //!

cprover_bindings/src/goto_program/builtin.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
 //! this module lazily declares builtin functions in CBMC
 use self::BuiltinFn::*;

cprover_bindings/src/goto_program/expr.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
 use self::BinaryOperand::*;
 use self::ExprValue::*;

cprover_bindings/src/goto_program/location.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
 use crate::cbmc_string::{InternStringOption, InternedString};
 use std::convert::TryInto;

cprover_bindings/src/goto_program/mod.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
 //! This module contains typesafe representations of CBMC's data structures
 

cprover_bindings/src/goto_program/stmt.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
 use self::StmtBody::*;
 use super::{BuiltinFn, Expr, Location};

cprover_bindings/src/goto_program/symbol.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
 use super::super::utils::aggr_tag;
 use super::{DatatypeComponent, Expr, Location, Parameter, Stmt, Type};

cprover_bindings/src/goto_program/symbol_table.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
 use super::super::{env, MachineModel};
 use super::{BuiltinFn, Stmt, Symbol};

cprover_bindings/src/goto_program/symtab_transformer/gen_c_transformer/expr_transformer.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
 
 use std::ops::{BitAnd, Shl, Shr};

cprover_bindings/src/goto_program/symtab_transformer/gen_c_transformer/mod.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
 
 mod expr_transformer;

cprover_bindings/src/goto_program/symtab_transformer/gen_c_transformer/name_transformer.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
 
 use super::super::Transformer;

cprover_bindings/src/goto_program/symtab_transformer/gen_c_transformer/nondet_transformer.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
 
 use super::super::Transformer;

cprover_bindings/src/goto_program/symtab_transformer/identity_transformer.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
 
 use super::Transformer;

cprover_bindings/src/goto_program/symtab_transformer/mod.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
 //! This module contains the structures used for symbol table transformations.
 

cprover_bindings/src/goto_program/symtab_transformer/passes.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
 
 use super::gen_c_transformer::{ExprTransformer, NameTransformer, NondetTransformer};

cprover_bindings/src/goto_program/symtab_transformer/transformer.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
 
 use crate::goto_program::{

cprover_bindings/src/goto_program/typ.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
 use self::DatatypeComponent::*;
 use self::Type::*;

cprover_bindings/src/irep/irep.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
 //! The actual `Irep` structure, and associated constructors, getters, and setters.
 

cprover_bindings/src/irep/irep_id.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
 //! find mod.rs for centralized documentation
 //!

cprover_bindings/src/irep/mod.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
 //! This module is am implementation of the `Irep` serilization format for goto programs.
 //!

cprover_bindings/src/irep/serialize.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
 //! This crate implements irep serialization using serde Serializer.
 use crate::irep::{Irep, IrepId, Symbol, SymbolTable};

cprover_bindings/src/irep/symbol.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
 use super::Irep;
 use crate::InternedString;

cprover_bindings/src/irep/symbol_table.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
 use super::Symbol;
 use crate::InternedString;

cprover_bindings/src/irep/to_irep.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
 //! Converts a typed goto-program into the `Irep` serilization format of CBMC
 // TODO: consider making a macro to replace `linear_map![])` for initilizing btrees.

cprover_bindings/src/lib.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
 //! This module contains the representations of CBMC's daa structures.
 //!

cprover_bindings/src/machine_model.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
 /// Represents the machine specific information necessary to generate an Irep.
 use num::bigint::BigInt;

cprover_bindings/src/utils.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
 //! Useful utilities for CBMC
 

docs/book.toml

@@ -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
 [book]
 title = "The Kani Rust Verifier"

docs/build-docs.sh

@@ -1,5 +1,5 @@
 #!/usr/bin/env bash
-# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# Copyright Kani Contributors
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 set -eu

docs/src/getting-started/verification-results/Cargo.toml

@@ -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
 
 [package]

docs/src/getting-started/verification-results/src/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
 
 #[kani::proof]

docs/src/tutorial/arbitrary-variables/Cargo.toml

@@ -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
 [package]
 name = "arbitrary-variables"

docs/src/tutorial/arbitrary-variables/src/inventory.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
 
 // ANCHOR: inventory_lib

docs/src/tutorial/arbitrary-variables/src/lib.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
 
 pub mod inventory;

docs/src/tutorial/arbitrary-variables/src/rating.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
 
 // ANCHOR: rating_struct

docs/src/tutorial/kani-first-steps/Cargo.toml

@@ -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
 [package]
 name = "kani-first-steps"

docs/src/tutorial/kani-first-steps/src/final_form.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
 
 // ANCHOR: code

docs/src/tutorial/kani-first-steps/src/lib.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
 // kani-verify-fail
 

docs/src/tutorial/kinds-of-failure/Cargo.toml

@@ -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
 [package]
 name = "kinds-of-failure"

docs/src/tutorial/kinds-of-failure/src/bounds_check.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
 // kani-verify-fail
 

docs/src/tutorial/kinds-of-failure/src/lib.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
 pub mod bounds_check;
 pub mod overflow;

docs/src/tutorial/kinds-of-failure/src/overflow.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
 // kani-verify-fail
 

docs/src/tutorial/kinds-of-failure/src/overflow_quicksort.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
 // kani-verify-fail
 

docs/src/tutorial/loops-unwinding/Cargo.toml

@@ -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
 [package]
 name = "loops-unwinding"

docs/src/tutorial/loops-unwinding/src/lib.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
 
 // ANCHOR: code

kani-compiler/Cargo.toml

@@ -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
 
 [package]

kani-compiler/build.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
 
 use std::env;

kani-compiler/kani_queries/Cargo.toml

@@ -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
 
 [package]

kani-compiler/kani_queries/src/lib.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
 
 use std::sync::atomic::{AtomicBool, Ordering};

kani-compiler/src/codegen_cprover_gotoc/codegen/assert.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
 
 //! This file contains the code that acts as a wrapper to create the new assert and related statements

kani-compiler/src/codegen_cprover_gotoc/codegen/block.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
 
 //! This file contains functions related to codegenning MIR blocks into gotoc

kani-compiler/src/codegen_cprover_gotoc/codegen/function.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
 
 //! This file contains functions related to codegenning MIR functions into gotoc

kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.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
 //! this module handles intrinsics
 use super::PropertyClass;

kani-compiler/src/codegen_cprover_gotoc/codegen/mod.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
 
 //! This module does that actual translation of MIR constructs to goto constructs.

kani-compiler/src/codegen_cprover_gotoc/codegen/operand.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
 use crate::codegen_cprover_gotoc::utils::slice_fat_ptr;
 use crate::codegen_cprover_gotoc::GotocCtx;

kani-compiler/src/codegen_cprover_gotoc/codegen/place.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
 //! responsible for handling codegening places.
 //!