diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 217db76767..042a38affb 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -322,7 +322,7 @@ jobs: # specifying a particular toolchain. args: "--package zerocopy --features __internal_use_only_features_that_work_on_stable --output-format=terse --randomize-layout --memory-safety-checks --overflow-checks --undefined-function-checks --unwinding-checks" # TODO(#929): Either roll this automatically or don't pin. - kani-version: 0.46.0 + kani-version: 0.47.0 check_fmt: runs-on: ubuntu-latest diff --git a/src/byteorder.rs b/src/byteorder.rs index f433775c36..5d36c0a2fd 100644 --- a/src/byteorder.rs +++ b/src/byteorder.rs @@ -889,17 +889,25 @@ mod tests { rng.sample(Self::DIST) } - #[cfg(kani)] - fn any() -> Self { - kani::any() - } - + #[cfg_attr(kani, allow(unused))] fn checked_add(self, rhs: Self) -> Option; + + #[cfg_attr(kani, allow(unused))] fn checked_div(self, rhs: Self) -> Option; + + #[cfg_attr(kani, allow(unused))] fn checked_mul(self, rhs: Self) -> Option; + + #[cfg_attr(kani, allow(unused))] fn checked_rem(self, rhs: Self) -> Option; + + #[cfg_attr(kani, allow(unused))] fn checked_sub(self, rhs: Self) -> Option; + + #[cfg_attr(kani, allow(unused))] fn checked_shl(self, rhs: Self) -> Option; + + #[cfg_attr(kani, allow(unused))] fn checked_shr(self, rhs: Self) -> Option; fn is_nan(self) -> bool;