Merge branch 'main' into bench-on-pull-request

Author: tautschnig

kani-compiler/src/kani_compiler.rs

@@ -170,6 +170,20 @@ impl Callbacks for KaniCompiler {
             // injecting `extern crate std` there would pull in a *second* `std`
             // (and `core`), causing duplicate-lang-item errors (E0152).
             && compiler.sess.opts.externs.get("std").is_some()
+            // Do not inject into external (registry/git) dependencies: the
+            // `#[macro_use]` scope is ambiguous (E0659) with an explicit glob
+            // import of the same macro name, and external crates may
+            // legitimately do that (e.g. libc >= 0.2.188 re-exports
+            // `core::assert` in an internal prelude that its modules
+            // glob-import, and calls `assert!`). External dependencies thus
+            // use the real `assert!`/`panic!`/... macros, which Kani models
+            // soundly, consistent with `no_std` dependencies which never had
+            // the overrides. Cargo passes `--cap-lints allow` exactly for
+            // non-local dependencies, so use that as the discriminator (like
+            // rustc's `Session::opts` consumers do for dependency-only
+            // behavior); local path/workspace crates and standalone `kani`
+            // builds keep the overrides.
+            && compiler.sess.opts.lint_cap.is_none()
         {
             inject_kani_macro_overrides(compiler, krate);
         }

library/std/src/lib.rs

@@ -32,8 +32,9 @@ pub mod prelude {
     // Kani's versions here makes `#![no_std]` dependencies that import this prelude
     // explicitly (`extern crate std; use std::prelude::v1::*;`, e.g. lazy_static)
     // ambiguous against the injected core prelude (E0659). Instead, kani-compiler
-    // injects those overrides only into the crate under verification (see
-    // kani_compiler's macro-override injection). The print family is defined in this
+    // injects those overrides only into local crates, not external (registry/git)
+    // dependencies (see kani_compiler's macro-override injection). The print family
+    // is defined in this
     // crate (std) with no core-prelude counterpart, so overriding it here is safe and
     // applies everywhere (dependencies included), which is important so that a
     // dependency's `println!` does not run real formatting/IO during verification.