Skip to content

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

@adpaco-aws

Description

@adpaco-aws

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).

Metadata

Metadata

Assignees

No one assigned

    Labels

    T-UserTag user issues / requests[C] Feature / EnhancementA new feature request or enhancement to an existing feature.

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions