Skip to content

Commit

Permalink
Implement Arbitrary for Range*
Browse files Browse the repository at this point in the history
  • Loading branch information
c410-f3r committed Oct 31, 2024
1 parent 1fe80f9 commit 9dc899e
Showing 1 changed file with 81 additions and 0 deletions.
81 changes: 81 additions & 0 deletions library/kani_core/src/arbitrary.rs
Original file line number Diff line number Diff line change
Expand Up @@ -193,6 +193,87 @@ macro_rules! generate_arbitrary {
pub mod slice {
kani_core::slice_generator!();
}

mod range_structures {
use super::{
Arbitrary,
core_path::{
mem,
ops::{Bound, Range, RangeFrom, RangeInclusive, RangeTo, RangeToInclusive},
},
};

impl<T> Arbitrary for Bound<T>
where
T: Arbitrary,
{
fn any() -> Self {
match u8::any() % 3 {
0 => Bound::Included(T::any()),
1 => Bound::Excluded(T::any()),
_ => Bound::Unbounded,
}
}
}

impl<T> Arbitrary for Range<T>
where
T: Arbitrary + PartialOrd,
{
fn any() -> Self {
let (mut first, mut second) = (T::any(), T::any());
adjust(&mut first, &mut second);
first..second
}
}

impl<T> Arbitrary for RangeFrom<T>
where
T: Arbitrary,
{
fn any() -> Self {
T::any()..
}
}

impl<T> Arbitrary for RangeInclusive<T>
where
T: Arbitrary + PartialOrd,
{
fn any() -> Self {
let (mut first, mut second) = (T::any(), T::any());
adjust(&mut first, &mut second);
first..=second
}
}

impl<T> Arbitrary for RangeTo<T>
where
T: Arbitrary,
{
fn any() -> Self {
..T::any()
}
}

impl<T> Arbitrary for RangeToInclusive<T>
where
T: Arbitrary,
{
fn any() -> Self {
..=T::any()
}
}

fn adjust<T>(first: &mut T, second: &mut T)
where
T: PartialOrd,
{
if first > second {
mem::swap(first, second);
}
}
}
};
}

Expand Down

0 comments on commit 9dc899e

Please sign in to comment.