Address comments

model-checking · Nov 2, 2024 · 1fbd5d8 · 1fbd5d8
1 parent a850f63
commit 1fbd5d8
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 18 deletions.
diff --git a/library/kani/tests/ops.rs b/library/kani/tests/ops.rs
@@ -0,0 +1,9 @@
+use core::ops::{Bound, Range, RangeFrom, RangeInclusive, RangeTo, RangeToInclusive};
+
+fn _has_range_implementations() {
+    let _: Bound<u8> = kani::any();
+    let _: RangeFrom<u8> = kani::any();
+    let _: RangeInclusive<u8> = kani::any();
+    let _: RangeTo<u8> = kani::any();
+    let _: RangeToInclusive<u8> = kani::any();
+}
diff --git a/library/kani_core/src/arbitrary.rs b/library/kani_core/src/arbitrary.rs
@@ -208,7 +208,7 @@ macro_rules! generate_arbitrary {
                 T: Arbitrary,
             {
                 fn any() -> Self {
-                    match u8::any() % 3 {
+                    match u8::any() {
                         0 => Bound::Included(T::any()),
                         1 => Bound::Excluded(T::any()),
                         _ => Bound::Unbounded,
@@ -218,12 +218,10 @@ macro_rules! generate_arbitrary {
 
             impl<T> Arbitrary for Range<T>
             where
-                T: Arbitrary + PartialOrd,
+                T: Arbitrary,
             {
                 fn any() -> Self {
-                    let (mut first, mut second) = (T::any(), T::any());
-                    adjust(&mut first, &mut second);
-                    first..second
+                    T::any()..T::any()
                 }
             }
 
@@ -238,12 +236,10 @@ macro_rules! generate_arbitrary {
 
             impl<T> Arbitrary for RangeInclusive<T>
             where
-                T: Arbitrary + PartialOrd,
+                T: Arbitrary,
             {
                 fn any() -> Self {
-                    let (mut first, mut second) = (T::any(), T::any());
-                    adjust(&mut first, &mut second);
-                    first..=second
+                    T::any()..=T::any()
                 }
             }
 
@@ -264,15 +260,6 @@ macro_rules! generate_arbitrary {
                     ..=T::any()
                 }
             }
-
-            fn adjust<T>(first: &mut T, second: &mut T)
-            where
-                T: PartialOrd,
-            {
-                if first > second {
-                    mem::swap(first, second);
-                }
-            }
         }
     };
 }