Address PR comments

celinval · Oct 2, 2024 · ffa99a5 · ffa99a5
1 parent 142f8d8
commit ffa99a5
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 4 deletions.
diff --git 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
@@ -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 <https://github.com/model-checking/kani/issues/3561> 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
@@ -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.