From 50dbdd7ecd82a39720782b4e15d221f166e34c9d Mon Sep 17 00:00:00 2001
From: Onyeka Obi <softwareengineerasaservant@isurvivable.cv>
Date: Wed, 15 Jul 2026 22:34:45 -0700
Subject: [PATCH] Fix codegen panic for calls through a function pointer
 returning `!`

Calling a function pointer whose return type is the never type `!` panicked
the compiler in `codegen_funcall`. The function-pointer branch built the
call's continuation with `Stmt::goto(bb_label(target.unwrap()), loc)`, but a
call that diverges (return type `!`) has no return target, so `target` is
`None` and the `unwrap()` panicked:

    thread 'rustc' panicked at .../codegen/statement.rs:
    called `Option::unwrap()` on a `None` value

The sibling branch for direct (`FnDef`) calls already handles this: it ends
the call with `codegen_end_call`, which emits an unreachable sanity check when
there is no return target. Route the function-pointer branch through the same
helper so both paths behave identically.

Resolves #4577

Signed-off-by: Onyeka Obi <softwareengineerasaservant@isurvivable.cv>
---
 .../codegen/statement.rs                      |  2 +-
 tests/kani/Never/fn_ptr_never_return.rs       | 22 +++++++++++++++++++
 2 files changed, 23 insertions(+), 1 deletion(-)
 create mode 100644 tests/kani/Never/fn_ptr_never_return.rs

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
index c758f2942afa..2827f058c3a2 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
@@ -791,7 +791,7 @@ impl GotocCtx<'_, '_> {
                 Stmt::block(
                     vec![
                         self.codegen_expr_to_place_stable(destination, func_expr.call(fargs), loc),
-                        Stmt::goto(bb_label(target.unwrap()), loc),
+                        self.codegen_end_call(*target, loc),
                     ],
                     loc,
                 )
diff --git a/tests/kani/Never/fn_ptr_never_return.rs b/tests/kani/Never/fn_ptr_never_return.rs
new file mode 100644
index 000000000000..4670a7a03bf2
--- /dev/null
+++ b/tests/kani/Never/fn_ptr_never_return.rs
@@ -0,0 +1,22 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-verify-fail
+
+//! Regression test for https://github.com/model-checking/kani/issues/4577
+//!
+//! Calling a function pointer whose return type is the never type `!` used to
+//! panic the Kani compiler in `codegen_funcall`: the function-pointer path
+//! unconditionally unwrapped the call's return target, but a diverging call
+//! has no return target. Codegen must instead treat the missing target like a
+//! direct call to a never-returning function does. Here the callee panics, so
+//! verification reaches the panic and fails (rather than the compiler crashing).
+
+fn diverge() -> ! {
+    panic!("EXPECTED FAIL: diverging function was called");
+}
+
+#[kani::proof]
+fn check_fnptr_never() {
+    let f: fn() -> ! = diverge;
+    f();
+}