Skip to content

Commit

Permalink
Update library/core/src/alloc/layout.rs
Browse files Browse the repository at this point in the history
Co-authored-by: Celina G. Val <celinval@amazon.com>
  • Loading branch information
tautschnig and celinval committed Aug 21, 2024
1 parent 10493b5 commit c534529
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions library/core/src/alloc/layout.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit c534529

Please sign in to comment.