diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index d827af6136..3e234368c1 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -323,7 +323,7 @@ jobs: 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" # This version is automatically rolled by # `roll-pinned-toolchain-versions.yml`. - 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;