Improve linking error output for #[no_std] crates

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -290,9 +290,23 @@ impl CodegenBackend for GotocCodegenBackend {
             if queries.args().reachability_analysis != ReachabilityType::None
                 && queries.kani_functions().is_empty()
             {
-                tcx.sess.dcx().err(
-                    "Failed to detect Kani functions. Please check your installation is correct.",
-                );
+                if stable_mir::find_crates("std").is_empty()
+                    && stable_mir::find_crates("kani").is_empty()
+                {
+                    // Special error for when not importing kani and using #[no_std].
+                    // See here for more info: https://github.com/model-checking/kani/issues/3906#issuecomment-2932687768.
+                    tcx.sess.dcx().struct_err(
+                        "Failed to detect Kani functions."
+                    ).with_help(
+                        "This project seems to be using #[no_std] but does not import Kani. \
+                        Try adding `crate extern kani` to the crate root to explicitly import Kani."
+                    )
+                    .emit();
+                } else {
+                    tcx.sess.dcx().struct_err(
+                        "Failed to detect Kani functions. Please check your installation is correct."
+                    ).emit();
+                }
             }
 
             // Codegen all items that need to be processed according to the selected reachability mode:

kani-compiler/src/kani_middle/kani_functions.rs

@@ -269,5 +269,9 @@ pub fn validate_kani_functions(kani_funcs: &HashMap<KaniFunction, FnDef>) {
             missing += 1;
         }
     }
-    assert_eq!(missing, 0, "Failed to find `{missing}` Kani functions");
+    // If this is failing for #[no_std] crates, try explicitly adding `extern crate kani` to the crate root.
+    // See https://github.com/model-checking/kani/issues/3906 for why this is required.
+    if missing != 0 {
+        tracing::error!("Failed to find `{missing}` Kani functions")
+    }
 }

tests/cargo-ui/no-std-no-kani/Cargo.toml

@@ -0,0 +1,9 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "no-std-help"
+version = "0.1.0"
+edition = "2024"
+
+[dependencies]

tests/cargo-ui/no-std-no-kani/expected

@@ -0,0 +1,3 @@
+error: Failed to detect Kani functions.\
+  |\
+  = help: This project seems to be using #[no_std] but does not import kani. Try adding `crate extern kani` to the crate root to explicitly import kani.

tests/cargo-ui/no-std-no-kani/src/lib.rs

@@ -0,0 +1,10 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Ensure that a no_std crate with no harnesses & no "extern crate kani" gets a useful error message.
+
+#![no_std]
+
+fn add(x: u8, y: u8) -> u8 {
+    x + y
+}