Implement kani::Arbitrary for Box<T>

library/kani/src/arbitrary.rs

@@ -161,3 +161,12 @@ impl Arbitrary for std::marker::PhantomPinned {
         PhantomPinned
     }
 }
+
+impl<T> Arbitrary for std::boxed::Box<T>
+where
+    T: Arbitrary,
+{
+    fn any() -> Self {
+        Box::new(T::any())
+    }
+}

tests/expected/derive-arbitrary/box/expected

@@ -0,0 +1,7 @@
+Status: SATISFIED\
+Description: "cover condition: *foo.boxed >= i32::MIN && *foo.boxed <= i32::MAX"
+Status: UNSATISFIABLE\
+Description: "cover condition: *foo.boxed < i32::MIN"
+Status: UNSATISFIABLE\
+Description: "cover condition: *foo.boxed > i32::MAX"
+VERIFICATION:- SUCCESSFUL

tests/expected/derive-arbitrary/box/test.rs

@@ -0,0 +1,18 @@
+// 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<T>`
+
+#[derive(kani::Arbitrary)]
+struct Foo<T> {
+    boxed: Box<T>,
+}
+
+#[kani::proof]
+fn main() {
+    let foo: Foo<i32> = kani::any();
+    kani::cover!(*foo.boxed >= i32::MIN && *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`
+}