Skip to content

Deriving BoundedArbitrary fails for enum with one variant #4170

@zhassan-aws

Description

@zhassan-aws

I tried this code:

#[derive(kani::BoundedArbitrary)]
enum Foo {
    A(#[bounded] String),
    //B(#[bounded] String),
}

#[kani::proof]
fn check_enum() {
    let _foo = kani::bounded_any::<Foo, 4>();
}

using the following command line invocation:

kani bounded_enum.rs

with Kani version: 37fb634

I expected to see this happen: Verification successful

Instead, this happened:

 $ kani bounded_enum.rs 
Kani Rust Verifier 0.63.0 (standalone)
error[E0283]: type annotations needed
  --> bounded_enum.rs:1:10
   |
1  | #[derive(kani::BoundedArbitrary)]
   |          ^^^^^^^^^^^^^^^^^^^^^^ 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 50 others
note: required by a bound in `kani::any`
  --> /home/ubuntu/git/kani/library/kani/src/lib.rs:55:1
   |
55 | kani_core::kani_lib!(kani);
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^ required by this bound in `any`
   = note: this error originates in the derive macro `kani::BoundedArbitrary` which comes from the expansion of the macro `kani_core::kani_lib` (in Nightly builds, run with -Z macro-backtrace for more info)

error: aborting due to 1 previous error

For more information about this error, try `rustc --explain E0283`.
error: /home/ubuntu/git/kani/target/kani/bin/kani-compiler exited with status exit status: 101

If I uncomment the second variant, verification is successful.

Metadata

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