Implement support for Cargo.toml's default-members

kani-driver/src/call_cargo.rs

@@ -408,14 +408,14 @@ crate-type = ["lib"]
 
     /// Extract the packages that should be verified.
     ///
-    /// The result is built following these rules:
+    /// The result is built following these rules (mimicking cargo, see
+    /// https://github.com/rust-lang/cargo/blob/master/src/cargo/core/workspace.rs):
     /// - If `--package <pkg>` is given, return the list of packages selected.
     /// - If `--exclude <pkg>` is given, return the list of packages not excluded.
     /// - If `--workspace` is given, return the list of workspace members.
-    /// - If no argument provided, return the root package if there's one or all members.
-    ///   - I.e.: Do whatever cargo does when there's no `default_members`.
-    ///   - This is because `default_members` is not available in cargo metadata.
-    ///     See <https://github.com/rust-lang/cargo/issues/8033>.
+    /// - Else obtain the set of packages from cargo's default_workspace_members (i.e., if
+    ///   `default-members` is specified in Cargo.toml, use that list; else if a root package is
+    ///   specified use that; else use all members).
     ///
     /// In addition, if either `--package <pkg>` or `--exclude <pkg>` is given,
     /// validate that `<pkg>` is a package name in the workspace, or return an error
@@ -455,11 +455,10 @@ crate-type = ["lib"]
                 .into_iter()
                 .filter(|pkg| !pkg_ids.contains_key(&pkg.id))
                 .collect()
+        } else if args.cargo.workspace {
+            metadata.workspace_packages()
         } else {
-            match (args.cargo.workspace, metadata.root_package()) {
-                (true, _) | (_, None) => metadata.workspace_packages(),
-                (_, Some(root_pkg)) => vec![root_pkg],
-            }
+            metadata.workspace_default_packages()
         };
         trace!(?packages, "packages_to_verify result");
         Ok(packages)

tests/cargo-kani/default-members/Cargo.toml

@@ -0,0 +1,17 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "empty-main"
+version = "0.1.0"
+edition = "2018"
+
+[dependencies]
+
+[workspace]
+members = [ "builds-ok","dont-build-me"]
+
+# This indicates what package to e.g. build with 'cargo build' without --workspace
+default-members = [
+  ".",
+  "builds-ok",
+]

tests/cargo-kani/default-members/builds-ok/Cargo.toml

@@ -0,0 +1,8 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "builds-ok"
+version = "0.1.0"
+edition = "2024"
+
+[dependencies]

tests/cargo-kani/default-members/builds-ok/src/main.rs

@@ -0,0 +1,6 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+#[kani::proof]
+fn main() {
+    assert!(1 == 2);
+}

tests/cargo-kani/default-members/dont-build-me/Cargo.toml

@@ -0,0 +1,8 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "dont-build-me"
+version = "0.1.0"
+edition = "2024"
+
+[dependencies]

tests/cargo-kani/default-members/dont-build-me/src/main.rs

@@ -0,0 +1,5 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+fn main() {
+    this - is - not - valid - rust;
+}

tests/cargo-kani/default-members/main.expected

@@ -0,0 +1,3 @@
+FAILURE\
+assertion failed: 1 == 2
+VERIFICATION:- FAILED

tests/cargo-kani/default-members/src/main.rs

@@ -0,0 +1,5 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+fn main() {
+    println!("Hello, world!");
+}