Derive macro for kani::Arbitrary
does not work on enums with a single variant. #3691
Closed
Description
I tried this code:
#[cfg_attr(kani, derive(kani::Arbitrary))]
enum Example {
Variant,
}
using the following command line invocation:
kani example.rs
with Kani version: 0.56.0
I expected to see this happen: the file compiles successfully.
Instead, the derived implementation of kani::Arbitrary
does not compile successfully:
Kani Rust Verifier 0.56.0 (standalone)
error[E0283]: type annotations needed
--> example.rs:1:25
|
1 | #[cfg_attr(kani, derive(kani::Arbitrary))]
| ^^^^^^^^^^^^^^^ cannot infer type
|
= note: cannot satisfy `_: kani::Arbitrary`
= help: the following 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 45 others
note: required by a bound in `kani::any`
--> /Users/runner/work/kani/kani/library/kani/src/lib.rs:55:1
= note: this error originates in the derive macro `kani::Arbitrary` which comes from the expansion of the macro `kani_core::kani_lib` (in Nightly builds, run with -Z macro-backtrace for more info)