Fix codegen panic for calls through a function pointer returning !

[MavenRain]

Description

Fixes a compiler panic when Kani codegens a call through a function pointer
whose return type is the never type !.

Context

Given the minimal reproducer from #4577:

fn diverge() -> ! {
    loop {}
}

#[kani::proof]
fn check_fnptr_never() {
    let f: fn() -> ! = diverge;
    f();
}

Kani panicked during codegen:

thread 'rustc' panicked at kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs:
called `Option::unwrap()` on a `None` value
  ...
  <GotocCtx>::codegen_funcall

In codegen_funcall, the function-pointer (RigidTy::FnPtr) branch ended the
call with:

Stmt::goto(bb_label(target.unwrap()), loc)

A call whose callee returns ! diverges, so MIR gives it no return target and
target is None; the unconditional unwrap() then panics. The sibling
branch for direct (RigidTy::FnDef) calls does not have this problem because
it ends the call with codegen_end_call, which already handles a missing
target by emitting an unreachable "Unexpected return from Never function"
sanity check instead of a goto.

Change

Route the function-pointer branch through the same codegen_end_call helper,
so a diverging call through a function pointer is handled exactly like a
diverging direct call. This is a one-line change; the diverging case is now
covered by the existing, tested code path.

Testing

• Added tests/kani/Never/fn_ptr_never_return.rs, a regression test that calls
  a fn() -> ! pointer. The callee panics, so the harness reaches the panic
  and verification fails as expected (// kani-verify-fail); before this fix
  the compiler crashed instead of producing any verification result. Built
  Kani (cargo build-dev) and ran it: the harness reports
  VERIFICATION:- FAILED with Failed Checks: EXPECTED FAIL: diverging function was called, i.e. codegen completes and CBMC runs.
• Ran the exact reproducer from the issue (the loop {} variant) against the
  built Kani: it no longer panics during codegen and proceeds into CBMC.
• cargo check -p kani-compiler passes.

Resolves #4577

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[Copilot]

Pull request overview

Fixes a Kani compiler codegen panic when generating calls through a function pointer (fn() -> !) by removing an unconditional target.unwrap() in the FnPtr call path and reusing the existing codegen_end_call handling for missing return targets (diverging/never-returning calls).

Changes:

• Route function-pointer calls in codegen_funcall through codegen_end_call(*target, loc) to correctly handle target: None for -> !.
• Add a regression test that calls a fn() -> ! function pointer and expects verification failure (panic), ensuring codegen no longer crashes.

Reviewed changes

Copilot reviewed 2 out of 2 changed files in this pull request and generated no comments.

File	Description
kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs	Replaces a target.unwrap()-based goto with codegen_end_call to avoid panics on diverging function-pointer calls.
tests/kani/Never/fn_ptr_never_return.rs	Adds a regression test for issue #4577 covering fn() -> ! function-pointer calls.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.