Do not fail on crates that forbid(unstable_features) - #4688
Open
tautschnig wants to merge 1 commit into
Open
Conversation
github-actions
Bot
added
Z-EndToEndBenchCI
Contributor
There was a problem hiding this comment.
Pull request overview
This PR makes Kani more robust when compiling third-party crates that set #![forbid(unstable_features)], which previously failed due to Kani injecting feature(register_tool) via -Z crate-attr. It unconditionally downgrades the unstable_features lint to a warning at the rustc invocation level and adds a regression test to ensure such crates can be verified.
Changes:
- Add
--force-warn unstable_featuresto Kani’s baseline rustc flags to override crate-levelforbid(unstable_features)for injected features. - Add a new
tests/kaniregression test that forbidsunstable_featuresand verifies successfully under Kani.
Reviewed changes
Copilot reviewed 2 out of 2 changed files in this pull request and generated no comments.
| File | Description |
|---|---|
| tests/kani/ForbidUnstableFeatures/forbid_unstable_features.rs | Adds a regression test crate that forbids unstable_features to validate the new driver behavior. |
| kani-driver/src/call_single_file.rs | Extends the base rustc flags with --force-warn unstable_features to prevent injected #![feature] from becoming a hard error. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Kani injects 'feature(register_tool)' via -Zcrate-attr into every crate it compiles, so crates that forbid(unstable_features) -- e.g. rustls, which gates the forbid on 'not(any(read_buf, bench, coverage_nightly))' -- failed to build under Kani with 'error: use of an unstable feature', through no fault of their own. Downgrade the lint with '--force-warn unstable_features', which overrides even a forbid in the crate source. The injected feature gate is a Kani implementation detail, not something the crate author can or should fix. Verified that rustls-0.23.42 (previously failing) now compiles under 'cargo kani --only-codegen'. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
tautschnig
force-pushed
the
fix-forbid-unstable-features
branch
from
July 29, 2026 00:42
c02c9b5 to
cc5fe8f
Compare
feliperodri
approved these changes
Jul 29, 2026
feliperodri
left a comment
feliperodri
left a comment
Contributor
There was a problem hiding this comment.
We should update the test case ui/ice-size-overflow/large_array.rs
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Description
Kani injects
feature(register_tool)via-Zcrate-attrinto every crate it compiles, so crates thatforbid(unstable_features)fail to build under Kani with "error: use of an unstable feature" — through no fault of their own. rustls is a prominent example: it applies the forbid unless benchmarking/coverage cfgs are set, socargo kanion rustls fails immediately.Downgrade the lint with
--force-warn unstable_features, which overrides even aforbidin the crate source. The injected feature gate is a Kani implementation detail, not something the crate author can or should fix, so downgrading unconditionally is the right semantics (the warning remains visible).Found while evaluating
kani autoharnesson the top-100 crates.io crates; verified rustls-0.23.42 (previously failing) now compiles undercargo kani --only-codegen.Testing
New regression test
tests/kani/ForbidUnstableFeatures/forbid_unstable_features.rs: a crate with#![forbid(unstable_features)]and a proof harness now verifies successfully.kani-driverunit tests and formatting pass.By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.