From e9b6e3a2221e77eb03a988034276f9760a35c37b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 13 Feb 2026 10:37:50 +0000 Subject: [PATCH 1/2] Fix workspace feature handling to filter features per-package The --features flag was being applied globally to all packages in a workspace, causing failures when packages don't all declare the same features. This change filters requested features for each package based on what that package actually defines in its features BTreeMap. Added regression test for --workspace --features with mixed features. Co-authored-by: Kiro autonomous agent Resolves: #4544 --- kani-driver/src/call_cargo.rs | 41 +++++++++++++++---- .../workspace_features/Cargo.toml | 6 +++ .../workspace_features/config.yml | 4 ++ .../workspace_features/mylib/Cargo.toml | 11 +++++ .../workspace_features/mylib/src/lib.rs | 14 +++++++ .../workspace_features/mytests/Cargo.toml | 13 ++++++ .../workspace_features/mytests/src/lib.rs | 19 +++++++++ .../workspace_features.expected | 1 + .../workspace_features/workspace_features.sh | 26 ++++++++++++ 9 files changed, 128 insertions(+), 7 deletions(-) create mode 100644 tests/script-based-pre/workspace_features/Cargo.toml create mode 100644 tests/script-based-pre/workspace_features/config.yml create mode 100644 tests/script-based-pre/workspace_features/mylib/Cargo.toml create mode 100644 tests/script-based-pre/workspace_features/mylib/src/lib.rs create mode 100644 tests/script-based-pre/workspace_features/mytests/Cargo.toml create mode 100644 tests/script-based-pre/workspace_features/mytests/src/lib.rs create mode 100644 tests/script-based-pre/workspace_features/workspace_features.expected create mode 100755 tests/script-based-pre/workspace_features/workspace_features.sh diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs index fbcd09c4c835..9394b373b47d 100644 --- a/kani-driver/src/call_cargo.rs +++ b/kani-driver/src/call_cargo.rs @@ -163,10 +163,10 @@ crate-type = ["lib"] if self.args.cargo.no_default_features { cargo_args.push("--no-default-features".into()); } - let features = self.args.cargo.features(); - if !features.is_empty() { - cargo_args.push(format!("--features={}", features.join(",")).into()); - } + // Note: We do NOT add --features here globally. Features are filtered + // per-package below to handle workspaces where packages don't all + // declare the same features. This matches cargo's behavior. + let requested_features = self.args.cargo.features(); cargo_args.append(&mut cargo_config_args()); @@ -210,12 +210,22 @@ crate-type = ["lib"] let mut artifacts = vec![]; let mut failed_targets = vec![]; for package in packages { + // Filter requested features to only include those that this package defines. + // This matches cargo's behavior for `cargo test --workspace --features ` + // where features are applied only to packages that declare them. + let pkg_features = filter_features_for_package(&requested_features, package); + for verification_target in package_targets(&self.args, package) { let mut cmd = setup_cargo_command_inner(Some(verification_target.target().name.clone()))?; - cmd.pass_cargo_args(&cargo_args) - .args(vec!["-p", &package.id.to_string()]) - .args(verification_target.to_args()) + cmd.pass_cargo_args(&cargo_args).args(vec!["-p", &package.id.to_string()]); + + // Add filtered features for this specific package + if !pkg_features.is_empty() { + cmd.arg(format!("--features={}", pkg_features.join(","))); + } + + cmd.args(verification_target.to_args()) .arg("--") // Add this delimiter so we start passing args to rustc and not Cargo .env("RUSTC", &self.kani_compiler) .pass_rustc_args(&rustc_args, PassTo::AllCrates) @@ -656,3 +666,20 @@ fn package_targets(args: &VerificationArgs, package: &Package) -> Vec` where not all +/// workspace members declare the same features. Without filtering, cargo would fail with +/// "none of the selected packages contains these features" error. +/// +/// This matches cargo's behavior for `cargo test --workspace --features ` where +/// features are applied only to packages that declare them, and silently skipped for +/// packages that don't. +fn filter_features_for_package(requested_features: &[String], package: &Package) -> Vec { + requested_features + .iter() + .filter(|feature| package.features.contains_key(*feature)) + .cloned() + .collect() +} diff --git a/tests/script-based-pre/workspace_features/Cargo.toml b/tests/script-based-pre/workspace_features/Cargo.toml new file mode 100644 index 000000000000..c370cc2f699b --- /dev/null +++ b/tests/script-based-pre/workspace_features/Cargo.toml @@ -0,0 +1,6 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +[workspace] +members = ["mylib", "mytests"] +resolver = "2" diff --git a/tests/script-based-pre/workspace_features/config.yml b/tests/script-based-pre/workspace_features/config.yml new file mode 100644 index 000000000000..3187e3a36b88 --- /dev/null +++ b/tests/script-based-pre/workspace_features/config.yml @@ -0,0 +1,4 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: workspace_features.sh +expected: workspace_features.expected diff --git a/tests/script-based-pre/workspace_features/mylib/Cargo.toml b/tests/script-based-pre/workspace_features/mylib/Cargo.toml new file mode 100644 index 000000000000..80c45a9033ee --- /dev/null +++ b/tests/script-based-pre/workspace_features/mylib/Cargo.toml @@ -0,0 +1,11 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +[package] +name = "mylib" +version = "0.1.0" +edition = "2021" + +# This package has NO features defined intentionally +# to test that --workspace --features works when some packages +# don't have the requested features diff --git a/tests/script-based-pre/workspace_features/mylib/src/lib.rs b/tests/script-based-pre/workspace_features/mylib/src/lib.rs new file mode 100644 index 000000000000..39b03baaf480 --- /dev/null +++ b/tests/script-based-pre/workspace_features/mylib/src/lib.rs @@ -0,0 +1,14 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! A simple library without any features defined. + +pub fn add(a: u32, b: u32) -> u32 { + a + b +} + +#[kani::proof] +fn check_add() { + let result = add(1, 2); + assert!(result == 3); +} diff --git a/tests/script-based-pre/workspace_features/mytests/Cargo.toml b/tests/script-based-pre/workspace_features/mytests/Cargo.toml new file mode 100644 index 000000000000..3fe332f70f69 --- /dev/null +++ b/tests/script-based-pre/workspace_features/mytests/Cargo.toml @@ -0,0 +1,13 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +[package] +name = "mytests" +version = "0.1.0" +edition = "2021" + +[features] +use_mylib = [] + +[dependencies] +mylib = { path = "../mylib" } diff --git a/tests/script-based-pre/workspace_features/mytests/src/lib.rs b/tests/script-based-pre/workspace_features/mytests/src/lib.rs new file mode 100644 index 000000000000..1655e39906c2 --- /dev/null +++ b/tests/script-based-pre/workspace_features/mytests/src/lib.rs @@ -0,0 +1,19 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! A test crate with the use_mylib feature defined. + +#[cfg(feature = "use_mylib")] +use mylib::add; + +#[cfg(feature = "use_mylib")] +#[kani::proof] +fn check_mylib_add() { + let result = add(2, 3); + assert!(result == 5); +} + +#[kani::proof] +fn check_basic() { + assert!(1 + 1 == 2); +} diff --git a/tests/script-based-pre/workspace_features/workspace_features.expected b/tests/script-based-pre/workspace_features/workspace_features.expected new file mode 100644 index 000000000000..81fef9812c31 --- /dev/null +++ b/tests/script-based-pre/workspace_features/workspace_features.expected @@ -0,0 +1 @@ +All workspace feature tests passed diff --git a/tests/script-based-pre/workspace_features/workspace_features.sh b/tests/script-based-pre/workspace_features/workspace_features.sh new file mode 100755 index 000000000000..403e8a3f6ab4 --- /dev/null +++ b/tests/script-based-pre/workspace_features/workspace_features.sh @@ -0,0 +1,26 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +# Test that cargo kani --workspace --features works correctly when some +# workspace members don't declare the requested features. +# This is a regression test for the issue where cargo kani fails with +# "none of the selected packages contains these features" when using +# --workspace --features with a workspace containing packages that don't +# all have the same features. + +set -e + +rm -rf target + +# Test with a feature that only exists in mytests, not in mylib +cargo kani --workspace --features use_mylib + +# Test with --no-default-features flag +cargo kani --workspace --no-default-features + +# Test combination of flags +cargo kani --workspace --no-default-features --features use_mylib + +rm -rf target +echo "All workspace feature tests passed" From 8ea843732a352422c55f7c70fc72abc902ca9e9e Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 16 Feb 2026 11:07:35 +0000 Subject: [PATCH 2/2] Add check_mylib_add harness verification to workspace_features test Ensures feature propagation to packages and validates proof inclusion as requested by tautschnig. --- .../workspace_features/workspace_features.expected | 2 ++ 1 file changed, 2 insertions(+) diff --git a/tests/script-based-pre/workspace_features/workspace_features.expected b/tests/script-based-pre/workspace_features/workspace_features.expected index 81fef9812c31..b04b35112ac2 100644 --- a/tests/script-based-pre/workspace_features/workspace_features.expected +++ b/tests/script-based-pre/workspace_features/workspace_features.expected @@ -1 +1,3 @@ +Checking harness check_mylib_add... +VERIFICATION:- SUCCESSFUL All workspace feature tests passed