Add ensures for unchecked_neg && Fix import

model-checking · Oct 8, 2024 · cb99f76 · cb99f76
1 parent 5e1c45f
commit cb99f76
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git a/library/core/src/num/int_macros.rs b/library/core/src/num/int_macros.rs
@@ -1168,6 +1168,7 @@ macro_rules! int_impl {
         #[inline(always)]
         #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
         #[requires(self != $SelfT::MIN)]
+        #[ensures(|result| *result == -self)]
         pub const unsafe fn unchecked_neg(self) -> Self {
             assert_unsafe_precondition!(
                 check_language_ub,

diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs
@@ -5,7 +5,7 @@
 use crate::str::FromStr;
 use crate::ub_checks::assert_unsafe_precondition;
 use crate::{ascii, intrinsics, mem};
-use safety::requires;
+use safety::{requires, ensures};
 
 #[cfg(kani)]
 use crate::kani;