Derive Arbitrary for enums with a single variant

library/kani_macros/src/derive.rs

@@ -364,6 +364,12 @@ fn fn_any_enum(ident: &Ident, data: &DataEnum) -> TokenStream {
         quote! {
             panic!(#msg)
         }
+    } else if data.variants.len() == 1 {
+        let variant = data.variants.first().unwrap();
+        let init = init_symbolic_item(&variant.ident, &variant.fields);
+        quote! {
+            #ident::#init
+        }
     } else {
         let arms = data.variants.iter().enumerate().map(|(idx, variant)| {
             let init = init_symbolic_item(&variant.ident, &variant.fields);

tests/ui/derive-arbitrary/single_variant_enum/expected

@@ -0,0 +1,16 @@
+Checking harness check_with_discriminant...
+SUCCESS\
+"assertion failed: disc == 42"
+
+Checking harness check_with_named_args...
+SUCCESS\
+"assertion failed: flag as u8 == 0 || flag as u8 == 1"
+2 of 2 cover properties satisfied
+
+Checking harness check_with_args...
+SUCCESS\
+"assertion failed: c <= char::MAX"
+2 of 2 cover properties satisfied
+
+Checking harness check_simple...
+1 of 1 cover properties satisfied

tests/ui/derive-arbitrary/single_variant_enum/single_variant_enum.rs

@@ -0,0 +1,65 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! Check that Kani can automatically derive Arbitrary enums.
+//! An arbitrary enum should always generate a valid arbitrary variant.
+
+extern crate kani;
+use kani::cover;
+
+#[derive(kani::Arbitrary)]
+enum Simple {
+    Empty,
+}
+
+#[kani::proof]
+fn check_simple() {
+    match kani::any::<Simple>() {
+        Simple::Empty => cover!(),
+    }
+}
+
+#[derive(kani::Arbitrary)]
+enum WithArgs {
+    Args(char),
+}
+
+#[kani::proof]
+fn check_with_args() {
+    match kani::any::<WithArgs>() {
+        WithArgs::Args(c) => {
+            assert!(c <= char::MAX);
+            cover!(c == 'a');
+            cover!(c == '1');
+        }
+    }
+}
+
+#[derive(kani::Arbitrary)]
+enum WithNamedArgs {
+    Args { flag: bool },
+}
+
+#[kani::proof]
+fn check_with_named_args() {
+    match kani::any::<WithNamedArgs>() {
+        WithNamedArgs::Args { flag } => {
+            cover!(flag as u8 == 0);
+            cover!(flag as u8 == 1);
+            assert!(flag as u8 == 0 || flag as u8 == 1);
+        }
+    }
+}
+
+#[derive(kani::Arbitrary)]
+enum WithDiscriminant {
+    Disc = 42,
+}
+
+#[kani::proof]
+fn check_with_discriminant() {
+    let v = kani::any::<WithDiscriminant>();
+    let disc = v as i8;
+    match v {
+        WithDiscriminant::Disc => assert!(disc == 42),
+    }
+}