diff --git a/library/core/src/num/int_macros.rs b/library/core/src/num/int_macros.rs index b7e7b2820b7be..c84087172974a 100644 --- 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 index 70218aea9cf2b..e8b7130995831 100644 --- 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;