From fb8003146fb11d12ae14ff6aeafc6afc16d9f115 Mon Sep 17 00:00:00 2001
From: "github-actions[bot]"
 <41898282+github-actions[bot]@users.noreply.github.com>
Date: Wed, 2 Oct 2024 03:58:02 +0000
Subject: [PATCH 1/4] Automatic toolchain upgrade to nightly-2024-10-02 (#3562)

Update Rust toolchain from nightly-2024-10-01 to nightly-2024-10-02
without any other source changes.

Co-authored-by: celinval <35149715+celinval@users.noreply.github.com>
---
 rust-toolchain.toml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index c0fba0261fa7..bd0b55ef531f 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2024-10-01"
+channel = "nightly-2024-10-02"
 components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]

From 14ebca99fbe9c7bb0f58b937bfb01d079687c51c Mon Sep 17 00:00:00 2001
From: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
Date: Wed, 2 Oct 2024 10:46:34 -0700
Subject: [PATCH 2/4] Remove obsolete linker options (#3559)

These were made obsolete a while back.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
---
 kani-driver/src/args/mod.rs                     | 17 +----------------
 tests/cargo-kani/asm/global/Cargo.toml          |  2 +-
 tests/cargo-kani/mir-linker/Cargo.toml          |  3 ---
 tests/cargo-ui/ws-integ-tests/Cargo.toml        |  2 --
 tests/kani/UnsizedCoercion/basic_coercion.rs    |  1 -
 .../UnsizedCoercion/basic_inner_coercion.rs     |  1 -
 .../UnsizedCoercion/basic_outer_coercion.rs     |  1 -
 tests/kani/UnsizedCoercion/box_coercion.rs      |  1 -
 .../kani/UnsizedCoercion/box_inner_coercion.rs  |  1 -
 .../kani/UnsizedCoercion/box_outer_coercion.rs  |  1 -
 .../UnsizedCoercion/custom_outer_coercion.rs    |  1 -
 tests/kani/UnsizedCoercion/double_coercion.rs   |  1 -
 tests/kani/UnsizedCoercion/rc_outer_coercion.rs |  1 -
 .../UnsizedCoercion/trait_to_trait_coercion.rs  |  1 -
 tests/perf/string/src/any_str.rs                |  5 -----
 .../Strings/copy_empty_string_by_intrinsic.rs   |  1 -
 .../ui/mir-linker/generic-harness/incorrect.rs  |  2 --
 17 files changed, 2 insertions(+), 40 deletions(-)

diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs
index 72de44e36014..573ad21ab31a 100644
--- a/kani-driver/src/args/mod.rs
+++ b/kani-driver/src/args/mod.rs
@@ -40,6 +40,7 @@ where
         .unwrap()
 }
 
