Skip to content

Commit 88e434d

Browse files
Implement Arbitrary manually
The implementations need a stability attribute. Co-authored-by: Michael Tautschnig <[email protected]>
1 parent 1f20a2b commit 88e434d

File tree

2 files changed

+16
-2
lines changed

2 files changed

+16
-2
lines changed

library/core/src/num/saturating.rs

+8-1
Original file line numberDiff line numberDiff line change
@@ -35,9 +35,16 @@ use crate::ops::{
3535
#[derive(PartialEq, Eq, PartialOrd, Ord, Clone, Copy, Default, Hash)]
3636
#[repr(transparent)]
3737
#[rustc_diagnostic_item = "Saturating"]
38-
#[cfg_attr(kani, derive(kani::Arbitrary))]
3938
pub struct Saturating<T>(#[stable(feature = "saturating_int_impl", since = "1.74.0")] pub T);
4039

40+
#[cfg(kani)]
41+
#[stable(feature = "saturating_int_impl", since = "1.74.0")]
42+
impl<T: kani::Arbitrary> kani::Arbitrary for Saturating<T> {
43+
fn any() -> Self {
44+
Self { 0: kani::any() }
45+
}
46+
}
47+
4148
#[stable(feature = "saturating_int_impl", since = "1.74.0")]
4249
impl<T: fmt::Debug> fmt::Debug for Saturating<T> {
4350
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {

library/core/src/num/wrapping.rs

+8-1
Original file line numberDiff line numberDiff line change
@@ -40,9 +40,16 @@ use crate::ops::{
4040
#[derive(PartialEq, Eq, PartialOrd, Ord, Clone, Copy, Default, Hash)]
4141
#[repr(transparent)]
4242
#[rustc_diagnostic_item = "Wrapping"]
43-
#[cfg_attr(kani, derive(kani::Arbitrary))]
4443
pub struct Wrapping<T>(#[stable(feature = "rust1", since = "1.0.0")] pub T);
4544

45+
#[cfg(kani)]
46+
#[stable(feature = "rust1", since = "1.0.0")]
47+
impl<T: kani::Arbitrary> kani::Arbitrary for Wrapping<T> {
48+
fn any() -> Self {
49+
Self { 0: kani::any() }
50+
}
51+
}
52+
4653
#[stable(feature = "rust1", since = "1.0.0")]
4754
impl<T: fmt::Debug> fmt::Debug for Wrapping<T> {
4855
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {

0 commit comments

Comments
 (0)