Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Implement Arbitrary for Range* #3662

Closed
c410-f3r opened this issue Oct 30, 2024 · 1 comment · Fixed by #3666
Closed

Implement Arbitrary for Range* #3662

c410-f3r opened this issue Oct 30, 2024 · 1 comment · Fixed by #3666
Labels
[C] Feature / Enhancement A new feature request or enhancement to an existing feature.

Comments

@c410-f3r
Copy link
Contributor

The Arbitrary trait is not implemented for the set of range-like structures.

  • Range
  • RangeFrom
  • RangeFull
  • RangeInclusive
  • RangeTo
  • RangeToInclusive

The lack of such a feature mandates the manual rolling of intended parameters.

#[kani::proof]
fn foo() {
let start = kani::any();
let end = kani::any();
let _ = std::ops::RangeInclusive::<u8>::new(start, end));
@c410-f3r c410-f3r added the [C] Feature / Enhancement A new feature request or enhancement to an existing feature. label Oct 30, 2024
@c410-f3r c410-f3r changed the title Implement Arbitrary for Range* Implement Arbitrary for Range* Oct 30, 2024
@zhassan-aws
Copy link
Contributor

Hi @c410-f3r. Thanks for the feature request. This shouldn't be difficult to add. If you would like to contribute the implementation, we would be happy to provide guidance.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
[C] Feature / Enhancement A new feature request or enhancement to an existing feature.
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants