Skip to content

Derive macro for kani::Arbitrary does not work on enums with a single variant. #3691

Closed
@AlgebraicWolf

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)

Metadata

Assignees

No one assigned

    Labels

    [C] BugThis is a bug. Something isn't working.

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions