Fix missing function declaration issue

In cases where a function pointer is created, but its value is never
used, Kani crashes due to missing function declaration.

For now, collect any instance that has its address taken even if its
never used.

Fixes #3799

kani-compiler/src/kani_middle/reachability.rs

@@ -470,6 +470,22 @@ impl MirVisitor for MonoItemsFnCollector<'_, '_> {
 
         self.super_terminator(terminator, location);
     }
+
+    /// Collect any function definition that may occur as a type.
+    ///
+    /// The codegen stage will require the definition to be available.
+    /// This is a conservative approach, since there are cases where the function is never
+    /// actually used, so we don't need the body.
+    ///
+    /// Another alternative would be to lazily declare functions, but it would require a bigger
+    /// change to codegen.
+    fn visit_ty(&mut self, ty: &Ty, _: Location) {
+        if let TyKind::RigidTy(RigidTy::FnDef(def, args)) = ty.kind() {
+            let instance = Instance::resolve(def, &args).unwrap();
+            self.collect_instance(instance, true);
+        }
+        self.super_ty(ty);
+    }
 }
 
 fn extract_unsize_coercion(tcx: TyCtxt, orig_ty: Ty, dst_trait: Ty) -> (Ty, Ty) {

tests/kani/CodegenMisc/missing_mut_fn.rs

@@ -0,0 +1,27 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! Ensure Kani can codegen code with a pointer to a function that is never used
+//! See <https://github.com/model-checking/kani/issues/3799> for more details.
+fn foo<F: Fn()>(_func: &mut F) {}
+fn foo_dyn(_func: &mut dyn Fn()) {}
+
+#[kani::proof]
+fn check_foo() {
+    fn f() {}
+
+    foo(&mut f);
+}
+
+#[kani::proof]
+fn check_foo_dyn() {
+    fn f() {}
+
+    foo_dyn(&mut f);
+}
+
+#[kani::proof]
+fn check_foo_unused() {
+    fn f() {}
+
+    let ptr = &mut f;
+}