Fix workspace feature handling to filter features per-package

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 <feature>`
+            // 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<Verificati
     }
     verification_targets
 }
+
+/// Filter a list of requested features to only include those that a package defines.
+///
+/// This is necessary to support `cargo kani --workspace --features <feature>` 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 <feature>` 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<String> {
+    requested_features
+        .iter()
+        .filter(|feature| package.features.contains_key(*feature))
+        .cloned()
+        .collect()
+}

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"

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

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

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);
+}

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" }

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);
+}

tests/script-based-pre/workspace_features/workspace_features.expected

@@ -0,0 +1,3 @@
+Checking harness check_mylib_add...
+VERIFICATION:- SUCCESSFUL
+All workspace feature tests passed

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"