[Breaking change] Make kani::check private (#3614)

In the previous release, we added a deprecation warning to `kani::check`
which was incorrectly exposed in our crate interface.

Make this private and remove the deprecation tag.

Resolves #3561

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Author: celinval

library/kani/src/lib.rs

@@ -19,8 +19,6 @@
 #![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;

library/kani_core/src/lib.rs

@@ -42,7 +42,6 @@ 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);
@@ -59,10 +58,6 @@ 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);
         }
@@ -462,51 +457,35 @@ macro_rules! kani_intrinsics {
 
             /// Stub the body with its contract.
             pub const REPLACE: Mode = 3;
-        }
-    };
-}
 
-#[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;
-        }
+            /// 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");
+            /// ```
+            ///
+            #[cfg(not(feature = "concrete_playback"))]
+            #[inline(never)]
+            #[rustc_diagnostic_item = "KaniCheck"]
+            pub(crate) 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);
+            #[cfg(feature = "concrete_playback")]
+            #[inline(never)]
+            #[rustc_diagnostic_item = "KaniCheck"]
+            pub(crate) const fn check(cond: bool, msg: &'static str) {
+                assert!(cond, "{}", msg);
+            }
         }
     };
 }

library/kani_core/src/mem.rs

@@ -327,7 +327,7 @@ macro_rules! kani_mem {
 
         /// A helper to assert `is_initialized` to use it as a part of other predicates.
         fn assert_is_initialized<T: ?Sized>(ptr: *const T) -> bool {
-            super::check(
+            super::internal::check(
                 is_initialized(ptr),
                 "Undefined Behavior: Reading from an uninitialized pointer",
             );