generated from amazon-archives/__template_Apache-2.0
-
Notifications
You must be signed in to change notification settings - Fork 129
Closed
Labels
T-UserTag user issues / requestsTag user issues / requests[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.
Description
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
Labels
T-UserTag user issues / requestsTag user issues / requests[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.