diff --git a/library/kani/src/invariant.rs b/library/kani/src/invariant.rs index d52d2f8e3572..b1bac031b677 100644 --- a/library/kani/src/invariant.rs +++ b/library/kani/src/invariant.rs @@ -70,7 +70,7 @@ /// # fn days_in_month(_: i64, _: u8) -> u8 { todo!() } /// # fn increase_date(_: &mut MyDate, _: u8) { todo!() } /// # -/// # impl kani::Invariant for MyDate { +/// # impl Invariant for MyDate { /// # fn is_safe(&self) -> bool { /// # self.month > 0 /// # && self.month <= 12 diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs index a61fcc1368bd..839313f084c2 100644 --- a/library/kani_core/src/lib.rs +++ b/library/kani_core/src/lib.rs @@ -60,8 +60,7 @@ macro_rules! kani_lib { kani_core::generate_arbitrary!(std); kani_core::check_intrinsic! { - msg="This API was accidently added as a public function and it will be made private in future releases.", - vis=pub + msg="This API will be made private in future releases.", vis=pub } pub mod mem { @@ -478,6 +477,8 @@ macro_rules! check_intrinsic { /// 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 for more details. #[cfg(not(feature = "concrete_playback"))] #[inline(never)] #[rustc_diagnostic_item = "KaniCheck"] diff --git a/tests/ui/check_deprecated/deprecated_warning.expected b/tests/ui/check_deprecated/deprecated_warning.expected index 851d7bffb27a..3a0760035f8b 100644 --- a/tests/ui/check_deprecated/deprecated_warning.expected +++ b/tests/ui/check_deprecated/deprecated_warning.expected @@ -1 +1 @@ -warning: use of deprecated function `kani::check`: This API was accidently added as a public function and it will be made private in future releases. +warning: use of deprecated function `kani::check`: This API will be made private in future releases.