generated from amazon-archives/__template_Apache-2.0
-
Notifications
You must be signed in to change notification settings - Fork 129
Closed
Labels
[C] BugThis is a bug. Something isn't working.This is a bug. Something isn't working.
Description
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: 101If I uncomment the second variant, verification is successful.
Metadata
Metadata
Assignees
Labels
[C] BugThis is a bug. Something isn't working.This is a bug. Something isn't working.