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

Feature request: Implement kani::Arbitrary for Box<T> #2403

Closed
adpaco-aws opened this issue Apr 24, 2023 · 0 comments · Fixed by #2404
Closed

Feature request: Implement kani::Arbitrary for Box<T> #2403

adpaco-aws opened this issue Apr 24, 2023 · 0 comments · Fixed by #2404
Labels
[C] Feature / Enhancement A new feature request or enhancement to an existing feature. T-User Tag user issues / requests

Comments

@adpaco-aws
Copy link
Contributor

Requested feature: Implement kani::Arbitrary for Box<T>
Use case: I'm experimenting with user code that defines a struct similar to:

struct Foo<T> {
    boxed: Box<T>,
}

If I attempt to #[derive(kani::Arbitrary)] on that struct, I get this error:

error[E0277]: the trait bound `std::boxed::Box<T>: kani::Arbitrary` is not satisfied
   --> test.rs:9:5
    |
9   |     boxed: Box<T>,
    |     ^^^^^^^^^^^^^ the trait `kani::Arbitrary` is not implemented for `std::boxed::Box<T>`
    |
    = help: the following other types implement trait `kani::Arbitrary`:
              ()
              (A, B)
              (A, B, C)
              (A, B, C, D)
              (A, B, C, D, E)
              (A, B, C, D, E, F)
              (A, B, C, D, E, F, G)
              (A, B, C, D, E, F, G, H)
            and 39 others
note: required by a bound in `kani::any`
   --> /home/ubuntu/kani/library/kani/src/lib.rs:114:15
    |
114 | pub fn any<T: Arbitrary>() -> T {
    |               ^^^^^^^^^ required by this bound in `any`

error: aborting due to previous error

Since Box<T> comes from Rust, the Kani library should implement Arbitrary for it (similar to #2224 / #2225).

@adpaco-aws adpaco-aws added [C] Feature / Enhancement A new feature request or enhancement to an existing feature. T-User Tag user issues / requests labels Apr 24, 2023
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. T-User Tag user issues / requests
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant