Skip to content

Commit d3b7763

Browse files
committed
Fix num::nonzero::NonZero::<*>::rotate_{left,right} contracts
The result of a rotate operation is always non-zero, which could still be less than zero in case of signed types. Proofs were failing with the prior contract, but this still passed CI as we haven't yet picked up the Kani version where autoharness exits with a non-zero exit code in case of proof failure.
1 parent f804a33 commit d3b7763

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

library/core/src/num/nonzero.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -755,7 +755,7 @@ macro_rules! nonzero_integer {
755755
#[must_use = "this returns the result of the operation, \
756756
without modifying the original"]
757757
#[inline(always)]
758-
#[ensures(|result| result.get() > 0)]
758+
#[ensures(|result| result.get() != 0)]
759759
#[ensures(|result| result.rotate_right(n).get() == old(self).get())]
760760
pub const fn rotate_left(self, n: u32) -> Self {
761761
let result = self.get().rotate_left(n);
@@ -790,7 +790,7 @@ macro_rules! nonzero_integer {
790790
#[must_use = "this returns the result of the operation, \
791791
without modifying the original"]
792792
#[inline(always)]
793-
#[ensures(|result| result.get() > 0)]
793+
#[ensures(|result| result.get() != 0)]
794794
#[ensures(|result| result.rotate_left(n).get() == old(self).get())]
795795
pub const fn rotate_right(self, n: u32) -> Self {
796796
let result = self.get().rotate_right(n);

0 commit comments

Comments
 (0)