+#[allow(dead_code)]
 pub fn print_obsolete(verbosity: &CommonArgs, option: &str) {
     if !verbosity.quiet {
         warning(&format!(
@@ -189,14 +190,6 @@ pub struct VerificationArgs {
     #[arg(long, hide_short_help = true)]
     pub only_codegen: bool,
 
-    /// Deprecated flag. This is a no-op since we no longer support the legacy linker and
-    /// it will be removed in a future Kani release.
-    #[arg(long, hide = true, conflicts_with("mir_linker"))]
-    pub legacy_linker: bool,
-    /// Deprecated flag. This is a no-op since we no longer support any other linker.
-    #[arg(long, hide = true)]
-    pub mir_linker: bool,
-
     /// Specify the value used for loop unwinding in CBMC
     #[arg(long)]
     pub default_unwind: Option<u32>,
@@ -524,14 +517,6 @@ impl ValidateArgs for VerificationArgs {
             }
         }
 
-        if self.mir_linker {
-            print_obsolete(&self.common_args, "--mir-linker");
-        }
-
-        if self.legacy_linker {
-            print_obsolete(&self.common_args, "--legacy-linker");
-        }
-
         // TODO: these conflicting flags reflect what's necessary to pass current tests unmodified.
         // We should consider improving the error messages slightly in a later pull request.
         if natives_unwind && extra_unwind {
diff --git a/tests/cargo-kani/asm/global/Cargo.toml b/tests/cargo-kani/asm/global/Cargo.toml
index 21ff904a2f99..79ffab9377c1 100644
--- a/tests/cargo-kani/asm/global/Cargo.toml
+++ b/tests/cargo-kani/asm/global/Cargo.toml
@@ -13,4 +13,4 @@ crate_with_global_asm = { path = "crate_with_global_asm" }
 
 [package.metadata.kani]
 # Issue with MIR Linker on static constant.
-flags = { enable-unstable = true, ignore-global-asm = true, mir-linker = true }
+flags = { enable-unstable = true, ignore-global-asm = true }
diff --git a/tests/cargo-kani/mir-linker/Cargo.toml b/tests/cargo-kani/mir-linker/Cargo.toml
index 39d5016a407b..f00d4c687864 100644
--- a/tests/cargo-kani/mir-linker/Cargo.toml
+++ b/tests/cargo-kani/mir-linker/Cargo.toml
@@ -8,6 +8,3 @@ description = "Ensures that the mir-linker works accross crates"
 
 [dependencies]
 semver = "1.0"
-
-[package.metadata.kani]
-flags = { mir-linker=true, enable-unstable=true }
diff --git a/tests/cargo-ui/ws-integ-tests/Cargo.toml b/tests/cargo-ui/ws-integ-tests/Cargo.toml
index b09d4c9a5f19..93c4baebe120 100644
--- a/tests/cargo-ui/ws-integ-tests/Cargo.toml
+++ b/tests/cargo-ui/ws-integ-tests/Cargo.toml
@@ -15,5 +15,3 @@ members = [
 [workspace.metadata.kani.flags]
 workspace = true
 tests = true
-enable-unstable=true
-mir-linker=true
diff --git a/tests/kani/UnsizedCoercion/basic_coercion.rs b/tests/kani/UnsizedCoercion/basic_coercion.rs
index a60a76aec3be..ee8c80e87011 100644
--- a/tests/kani/UnsizedCoercion/basic_coercion.rs
+++ b/tests/kani/UnsizedCoercion/basic_coercion.rs
@@ -1,6 +1,5 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: --mir-linker --enable-unstable
 //! Check the basic coercion from using built-in references and pointers.
 //! Tests are broken down into different crates to ensure that the reachability works for each case.
 
diff --git a/tests/kani/UnsizedCoercion/basic_inner_coercion.rs b/tests/kani/UnsizedCoercion/basic_inner_coercion.rs
index efc84b61ea1e..19d8f39fed7e 100644
--- a/tests/kani/UnsizedCoercion/basic_inner_coercion.rs
+++ b/tests/kani/UnsizedCoercion/basic_inner_coercion.rs
@@ -1,6 +1,5 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: --mir-linker --enable-unstable
 //! Check the basic coercion from using built-in references and pointers.
 //! Tests are broken down into different crates to ensure that the reachability works for each case.
 
diff --git a/tests/kani/UnsizedCoercion/basic_outer_coercion.rs b/tests/kani/UnsizedCoercion/basic_outer_coercion.rs
index a2b5bfae3129..633dfbdaa995 100644
--- a/tests/kani/UnsizedCoercion/basic_outer_coercion.rs
+++ b/tests/kani/UnsizedCoercion/basic_outer_coercion.rs
@@ -1,6 +1,5 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: --mir-linker --enable-unstable
 //! Check the basic coercion from using built-in references and pointers.
 //! Tests are broken down into different crates to ensure that the reachability works for each case.
 
diff --git a/tests/kani/UnsizedCoercion/box_coercion.rs b/tests/kani/UnsizedCoercion/box_coercion.rs
index e022bdef06e1..106f586f8eed 100644
--- a/tests/kani/UnsizedCoercion/box_coercion.rs
+++ b/tests/kani/UnsizedCoercion/box_coercion.rs
@@ -1,6 +1,5 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: --mir-linker --enable-unstable
 //! Check the basic coercion when using boxes.
 //! Tests are broken down into different crates to ensure that the reachability works for each case.
 
diff --git a/tests/kani/UnsizedCoercion/box_inner_coercion.rs b/tests/kani/UnsizedCoercion/box_inner_coercion.rs
index 35f10373d5ef..4e8a8b56624c 100644
--- a/tests/kani/UnsizedCoercion/box_inner_coercion.rs
+++ b/tests/kani/UnsizedCoercion/box_inner_coercion.rs
@@ -1,6 +1,5 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: --mir-linker --enable-unstable
 //! Check the basic coercion when using boxes.
 //! Tests are broken down into different crates to ensure that the reachability works for each case.
 
diff --git a/tests/kani/UnsizedCoercion/box_outer_coercion.rs b/tests/kani/UnsizedCoercion/box_outer_coercion.rs
index 586f54003cdf..2d91360cd576 100644
--- a/tests/kani/UnsizedCoercion/box_outer_coercion.rs
+++ b/tests/kani/UnsizedCoercion/box_outer_coercion.rs
@@ -1,6 +1,5 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: --mir-linker --enable-unstable
 //! Check the basic coercion when using boxes.
 //! Tests are broken down into different crates to ensure that the reachability works for each case.
 mod defs;
diff --git a/tests/kani/UnsizedCoercion/custom_outer_coercion.rs b/tests/kani/UnsizedCoercion/custom_outer_coercion.rs
index 7f7d68ef6e84..6d75204223c1 100644
--- a/tests/kani/UnsizedCoercion/custom_outer_coercion.rs
+++ b/tests/kani/UnsizedCoercion/custom_outer_coercion.rs
@@ -1,6 +1,5 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: --mir-linker --enable-unstable
 //! Check the basic coercion when using a custom CoerceUnsized implementation.
 //! Tests are broken down into different crates to ensure that the reachability works for each case.
 #![feature(coerce_unsized)]
diff --git a/tests/kani/UnsizedCoercion/double_coercion.rs b/tests/kani/UnsizedCoercion/double_coercion.rs
index 26cfb585821e..76158c811c00 100644
--- a/tests/kani/UnsizedCoercion/double_coercion.rs
+++ b/tests/kani/UnsizedCoercion/double_coercion.rs
@@ -1,6 +1,5 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: --mir-linker --enable-unstable
 //! Check the basic coercion when using box of box.
 //! Tests are broken down into different crates to ensure that the reachability works for each case.
 
diff --git a/tests/kani/UnsizedCoercion/rc_outer_coercion.rs b/tests/kani/UnsizedCoercion/rc_outer_coercion.rs
index 2543498cca80..7a608d7d1d57 100644
--- a/tests/kani/UnsizedCoercion/rc_outer_coercion.rs
+++ b/tests/kani/UnsizedCoercion/rc_outer_coercion.rs
@@ -1,6 +1,5 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: --mir-linker --enable-unstable
 //! Check the basic coercion from using reference counter.
 //! Tests are broken down into different crates to ensure that the reachability works for each case.
 mod defs;
diff --git a/tests/kani/UnsizedCoercion/trait_to_trait_coercion.rs b/tests/kani/UnsizedCoercion/trait_to_trait_coercion.rs
index 32875f8b8e22..b7750db487e2 100644
--- a/tests/kani/UnsizedCoercion/trait_to_trait_coercion.rs
+++ b/tests/kani/UnsizedCoercion/trait_to_trait_coercion.rs
@@ -1,6 +1,5 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: --mir-linker --enable-unstable
 //! Check the basic coercion from using built-in references and pointers.
 //! Tests are broken down into different crates to ensure that the reachability works for each case.
 
diff --git a/tests/perf/string/src/any_str.rs b/tests/perf/string/src/any_str.rs
index 3b58d56750a7..6b3f9cffbc37 100644
--- a/tests/perf/string/src/any_str.rs
+++ b/tests/perf/string/src/any_str.rs
@@ -1,10 +1,5 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-//
-// kani-flags: --enable-unstable --mir-linker
-//
-//! This test is to check MIR linker state of the art.
-//! I.e.: Currently, this should fail with missing function definition.
 
 #[kani::proof]
 #[kani::unwind(4)]
diff --git a/tests/slow/kani/Strings/copy_empty_string_by_intrinsic.rs b/tests/slow/kani/Strings/copy_empty_string_by_intrinsic.rs
index a0c1bef7d003..596bedaa7825 100644
--- a/tests/slow/kani/Strings/copy_empty_string_by_intrinsic.rs
+++ b/tests/slow/kani/Strings/copy_empty_string_by_intrinsic.rs
@@ -1,7 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// kani-flags: --enable-unstable --mir-linker
 //! Make sure we can handle explicit copy_nonoverlapping on empty string
 //! This used to trigger an issue: https://github.com/model-checking/kani/issues/241
 
diff --git a/tests/ui/mir-linker/generic-harness/incorrect.rs b/tests/ui/mir-linker/generic-harness/incorrect.rs
index e68eba6ec834..e52b06801517 100644
--- a/tests/ui/mir-linker/generic-harness/incorrect.rs
+++ b/tests/ui/mir-linker/generic-harness/incorrect.rs
@@ -1,8 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-// kani-flags: --enable-unstable --mir-linker
-//
 //! Checks that we correctly fail if the harness is a generic function.
 
 #[kani::proof]

From 68387e4cf462541028892772d2fc12da8abd6a6c Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Wed, 2 Oct 2024 14:01:39 -0400
Subject: [PATCH 3/4] Enable doctests to avoid coding mistakes in our API
 documentation (#3557)

In order to enable the tests, I had to fix a few tests, enhance tests
with hidden code, and mark a few as `no_run` instead of `rust`.

The tests marked as `no_run` will at least compile, but we cannot
execute them otherwise execution would
be stuck in an infinite loop, since we provide dummy implementation
to a lot of our intrinsics with `loop {}`.

Finally, as I was cleaning up the documentation, I noticed that we
accidently published an API that was meant to be internal to Kani.
I marked this API as deprecated for now.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
---
 library/kani/src/contracts.rs                 | 43 ++++++--
 library/kani/src/invariant.rs                 | 33 ++++++-
 library/kani/src/lib.rs                       |  2 +
 library/kani/src/shadow.rs                    |  2 +-
 library/kani/src/slice.rs                     |  3 +-
 library/kani_core/src/lib.rs                  | 98 +++++++++++++------
 scripts/kani-regression.sh                    |  4 +-
 .../deprecated_warning.expected               |  1 +
 .../ui/check_deprecated/deprecated_warning.rs | 10 ++
 9 files changed, 152 insertions(+), 44 deletions(-)
 create mode 100644 tests/ui/check_deprecated/deprecated_warning.expected
 create mode 100644 tests/ui/check_deprecated/deprecated_warning.rs

diff --git a/library/kani/src/contracts.rs b/library/kani/src/contracts.rs
index beddd7cc580e..2dc2bd2a4957 100644
--- a/library/kani/src/contracts.rs
+++ b/library/kani/src/contracts.rs
@@ -25,7 +25,7 @@
 //! simple division function `my_div`:
 //!
 //! ```
-//! fn my_div(dividend: u32, divisor: u32) -> u32 {
+//! fn my_div(dividend: usize, divisor: usize) -> usize {
 //!   dividend / divisor
 //! }
 //! ```
@@ -35,8 +35,12 @@
 //! allows us to declare constraints on what constitutes valid inputs to our
 //! function. In this case we would want to disallow a divisor that is `0`.
 //!
-//! ```ignore
+//! ```
+//! # use kani::requires;
 //! #[requires(divisor != 0)]
+//! # fn my_div(dividend: usize, divisor: usize) -> usize {
+//! #  dividend / divisor
+//! # }
 //! ```
 //!
 //! This is called a precondition, because it is enforced before (pre-) the
@@ -51,7 +55,11 @@
 //! approximation of the result of division for instance could be this:
 //!
 //! ```
-//! #[ensures(|result : &u32| *result <= dividend)]
+//! # use kani::ensures;
+//! #[ensures(|result : &usize| *result <= dividend)]
+//! # fn my_div(dividend: usize, divisor: usize) -> usize {
+//! #  dividend / divisor
+//! # }
 //! ```
 //!
 //! This is called a postcondition and it also has access to the arguments and
@@ -66,9 +74,11 @@
 //! order does not matter. In our example putting them together looks like this:
 //!
 //! ```
-//! #[kani::requires(divisor != 0)]
-//! #[kani::ensures(|result : &u32| *result <= dividend)]
-//! fn my_div(dividend: u32, divisor: u32) -> u32 {
+//! use kani::{requires, ensures};
+//!
+//! #[requires(divisor != 0)]
+//! #[ensures(|result : &usize| *result <= dividend)]
+//! fn my_div(dividend: usize, divisor: usize) -> usize {
 //!   dividend / divisor
 //! }
 //! ```
@@ -84,9 +94,18 @@
 //! function we want to check.
 //!
 //! ```
+//! # use kani::{requires, ensures};
+//! #
+//! # #[requires(divisor != 0)]
+//! # #[ensures(|result : &usize| *result <= dividend)]
+//! # fn my_div(dividend: usize, divisor: usize) -> usize {
+//! #   dividend / divisor
+//! # }
+//! #
 //! #[kani::proof_for_contract(my_div)]
 //! fn my_div_harness() {
-//!     my_div(kani::any(), kani::any()) }
+//!     my_div(kani::any(), kani::any());
+//! }
 //! ```
 //!
 //! The harness is checked like any other by running `cargo kani` and can be
@@ -104,10 +123,18 @@
 //! the contract will be used automatically.
 //!
 //! ```
+//! # use kani::{requires, ensures};
+//! #
+//! # #[requires(divisor != 0)]
+//! # #[ensures(|result : &usize| *result <= dividend)]
+//! # fn my_div(dividend: usize, divisor: usize) -> usize {
+//! #   dividend / divisor
+//! # }
+//! #
 //! #[kani::proof]
 //! #[kani::stub_verified(my_div)]
 //! fn use_div() {
-//!   let v = vec![...];
+//!   let v = kani::vec::any_vec::<char, 5>();
 //!   let some_idx = my_div(v.len() - 1, 3);
 //!   v[some_idx];
 //! }
diff --git a/library/kani/src/invariant.rs b/library/kani/src/invariant.rs
index 068cdedc277e..b1bac031b677 100644
--- a/library/kani/src/invariant.rs
+++ b/library/kani/src/invariant.rs
@@ -39,6 +39,14 @@
 /// ```
 /// You can specify its safety invariant as:
 /// ```rust
+/// # #[derive(kani::Arbitrary)]
+/// # pub struct MyDate {
+/// #  day: u8,
+/// #  month: u8,
+/// #  year: i64,
+/// # }
+/// # fn days_in_month(_: i64, _: u8) -> u8 { 31 }
+///
 /// impl kani::Invariant for MyDate {
 ///   fn is_safe(&self) -> bool {
 ///     self.month > 0
@@ -49,12 +57,33 @@
 /// }
 /// ```
 /// And use it to check that your APIs are safe:
-/// ```rust
+/// ```no_run
+/// # use kani::Invariant;
+/// #
+/// # #[derive(kani::Arbitrary)]
+/// # pub struct MyDate {
+/// #  day: u8,
+/// #  month: u8,
+/// #  year: i64,
+/// # }
+/// #
+/// # fn days_in_month(_: i64, _: u8) -> u8 { todo!() }
+/// # fn increase_date(_: &mut MyDate, _: u8) { todo!() }
+/// #
+/// # impl Invariant for MyDate {
+/// #   fn is_safe(&self) -> bool {
+/// #     self.month > 0
+/// #       && self.month <= 12
+/// #       && self.day > 0
+/// #       && self.day <= days_in_month(self.year, self.month)
+/// #   }
+/// # }
+/// #
 /// #[kani::proof]
 /// fn check_increase_date() {
 ///   let mut date: MyDate = kani::any();
 ///   // Increase date by one day
-///   increase_date(date, 1);
+///   increase_date(&mut date, 1);
 ///   assert!(date.is_safe());
 /// }
 /// ```
diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs
index 053af760067b..ce1eeb992121 100644
--- a/library/kani/src/lib.rs
+++ b/library/kani/src/lib.rs
@@ -19,6 +19,8 @@
 #![feature(ptr_metadata)]
 #![feature(f16)]
 #![feature(f128)]
+// Need to add this since we are deprecating `kani::check`. Remove this when we remove that API.
+#![allow(deprecated)]
 
 // Allow us to use `kani::` to access crate features.
 extern crate self as kani;
diff --git a/library/kani/src/shadow.rs b/library/kani/src/shadow.rs
index a7ea57c6fd40..48ce8f0f9211 100644
--- a/library/kani/src/shadow.rs
+++ b/library/kani/src/shadow.rs
@@ -10,7 +10,7 @@
 //!
 //! # Example
 //!
-//! ```
+//! ```no_run
 //! use kani::shadow::ShadowMem;
 //! use std::alloc::{alloc, Layout};
 //!
diff --git a/library/kani/src/slice.rs b/library/kani/src/slice.rs
index 1b13de29d589..c419a881fa55 100644
--- a/library/kani/src/slice.rs
+++ b/library/kani/src/slice.rs
@@ -9,7 +9,8 @@ use crate::{any, assume};
 ///
 /// # Example:
 ///
-/// ```rust
+/// ```no_run
+/// # fn foo(_: &[i32]) {}
 /// let arr = [1, 2, 3];
 /// let slice = kani::slice::any_slice_of_array(&arr);
 /// foo(slice); // where foo is a function that takes a slice and verifies a property about it
diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs
index 5df8f2228c62..839313f084c2 100644
--- a/library/kani_core/src/lib.rs
+++ b/library/kani_core/src/lib.rs
@@ -42,6 +42,7 @@ macro_rules! kani_lib {
             pub use kani_core::*;
             kani_core::kani_intrinsics!(core);
             kani_core::generate_arbitrary!(core);
+            kani_core::check_intrinsic!();
 
             pub mod mem {
                 kani_core::kani_mem!(core);
@@ -58,6 +59,10 @@ macro_rules! kani_lib {
         kani_core::kani_intrinsics!(std);
         kani_core::generate_arbitrary!(std);
 
+        kani_core::check_intrinsic! {
+            msg="This API will be made private in future releases.", vis=pub
+        }
+
         pub mod mem {
             kani_core::kani_mem!(std);
         }
@@ -85,7 +90,7 @@ macro_rules! kani_intrinsics {
         ///
         /// The code snippet below should never panic.
         ///
-        /// ```rust
+        /// ```no_run
         /// let i : i32 = kani::any();
         /// kani::assume(i > 10);
         /// if i < 0 {
@@ -95,7 +100,7 @@ macro_rules! kani_intrinsics {
         ///
         /// The following code may panic though:
         ///
-        /// ```rust
+        /// ```no_run
         /// let i : i32 = kani::any();
         /// assert!(i < 0, "This may panic and verification should fail.");
         /// kani::assume(i > 10);
@@ -118,7 +123,7 @@ macro_rules! kani_intrinsics {
         ///
         /// # Example:
         ///
-        /// ```rust
+        /// ```no_run
         /// let x: bool = kani::any();
         /// let y = !x;
         /// kani::assert(x || y, "ORing a boolean variable with its negation must be true")
@@ -138,35 +143,15 @@ macro_rules! kani_intrinsics {
             assert!(cond, "{}", msg);
         }
 
-        /// Creates an assertion of the specified condition and message, but does not assume it afterwards.
-        ///
-        /// # Example:
-        ///
-        /// ```rust
-        /// let x: bool = kani::any();
-        /// let y = !x;
-        /// kani::check(x || y, "ORing a boolean variable with its negation must be true")
-        /// ```
-        #[cfg(not(feature = "concrete_playback"))]
-        #[inline(never)]
-        #[rustc_diagnostic_item = "KaniCheck"]
-        pub const fn check(cond: bool, msg: &'static str) {
-            let _ = cond;
-            let _ = msg;
-        }
-
-        #[cfg(feature = "concrete_playback")]
-        #[inline(never)]
-        #[rustc_diagnostic_item = "KaniCheck"]
-        pub const fn check(cond: bool, msg: &'static str) {
-            assert!(cond, "{}", msg);
-        }
-
         /// Creates a cover property with the specified condition and message.
         ///
         /// # Example:
         ///
-        /// ```rust
+        /// ```no_run
+        /// # use crate::kani;
+        /// #
+        /// # let array: [u8; 10]  = kani::any();
+        /// # let slice = kani::slice::any_slice_of_array(&array);
         /// kani::cover(slice.len() == 0, "The slice may have a length of 0");
         /// ```
         ///
@@ -193,7 +178,11 @@ macro_rules! kani_intrinsics {
         /// In the snippet below, we are verifying the behavior of the function `fn_under_verification`
         /// under all possible `NonZeroU8` input values, i.e., all possible `u8` values except zero.
         ///
-        /// ```rust
+        /// ```no_run
+        /// # use std::num::NonZeroU8;
+        /// # use crate::kani;
+        /// #
+        /// # fn fn_under_verification(_: NonZeroU8) {}
         /// let inputA = kani::any::<core::num::NonZeroU8>();
         /// fn_under_verification(inputA);
         /// ```
@@ -231,7 +220,11 @@ macro_rules! kani_intrinsics {
         /// In the snippet below, we are verifying the behavior of the function `fn_under_verification`
         /// under all possible `u8` input values between 0 and 12.
         ///
-        /// ```rust
+        /// ```no_run
+        /// # use std::num::NonZeroU8;
+        /// # use crate::kani;
+        /// #
+        /// # fn fn_under_verification(_: u8) {}
         /// let inputA: u8 = kani::any_where(|x| *x < 12);
         /// fn_under_verification(inputA);
         /// ```
@@ -460,3 +453,48 @@ macro_rules! kani_intrinsics {
         }
     };
 }
+
+#[macro_export]
+macro_rules! check_intrinsic {
+    ($(msg=$msg:literal, vis=$vis:vis)?) => {
+        /// Creates a non-fatal property with the specified condition and message.
+        ///
+        /// This check will not impact the program control flow even when it fails.
+        ///
+        /// # Example:
+        ///
+        /// ```no_run
+        /// let x: bool = kani::any();
+        /// let y = !x;
+        /// kani::check(x || y, "ORing a boolean variable with its negation must be true");
+        /// kani::check(x == y, "A boolean variable is always different than its negation");
+        /// kani::cover!(true, "This should still be reachable");
+        /// ```
+        ///
+        /// # Deprecated
+        ///
+        /// This function was meant to be internal only, and it was added to Kani's public interface
+        /// by mistake. Thus, it will be made private in future releases.
+        /// Instead, we recommend users to either use `assert` or `cover` to create properties they
+        /// would like to verify.
+        ///
+        /// See <https://github.com/model-checking/kani/issues/3561> for more details.
+        #[cfg(not(feature = "concrete_playback"))]
+        #[inline(never)]
+        #[rustc_diagnostic_item = "KaniCheck"]
+        // TODO: Remove the `#![allow(deprecated)]` inside kani's crate once this is made private.
+        $(#[deprecated(since="0.55.0", note=$msg)])?
+        $($vis)? const fn check(cond: bool, msg: &'static str) {
+            let _ = cond;
+            let _ = msg;
+        }
+
+        #[cfg(feature = "concrete_playback")]
+        #[inline(never)]
+        #[rustc_diagnostic_item = "KaniCheck"]
+        $(#[deprecated(since="0.55.0", note=$msg)])?
+        $($vis)? const fn check(cond: bool, msg: &'static str) {
+            assert!(cond, "{}", msg);
+        }
+    };
+}
diff --git a/scripts/kani-regression.sh b/scripts/kani-regression.sh
index bd6b04d7386e..be2548235ce6 100755
--- a/scripts/kani-regression.sh
+++ b/scripts/kani-regression.sh
@@ -41,8 +41,8 @@ cargo test -p cprover_bindings
 cargo test -p kani-compiler
 cargo test -p kani-driver
 cargo test -p kani_metadata
-# skip doc tests and enable assertions to fail
-cargo test -p kani --lib --features concrete_playback
+# Use concrete playback to enable assertions failure
+cargo test -p kani --features concrete_playback
 # Test the actual macros, skipping doc tests and enabling extra traits for "syn"
 # so we can debug print AST
 RUSTFLAGS=--cfg=kani_sysroot cargo test -p kani_macros --features syn/extra-traits --lib
diff --git a/tests/ui/check_deprecated/deprecated_warning.expected b/tests/ui/check_deprecated/deprecated_warning.expected
new file mode 100644
index 000000000000..3a0760035f8b
--- /dev/null
+++ b/tests/ui/check_deprecated/deprecated_warning.expected
@@ -0,0 +1 @@
+warning: use of deprecated function `kani::check`: This API will be made private in future releases.
diff --git a/tests/ui/check_deprecated/deprecated_warning.rs b/tests/ui/check_deprecated/deprecated_warning.rs
new file mode 100644
index 000000000000..f3d791256081
--- /dev/null
+++ b/tests/ui/check_deprecated/deprecated_warning.rs
@@ -0,0 +1,10 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// kani-flags: --only-codegen
+
+/// Ensure that Kani prints a deprecation warning if users invoke `kani::check`.
+#[kani::proof]
+fn internal_api() {
+    kani::check(kani::any(), "oops");
+}

From f3ed5e80fb24e2e8256244b93657bb99821eaaff Mon Sep 17 00:00:00 2001
From: "github-actions[bot]"
 <41898282+github-actions[bot]@users.noreply.github.com>
Date: Thu, 3 Oct 2024 09:22:55 -0400
Subject: [PATCH 4/4] Automatic toolchain upgrade to nightly-2024-10-03 (#3564)

Update Rust toolchain from nightly-2024-10-02 to nightly-2024-10-03
without any other source changes.

Co-authored-by: celinval <35149715+celinval@users.noreply.github.com>
---
 rust-toolchain.toml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index bd0b55ef531f..7ef640dbfdc9 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2024-10-02"
+channel = "nightly-2024-10-03"
 components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]