Fix a bug codegening SwitchInts with only an otherwise branch (#4095)

The first commit adds a failing test: it exposes a bug dealing with
dropping single-variant enums.

```
thread 'rustc' panicked at kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs:499:9:
assertion failed: targets.len() > 1
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

Kani unexpectedly panicked during compilation.
Please file an issue here: https://github.com/model-checking/kani/issues/new?labels=bug&template=bug_report.md

[Kani] current codegen item: codegen_function: std::ptr::drop_in_place::<Reference>
_RINvNtCs4AkhfejoRTd_4core3ptr13drop_in_placeNtCs6S0fALEP9ee_19single_variant_enum9ReferenceEBI_
[Kani] current codegen location: Loc { file: "/Users/bkirwi/.rustup/toolchains/nightly-2025-05-20-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/ptr/mod.rs", function: None, start_line: 524, start_col: Some(1), end_line: 524, end_col: Some(56), pragmas: [] }
error: /Users/bkirwi/Code/kani/target/kani/bin/kani-compiler exited with status exit status: 101
```

This seems to affect both `main` and the latest release.

Resolves #4103

---------

Co-authored-by: Carolyn Zech <[email protected]>

Author: bkirwi

kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs

@@ -497,32 +497,39 @@ impl GotocCtx<'_> {
         let switch_ty = v.typ().clone();
 
         // Switches with empty branches should've been eliminated already.
-        assert!(targets.len() > 1);
-        if targets.len() == 2 {
-            // Translate to a guarded goto
-            let (case, first_target) = targets.branches().next().unwrap();
-            Stmt::block(
-                vec![
-                    v.eq(Expr::int_constant(case, switch_ty)).if_then_else(
-                        Stmt::goto(bb_label(first_target), loc),
-                        None,
-                        loc,
-                    ),
-                    Stmt::goto(bb_label(targets.otherwise()), loc),
-                ],
-                loc,
-            )
-        } else {
-            let cases = targets
-                .branches()
-                .map(|(c, bb)| {
-                    Expr::int_constant(c, switch_ty.clone())
-                        .with_location(loc)
-                        .switch_case(Stmt::goto(bb_label(bb), loc))
-                })
-                .collect();
-            let default = Stmt::goto(bb_label(targets.otherwise()), loc);
-            v.switch(cases, Some(default), loc)
+        match targets.len() {
+            0 => unreachable!("switches have at least one target"),
+            1 => {
+                // Trivial switch.
+                Stmt::goto(bb_label(targets.otherwise()), loc)
+            }
+            2 => {
+                // Translate to a guarded goto
+                let (case, first_target) = targets.branches().next().unwrap();
+                Stmt::block(
+                    vec![
+                        v.eq(Expr::int_constant(case, switch_ty)).if_then_else(
+                            Stmt::goto(bb_label(first_target), loc),
+                            None,
+                            loc,
+                        ),
+                        Stmt::goto(bb_label(targets.otherwise()), loc),
+                    ],
+                    loc,
+                )
+            }
+            3.. => {
+                let cases = targets
+                    .branches()
+                    .map(|(c, bb)| {
+                        Expr::int_constant(c, switch_ty.clone())
+                            .with_location(loc)
+                            .switch_case(Stmt::goto(bb_label(bb), loc))
+                    })
+                    .collect();
+                let default = Stmt::goto(bb_label(targets.otherwise()), loc);
+                v.switch(cases, Some(default), loc)
+            }
         }
     }
 

tests/kani/SwitchInt/main.rs

@@ -38,3 +38,15 @@ fn main() {
     let v = doswitch_bytes();
     assert!(v == 1);
 }
+
+// Check that Kani can codegen a SwitchInt that has no targets (only an otherwise)
+// c.f. https://github.com/model-checking/kani/issues/4103
+pub enum Reference {
+    ByName { alias: String },
+}
+
+#[kani::proof]
+fn check_nontrivial_drop() {
+    let result: Reference = Reference::ByName { alias: "foo".into() };
+    drop(result)
+}