From c5345295114010af7d16977ac58c90b5538114b4 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 21 Aug 2024 12:06:14 +0200 Subject: [PATCH] Update library/core/src/alloc/layout.rs Co-authored-by: Celina G. Val --- library/core/src/alloc/layout.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/core/src/alloc/layout.rs b/library/core/src/alloc/layout.rs index b23ed074c1c66..f8830ec437fad 100644 --- a/library/core/src/alloc/layout.rs +++ b/library/core/src/alloc/layout.rs @@ -346,8 +346,8 @@ impl Layout { #[unstable(feature = "alloc_layout_extra", issue = "55724")] #[inline] // the below modulo operation might be too costly to prove - // #[ensures(|result| result.is_err() || n == 0 || result.as_ref().unwrap().0.size() % n == 0)] - #[ensures(|result| result.is_err() || n == 0 || result.as_ref().unwrap().0.size() >= self.size())] + #[cfg_attr(not(kani), ensures(|result| result.is_err() || n == 0 || result.as_ref().unwrap().0.size() % n == 0))] + #[cfg_attr(kani, ensures(|result| result.is_err() || n == 0 || result.as_ref().unwrap().0.size() >= self.size()))] // the below multiplication might be too costly to prove at this time // #[ensures(|result| result.is_err() || result.as_ref().unwrap().0.size() == n * result.as_ref().unwrap().1)] // use the weaker statement below for now