diff --git a/library/kani/src/arbitrary.rs b/library/kani/src/arbitrary.rs index 2e13f90e3aef..2d89e7084d36 100644 --- a/library/kani/src/arbitrary.rs +++ b/library/kani/src/arbitrary.rs @@ -161,3 +161,12 @@ impl Arbitrary for std::marker::PhantomPinned { PhantomPinned } } + +impl Arbitrary for std::boxed::Box +where + T: Arbitrary, +{ + fn any() -> Self { + Box::new(T::any()) + } +} diff --git a/tests/expected/derive-arbitrary/box/expected b/tests/expected/derive-arbitrary/box/expected new file mode 100644 index 000000000000..4cef537ffd6a --- /dev/null +++ b/tests/expected/derive-arbitrary/box/expected @@ -0,0 +1,11 @@ +Status: SATISFIED\ +Description: "cover condition: *foo.boxed == i32::MIN" +Status: SATISFIED\ +Description: "cover condition: *foo.boxed == 0" +Status: SATISFIED\ +Description: "cover condition: *foo.boxed == i32::MAX" +Status: UNSATISFIABLE\ +Description: "cover condition: *foo.boxed < i32::MIN" +Status: UNSATISFIABLE\ +Description: "cover condition: *foo.boxed > i32::MAX" +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/derive-arbitrary/box/test.rs b/tests/expected/derive-arbitrary/box/test.rs new file mode 100644 index 000000000000..f3e95115a6d4 --- /dev/null +++ b/tests/expected/derive-arbitrary/box/test.rs @@ -0,0 +1,20 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check that Kani can automatically derive `Arbitrary` on a struct with a +//! member of type `Box` + +#[derive(kani::Arbitrary)] +struct Foo { + boxed: Box, +} + +#[kani::proof] +fn main() { + let foo: Foo = kani::any(); + kani::cover!(*foo.boxed == i32::MIN); + kani::cover!(*foo.boxed == 0); + kani::cover!(*foo.boxed == i32::MAX); + kani::cover!(*foo.boxed < i32::MIN); // <-- this condition should be `UNSATISFIABLE` + kani::cover!(*foo.boxed > i32::MAX); // <-- this condition should be `UNSATISFIABLE` +} diff --git a/tests/ui/derive-arbitrary/phantom_data/expected b/tests/expected/derive-arbitrary/phantom_data/expected similarity index 100% rename from tests/ui/derive-arbitrary/phantom_data/expected rename to tests/expected/derive-arbitrary/phantom_data/expected diff --git a/tests/ui/derive-arbitrary/phantom_data/test.rs b/tests/expected/derive-arbitrary/phantom_data/test.rs similarity index 100% rename from tests/ui/derive-arbitrary/phantom_data/test.rs rename to tests/expected/derive-arbitrary/phantom_data/test.rs diff --git a/tests/ui/derive-arbitrary/phantom_pinned/expected b/tests/expected/derive-arbitrary/phantom_pinned/expected similarity index 100% rename from tests/ui/derive-arbitrary/phantom_pinned/expected rename to tests/expected/derive-arbitrary/phantom_pinned/expected diff --git a/tests/ui/derive-arbitrary/phantom_pinned/test.rs b/tests/expected/derive-arbitrary/phantom_pinned/test.rs similarity index 100% rename from tests/ui/derive-arbitrary/phantom_pinned/test.rs rename to tests/expected/derive-arbitrary/phantom_pinned/test.rs