Do not inject macro overrides into external dependencies

[tautschnig]

Since libc 0.2.188 was published (2026-07-21 09:38 UTC), every crate graph containing it fails to compile under Kani with dozens of error[E0659]: `assert` is ambiguous errors — including Kani's own regression and perf CI jobs on every PR (the cargo-kani test manifests use a floating libc = "0.2"; pushes to main still pass only because their last dependency resolution predates the release). See #4665 for the full analysis.

Root cause: the macro-override injection introduced in #4643 (#[macro_use] extern crate std as _kani_std_macros;) puts Kani's assert!/panic!/… overrides in the macro_use-prelude scope of every std crate kani-compiler builds. That scope shadows the standard prelude silently (intended), but is ambiguous (E0659) against an explicit glob import of the same macro name. libc's internal prelude re-exports core::assert and its modules glob-import that prelude; libc 0.2.188 added assert! calls in such a module (type-size sanity checks in src/types.rs), turning the latent conflict into a hard error.

Fix: restrict the injection to local crates. Cargo passes --cap-lints allow exactly for non-local (registry/git) dependencies, so Session::opts.lint_cap is the discriminator. External dependencies then use the real assert!/panic!/… macros, which Kani models soundly — consistent with no_std dependencies, which never had the overrides. Local path/workspace dependencies and standalone kani builds keep the overrides, preserving the dependency reachability/message behavior pinned by the assert-reach and stubbing-ws-packages tests.

Testing:

• The existing cargo-kani/libc test acts as the regression test: with libc 0.2.188 it fails before this change and passes after (its floating version requirement is a feature — it surfaced this bug within hours of the libc release). I first prototyped a hermetic path-dependency reproducer, but local path deps should keep the overrides (as assert-reach/stubbing-ws-packages demonstrate), so the libc test is the accurate coverage.
• Full cargo-kani suite: 71 passed / 0 failed, including the five tests failing in CI today (libc, chrono_dep, dependencies, cbmc-unknown-lang-mode, stubbing-validate-random) and the two that pin local-dependency semantics.
• expected/assert* standalone tests pass (override still active outside cargo).

An earlier iteration used CARGO_PRIMARY_PACKAGE as the discriminator, but that also strips the overrides from workspace/path dependencies, breaking assert-reach and stubbing-ws-packages; lint_cap matches the desired local/external cut exactly.

Resolves #4665

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

This PR fixes a newly triggered Rust macro-resolution conflict (E0659 “assert is ambiguous”) caused by Kani’s #[macro_use] extern crate std as _kani_std_macros; injection being applied to external dependencies. It updates kani-compiler to inject macro overrides only for local crates, so registry/git dependencies like libc >= 0.2.188 compile normally under cargo kani while preserving the existing override behavior for local/workspace crates and standalone kani builds.

Changes:

• Gate macro-override injection on compiler.sess.opts.lint_cap.is_none() to avoid injecting into dependency crates where Cargo uses --cap-lints allow.
• Update library/std documentation comment to match the new “local crates only” injection behavior.

Reviewed changes

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

File	Description
library/std/src/lib.rs	Updates commentary to reflect that core-prelude macro overrides are injected only into local crates (not external deps).
kani-compiler/src/kani_compiler.rs	Restricts macro-override injection to local crates using Session::opts.lint_cap as the discriminator to avoid E0659 in external dependencies.

---

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

[tautschnig]

The compiler benchmarks need #4664, but those are not marked "Required" so we'll need to get the changes in this PR merged first.