Skip to content

Deriving BoundedArbitrary fails with generic type defaults #4116

@zhassan-aws

Description

@zhassan-aws

I tried this code:

#[derive(kani::BoundedArbitrary)]
pub struct Foo<T = i32> {
    #[bounded]
    v: Vec<T>,
}

#[kani::proof]
fn main() {
    let f: Foo<u8> = kani::bounded_any::<_, 16>();
    assert!(f.v.len() <= 16);
}

using the following command line invocation:

kani ba.rs

with Kani version: a0f9364

I expected to see this happen: Verification succeeds

Instead, this happened:

$ kani ba.rs 
Kani Rust Verifier 0.62.0 (standalone)
error: expected one of `!`, `(`, `+`, `,`, `::`, `<`, or `{`, found `:`
 --> ba.rs:1:10
  |
1 | #[derive(kani::BoundedArbitrary)]
  |          ^^^^^^^^^^^^^^^^^^^^^^ expected one of 7 possible tokens
  |
  = note: this error originates in the derive macro `kani::BoundedArbitrary` (in Nightly builds, run with -Z macro-backtrace for more info)

error: proc-macro derive produced unparsable tokens
 --> ba.rs:1:10
  |
1 | #[derive(kani::BoundedArbitrary)]
  |          ^^^^^^^^^^^^^^^^^^^^^^

error[E0277]: the trait bound `Foo<u8>: kani::BoundedArbitrary` is not satisfied
  --> ba.rs:9:42
   |
9  |     let f: Foo<u8> = kani::bounded_any::<_, 16>();
   |                                          ^ the trait `kani::BoundedArbitrary` is not implemented for `Foo<u8>`
   |
   = help: the following other types implement trait `kani::BoundedArbitrary`:
             std::collections::HashMap<K, V, std::hash::BuildHasherDefault<std::hash::DefaultHasher>>
             std::collections::HashSet<V, std::hash::BuildHasherDefault<std::hash::DefaultHasher>>
             std::option::Option<T>
             std::result::Result<T, E>
             std::string::String
             std::vec::Vec<T>
note: required by a bound in `kani::bounded_any`
  --> /home/ubuntu/git/kani/library/kani/src/lib.rs:55:1
   |
55 | kani_core::kani_lib!(kani);
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^ required by this bound in `bounded_any`
   = note: this error originates in the macro `kani_core::kani_intrinsics` 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 3 previous errors

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