From f878a55b42f9851d1f9e53ca81ee3c616abdd5b5 Mon Sep 17 00:00:00 2001
From: Adrian Palacios <accorell@amazon.com>
Date: Thu, 20 Apr 2023 18:34:05 +0000
Subject: [PATCH 01/10] Add a `--exclude` option for package exclusion

---
 kani-driver/src/args.rs       |  6 +++++
 kani-driver/src/call_cargo.rs | 49 +++++++++++++++++++++++++++--------
 2 files changed, 44 insertions(+), 11 deletions(-)

diff --git a/kani-driver/src/args.rs b/kani-driver/src/args.rs
index e37033aa3da1..a5a495564467 100644
--- a/kani-driver/src/args.rs
+++ b/kani-driver/src/args.rs
@@ -302,6 +302,7 @@ pub struct CargoArgs {
     /// Do not activate the `default` feature
     #[arg(long)]
     pub no_default_features: bool,
+
     // This tolerates spaces too, but we say "comma" only because this is the least error-prone approach...
     /// Comma separated list of features to activate
     #[arg(short = 'F', long)]
@@ -314,9 +315,14 @@ pub struct CargoArgs {
     /// Build all packages in the workspace
     #[arg(long)]
     pub workspace: bool,
+
     /// Run Kani on the specified packages.
     #[arg(long, short, conflicts_with("workspace"), num_args(1..))]
     pub package: Vec<String>,
+
+    /// Run Kani on the specified packages.
+    #[arg(long, short, conflicts_with("package"), num_args(1..))]
+    pub exclude: Vec<String>,
 }
 
 impl CargoArgs {
diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs
index 31e32f7c8004..f9bd98d61abd 100644
--- a/kani-driver/src/call_cargo.rs
+++ b/kani-driver/src/call_cargo.rs
@@ -103,8 +103,13 @@ impl KaniSession {
         let mut pkg_args: Vec<String> = vec![];
         pkg_args.extend(["--".to_string(), self.reachability_arg()]);
 
+        let packages_to_verify = packages_to_verify(&self.args, &metadata);
+        if let Err(package_error) = packages_to_verify {
+            bail!(package_error)
+        };
+
         let mut found_target = false;
-        let packages = packages_to_verify(&self.args, &metadata);
+        let packages = packages_to_verify.unwrap();
         let mut artifacts = vec![];
         let mut failed_targets = vec![];
         for package in packages {
@@ -261,27 +266,49 @@ fn print_msg(diagnostic: &Diagnostic, use_rendered: bool) -> Result<()> {
     Ok(())
 }
 
+/// Check that all package names are present in the workspace, otherwise return which aren't.
+fn validate_package_names(package_names: Vec<String>, packages: Vec<Package>) -> Result<()> {
+    let package_list: Vec<String> = packages.iter().map(|pkg| pkg.name.clone()).collect();
+    let unknown_packages: Vec<&String> =
+        package_names.iter().filter(|pkg_name| !package_list.contains(pkg_name)).collect();
+
+    // Some packages aren't in the workspace. Return an error which includes their names.
+    if unknown_packages.len() > 0 {
+        let fmt_packages: Vec<String> =
+            unknown_packages.iter().map(|pkg| format!("`{pkg}`")).collect();
+        let error_msg = if unknown_packages.len() == 1 {
+            format!("couldn't find package {}", fmt_packages[0])
+        } else {
+            format!("couldn't find packages {}", fmt_packages.join(", "))
+        };
+        bail!(error_msg);
+    };
+    Ok(())
+}
+
 /// Extract the packages that should be verified.
 /// 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>.
-fn packages_to_verify<'b>(args: &KaniArgs, metadata: &'b Metadata) -> Vec<&'b Package> {
-    debug!(package_selection=?args.cargo.package, workspace=args.cargo.workspace, "packages_to_verify args");
+/// 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
+/// otherwise.
+fn packages_to_verify<'b>(args: &KaniArgs, metadata: &'b Metadata) -> Result<Vec<&'b Package>> {
+    debug!(package_selection=?args.cargo.package, package_exclusion=?args.cargo.exclude, workspace=args.cargo.workspace, "packages_to_verify args");
     let packages = if !args.cargo.package.is_empty() {
+        validate_package_names(args.cargo.package.clone(), metadata.packages.clone())?;
         args.cargo
             .package
             .iter()
-            .map(|pkg_name| {
-                metadata
-                    .packages
-                    .iter()
-                    .find(|pkg| pkg.name == *pkg_name)
-                    .expect(&format!("Cannot find package '{pkg_name}'"))
-            })
+            .map(|pkg_name| metadata.packages.iter().find(|pkg| pkg.name == *pkg_name).unwrap())
             .collect()
+    } else if !args.cargo.exclude.is_empty() {
+        validate_package_names(args.cargo.exclude.clone(), metadata.packages.clone())?;
+        metadata.packages.iter().filter(|pkg| !args.cargo.exclude.contains(&pkg.name)).collect()
     } else {
         match (args.cargo.workspace, metadata.root_package()) {
             (true, _) | (_, None) => metadata.workspace_packages(),
@@ -289,7 +316,7 @@ fn packages_to_verify<'b>(args: &KaniArgs, metadata: &'b Metadata) -> Vec<&'b Pa
         }
     };
     trace!(?packages, "packages_to_verify result");
-    packages
+    Ok(packages)
 }
 
 /// Extract Kani artifact that might've been generated from a given rustc artifact.

From d39a6b4082e0ba74a4a39d962a895fd1ed2cd312 Mon Sep 17 00:00:00 2001
From: Adrian Palacios <accorell@amazon.com>
Date: Thu, 20 Apr 2023 20:11:33 +0000
Subject: [PATCH 02/10] Add `cargo-ui` tests

---
 tests/cargo-ui/ws-package-exclude-unknown/Cargo.toml   | 10 ++++++++++
 .../ws-package-exclude-unknown/bin_package/Cargo.toml  |  8 ++++++++
 .../ws-package-exclude-unknown/bin_package/src/main.rs |  6 ++++++
 .../ws-package-exclude-unknown/lib_package/Cargo.toml  |  8 ++++++++
 .../ws-package-exclude-unknown/lib_package/src/lib.rs  |  6 ++++++
 tests/cargo-ui/ws-package-exclude-unknown/src/main.rs  |  6 ++++++
 tests/cargo-ui/ws-package-exclude/Cargo.toml           | 10 ++++++++++
 .../cargo-ui/ws-package-exclude/bin_package/Cargo.toml |  8 ++++++++
 .../ws-package-exclude/bin_package/src/main.rs         |  6 ++++++
 .../cargo-ui/ws-package-exclude/lib_package/Cargo.toml |  8 ++++++++
 .../cargo-ui/ws-package-exclude/lib_package/src/lib.rs |  6 ++++++
 tests/cargo-ui/ws-package-exclude/src/main.rs          |  6 ++++++
 tests/cargo-ui/ws-package-select-unknown/Cargo.toml    | 10 ++++++++++
 .../ws-package-select-unknown/bin_package/Cargo.toml   |  8 ++++++++
 .../ws-package-select-unknown/bin_package/src/main.rs  |  6 ++++++
 .../ws-package-select-unknown/lib_package/Cargo.toml   |  8 ++++++++
 .../ws-package-select-unknown/lib_package/src/lib.rs   |  6 ++++++
 tests/cargo-ui/ws-package-select-unknown/src/main.rs   |  6 ++++++
 tests/cargo-ui/ws-package-select/Cargo.toml            | 10 ++++++++++
 .../cargo-ui/ws-package-select/bin_package/Cargo.toml  |  8 ++++++++
 .../cargo-ui/ws-package-select/bin_package/src/main.rs |  6 ++++++
 .../cargo-ui/ws-package-select/lib_package/Cargo.toml  |  8 ++++++++
 .../cargo-ui/ws-package-select/lib_package/src/lib.rs  |  6 ++++++
 tests/cargo-ui/ws-package-select/src/main.rs           |  6 ++++++
 24 files changed, 176 insertions(+)
 create mode 100644 tests/cargo-ui/ws-package-exclude-unknown/Cargo.toml
 create mode 100644 tests/cargo-ui/ws-package-exclude-unknown/bin_package/Cargo.toml
 create mode 100644 tests/cargo-ui/ws-package-exclude-unknown/bin_package/src/main.rs
 create mode 100644 tests/cargo-ui/ws-package-exclude-unknown/lib_package/Cargo.toml
 create mode 100644 tests/cargo-ui/ws-package-exclude-unknown/lib_package/src/lib.rs
 create mode 100644 tests/cargo-ui/ws-package-exclude-unknown/src/main.rs
 create mode 100644 tests/cargo-ui/ws-package-exclude/Cargo.toml
 create mode 100644 tests/cargo-ui/ws-package-exclude/bin_package/Cargo.toml
 create mode 100644 tests/cargo-ui/ws-package-exclude/bin_package/src/main.rs
 create mode 100644 tests/cargo-ui/ws-package-exclude/lib_package/Cargo.toml
 create mode 100644 tests/cargo-ui/ws-package-exclude/lib_package/src/lib.rs
 create mode 100644 tests/cargo-ui/ws-package-exclude/src/main.rs
 create mode 100644 tests/cargo-ui/ws-package-select-unknown/Cargo.toml
 create mode 100644 tests/cargo-ui/ws-package-select-unknown/bin_package/Cargo.toml
 create mode 100644 tests/cargo-ui/ws-package-select-unknown/bin_package/src/main.rs
 create mode 100644 tests/cargo-ui/ws-package-select-unknown/lib_package/Cargo.toml
 create mode 100644 tests/cargo-ui/ws-package-select-unknown/lib_package/src/lib.rs
 create mode 100644 tests/cargo-ui/ws-package-select-unknown/src/main.rs
 create mode 100644 tests/cargo-ui/ws-package-select/Cargo.toml
 create mode 100644 tests/cargo-ui/ws-package-select/bin_package/Cargo.toml
 create mode 100644 tests/cargo-ui/ws-package-select/bin_package/src/main.rs
 create mode 100644 tests/cargo-ui/ws-package-select/lib_package/Cargo.toml
 create mode 100644 tests/cargo-ui/ws-package-select/lib_package/src/lib.rs
 create mode 100644 tests/cargo-ui/ws-package-select/src/main.rs

diff --git a/tests/cargo-ui/ws-package-exclude-unknown/Cargo.toml b/tests/cargo-ui/ws-package-exclude-unknown/Cargo.toml
new file mode 100644
index 000000000000..8b5c5ea760fc
--- /dev/null
+++ b/tests/cargo-ui/ws-package-exclude-unknown/Cargo.toml
@@ -0,0 +1,10 @@
+[package]
+name = "ws-package-exclude"
+version = "0.1.0"
+edition = "2021"
+
+[workspace]
+members = ["lib_package", "bin_package"]
+
+[workspace.metadata.kani.flags]
+exclude = ["unknown_package"]
diff --git a/tests/cargo-ui/ws-package-exclude-unknown/bin_package/Cargo.toml b/tests/cargo-ui/ws-package-exclude-unknown/bin_package/Cargo.toml
new file mode 100644
index 000000000000..f6dc80f0babc
--- /dev/null
+++ b/tests/cargo-ui/ws-package-exclude-unknown/bin_package/Cargo.toml
@@ -0,0 +1,8 @@
+[package]
+name = "bin_package"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
diff --git a/tests/cargo-ui/ws-package-exclude-unknown/bin_package/src/main.rs b/tests/cargo-ui/ws-package-exclude-unknown/bin_package/src/main.rs
new file mode 100644
index 000000000000..47e452f47dd9
--- /dev/null
+++ b/tests/cargo-ui/ws-package-exclude-unknown/bin_package/src/main.rs
@@ -0,0 +1,6 @@
+fn main() {}
+
+#[kani::proof]
+fn harness_in_bin_package() {
+    assert!(1 + 1 == 2);
+}
\ No newline at end of file
diff --git a/tests/cargo-ui/ws-package-exclude-unknown/lib_package/Cargo.toml b/tests/cargo-ui/ws-package-exclude-unknown/lib_package/Cargo.toml
new file mode 100644
index 000000000000..d60143e79233
--- /dev/null
+++ b/tests/cargo-ui/ws-package-exclude-unknown/lib_package/Cargo.toml
@@ -0,0 +1,8 @@
+[package]
+name = "lib_package"
+version = "0.1.0"
+edition = "2021"
+
+[lib]
+name = "lib_package"
+path = "src/lib.rs"
diff --git a/tests/cargo-ui/ws-package-exclude-unknown/lib_package/src/lib.rs b/tests/cargo-ui/ws-package-exclude-unknown/lib_package/src/lib.rs
new file mode 100644
index 000000000000..a6a2da70c4f9
--- /dev/null
+++ b/tests/cargo-ui/ws-package-exclude-unknown/lib_package/src/lib.rs
@@ -0,0 +1,6 @@
+pub fn api() {}
+
+#[kani::proof]
+fn harness_in_lib_package() {
+    assert!(1 + 1 == 2);
+}
\ No newline at end of file
diff --git a/tests/cargo-ui/ws-package-exclude-unknown/src/main.rs b/tests/cargo-ui/ws-package-exclude-unknown/src/main.rs
new file mode 100644
index 000000000000..cec32d76fc4c
--- /dev/null
+++ b/tests/cargo-ui/ws-package-exclude-unknown/src/main.rs
@@ -0,0 +1,6 @@
+fn main() {}
+
+#[kani::proof]
+fn harness_in_ws_package() {
+    assert!(1 + 1 == 2);
+}
diff --git a/tests/cargo-ui/ws-package-exclude/Cargo.toml b/tests/cargo-ui/ws-package-exclude/Cargo.toml
new file mode 100644
index 000000000000..50f7f55aac8f
--- /dev/null
+++ b/tests/cargo-ui/ws-package-exclude/Cargo.toml
@@ -0,0 +1,10 @@
+[package]
+name = "ws-package-exclude"
+version = "0.1.0"
+edition = "2021"
+
+[workspace]
+members = ["lib_package", "bin_package"]
+
+[workspace.metadata.kani.flags]
+exclude = ["ws-package-exclude"]
diff --git a/tests/cargo-ui/ws-package-exclude/bin_package/Cargo.toml b/tests/cargo-ui/ws-package-exclude/bin_package/Cargo.toml
new file mode 100644
index 000000000000..f6dc80f0babc
--- /dev/null
+++ b/tests/cargo-ui/ws-package-exclude/bin_package/Cargo.toml
@@ -0,0 +1,8 @@
+[package]
+name = "bin_package"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
diff --git a/tests/cargo-ui/ws-package-exclude/bin_package/src/main.rs b/tests/cargo-ui/ws-package-exclude/bin_package/src/main.rs
new file mode 100644
index 000000000000..47e452f47dd9
--- /dev/null
+++ b/tests/cargo-ui/ws-package-exclude/bin_package/src/main.rs
@@ -0,0 +1,6 @@
+fn main() {}
+
+#[kani::proof]
+fn harness_in_bin_package() {
+    assert!(1 + 1 == 2);
+}
\ No newline at end of file
diff --git a/tests/cargo-ui/ws-package-exclude/lib_package/Cargo.toml b/tests/cargo-ui/ws-package-exclude/lib_package/Cargo.toml
new file mode 100644
index 000000000000..d60143e79233
--- /dev/null
+++ b/tests/cargo-ui/ws-package-exclude/lib_package/Cargo.toml
@@ -0,0 +1,8 @@
+[package]
+name = "lib_package"
+version = "0.1.0"
+edition = "2021"
+
+[lib]
+name = "lib_package"
+path = "src/lib.rs"
diff --git a/tests/cargo-ui/ws-package-exclude/lib_package/src/lib.rs b/tests/cargo-ui/ws-package-exclude/lib_package/src/lib.rs
new file mode 100644
index 000000000000..a6a2da70c4f9
--- /dev/null
+++ b/tests/cargo-ui/ws-package-exclude/lib_package/src/lib.rs
@@ -0,0 +1,6 @@
+pub fn api() {}
+
+#[kani::proof]
+fn harness_in_lib_package() {
+    assert!(1 + 1 == 2);
+}
\ No newline at end of file
diff --git a/tests/cargo-ui/ws-package-exclude/src/main.rs b/tests/cargo-ui/ws-package-exclude/src/main.rs
new file mode 100644
index 000000000000..cec32d76fc4c
--- /dev/null
+++ b/tests/cargo-ui/ws-package-exclude/src/main.rs
@@ -0,0 +1,6 @@
+fn main() {}
+
+#[kani::proof]
+fn harness_in_ws_package() {
+    assert!(1 + 1 == 2);
+}
diff --git a/tests/cargo-ui/ws-package-select-unknown/Cargo.toml b/tests/cargo-ui/ws-package-select-unknown/Cargo.toml
new file mode 100644
index 000000000000..2c8e4822f3bf
--- /dev/null
+++ b/tests/cargo-ui/ws-package-select-unknown/Cargo.toml
@@ -0,0 +1,10 @@
+[package]
+name = "ws-package-select"
+version = "0.1.0"
+edition = "2021"
+
+[workspace]
+members = ["lib_package", "bin_package"]
+
+[workspace.metadata.kani.flags]
+package = ["unknown_package"]
diff --git a/tests/cargo-ui/ws-package-select-unknown/bin_package/Cargo.toml b/tests/cargo-ui/ws-package-select-unknown/bin_package/Cargo.toml
new file mode 100644
index 000000000000..f6dc80f0babc
--- /dev/null
+++ b/tests/cargo-ui/ws-package-select-unknown/bin_package/Cargo.toml
@@ -0,0 +1,8 @@
+[package]
+name = "bin_package"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
diff --git a/tests/cargo-ui/ws-package-select-unknown/bin_package/src/main.rs b/tests/cargo-ui/ws-package-select-unknown/bin_package/src/main.rs
new file mode 100644
index 000000000000..47e452f47dd9
--- /dev/null
+++ b/tests/cargo-ui/ws-package-select-unknown/bin_package/src/main.rs
@@ -0,0 +1,6 @@
+fn main() {}
+
+#[kani::proof]
+fn harness_in_bin_package() {
+    assert!(1 + 1 == 2);
+}
\ No newline at end of file
diff --git a/tests/cargo-ui/ws-package-select-unknown/lib_package/Cargo.toml b/tests/cargo-ui/ws-package-select-unknown/lib_package/Cargo.toml
new file mode 100644
index 000000000000..d60143e79233
--- /dev/null
+++ b/tests/cargo-ui/ws-package-select-unknown/lib_package/Cargo.toml
@@ -0,0 +1,8 @@
+[package]
+name = "lib_package"
+version = "0.1.0"
+edition = "2021"
+
+[lib]
+name = "lib_package"
+path = "src/lib.rs"
diff --git a/tests/cargo-ui/ws-package-select-unknown/lib_package/src/lib.rs b/tests/cargo-ui/ws-package-select-unknown/lib_package/src/lib.rs
new file mode 100644
index 000000000000..a6a2da70c4f9
--- /dev/null
+++ b/tests/cargo-ui/ws-package-select-unknown/lib_package/src/lib.rs
@@ -0,0 +1,6 @@
+pub fn api() {}
+
+#[kani::proof]
+fn harness_in_lib_package() {
+    assert!(1 + 1 == 2);
+}
\ No newline at end of file
diff --git a/tests/cargo-ui/ws-package-select-unknown/src/main.rs b/tests/cargo-ui/ws-package-select-unknown/src/main.rs
new file mode 100644
index 000000000000..cec32d76fc4c
--- /dev/null
+++ b/tests/cargo-ui/ws-package-select-unknown/src/main.rs
@@ -0,0 +1,6 @@
+fn main() {}
+
+#[kani::proof]
+fn harness_in_ws_package() {
+    assert!(1 + 1 == 2);
+}
diff --git a/tests/cargo-ui/ws-package-select/Cargo.toml b/tests/cargo-ui/ws-package-select/Cargo.toml
new file mode 100644
index 000000000000..a43d670c8a68
--- /dev/null
+++ b/tests/cargo-ui/ws-package-select/Cargo.toml
@@ -0,0 +1,10 @@
+[package]
+name = "ws-package-select"
+version = "0.1.0"
+edition = "2021"
+
+[workspace]
+members = ["lib_package", "bin_package"]
+
+[workspace.metadata.kani.flags]
+package = ["lib_package", "bin_package"]
diff --git a/tests/cargo-ui/ws-package-select/bin_package/Cargo.toml b/tests/cargo-ui/ws-package-select/bin_package/Cargo.toml
new file mode 100644
index 000000000000..f6dc80f0babc
--- /dev/null
+++ b/tests/cargo-ui/ws-package-select/bin_package/Cargo.toml
@@ -0,0 +1,8 @@
+[package]
+name = "bin_package"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
diff --git a/tests/cargo-ui/ws-package-select/bin_package/src/main.rs b/tests/cargo-ui/ws-package-select/bin_package/src/main.rs
new file mode 100644
index 000000000000..47e452f47dd9
--- /dev/null
+++ b/tests/cargo-ui/ws-package-select/bin_package/src/main.rs
@@ -0,0 +1,6 @@
+fn main() {}
+
+#[kani::proof]
+fn harness_in_bin_package() {
+    assert!(1 + 1 == 2);
+}
\ No newline at end of file
diff --git a/tests/cargo-ui/ws-package-select/lib_package/Cargo.toml b/tests/cargo-ui/ws-package-select/lib_package/Cargo.toml
new file mode 100644
index 000000000000..d60143e79233
--- /dev/null
+++ b/tests/cargo-ui/ws-package-select/lib_package/Cargo.toml
@@ -0,0 +1,8 @@
+[package]
+name = "lib_package"
+version = "0.1.0"
+edition = "2021"
+
+[lib]
+name = "lib_package"
+path = "src/lib.rs"
diff --git a/tests/cargo-ui/ws-package-select/lib_package/src/lib.rs b/tests/cargo-ui/ws-package-select/lib_package/src/lib.rs
new file mode 100644
index 000000000000..a6a2da70c4f9
--- /dev/null
+++ b/tests/cargo-ui/ws-package-select/lib_package/src/lib.rs
@@ -0,0 +1,6 @@
+pub fn api() {}
+
+#[kani::proof]
+fn harness_in_lib_package() {
+    assert!(1 + 1 == 2);
+}
\ No newline at end of file
diff --git a/tests/cargo-ui/ws-package-select/src/main.rs b/tests/cargo-ui/ws-package-select/src/main.rs
new file mode 100644
index 000000000000..cec32d76fc4c
--- /dev/null
+++ b/tests/cargo-ui/ws-package-select/src/main.rs
@@ -0,0 +1,6 @@
+fn main() {}
+
+#[kani::proof]
+fn harness_in_ws_package() {
+    assert!(1 + 1 == 2);
+}

From ffaecc44e88e3c1f3e8b546794114cbfa05397be Mon Sep 17 00:00:00 2001
From: Adrian Palacios <accorell@amazon.com>
Date: Thu, 20 Apr 2023 20:24:12 +0000
Subject: [PATCH 03/10] Format changes

---
 kani-driver/src/call_cargo.rs                                   | 2 +-
 .../cargo-ui/ws-package-exclude-unknown/bin_package/src/main.rs | 2 +-
 .../cargo-ui/ws-package-exclude-unknown/lib_package/src/lib.rs  | 2 +-
 tests/cargo-ui/ws-package-exclude/bin_package/src/main.rs       | 2 +-
 tests/cargo-ui/ws-package-exclude/lib_package/src/lib.rs        | 2 +-
 .../cargo-ui/ws-package-select-unknown/bin_package/src/main.rs  | 2 +-
 tests/cargo-ui/ws-package-select-unknown/lib_package/src/lib.rs | 2 +-
 tests/cargo-ui/ws-package-select/bin_package/src/main.rs        | 2 +-
 tests/cargo-ui/ws-package-select/lib_package/src/lib.rs         | 2 +-
 9 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs
index f9bd98d61abd..a748128049dd 100644
--- a/kani-driver/src/call_cargo.rs
+++ b/kani-driver/src/call_cargo.rs
@@ -273,7 +273,7 @@ fn validate_package_names(package_names: Vec<String>, packages: Vec<Package>) ->
         package_names.iter().filter(|pkg_name| !package_list.contains(pkg_name)).collect();
 
     // Some packages aren't in the workspace. Return an error which includes their names.
-    if unknown_packages.len() > 0 {
+    if !unknown_packages.is_empty() {
         let fmt_packages: Vec<String> =
             unknown_packages.iter().map(|pkg| format!("`{pkg}`")).collect();
         let error_msg = if unknown_packages.len() == 1 {
diff --git a/tests/cargo-ui/ws-package-exclude-unknown/bin_package/src/main.rs b/tests/cargo-ui/ws-package-exclude-unknown/bin_package/src/main.rs
index 47e452f47dd9..48adc4c92b74 100644
--- a/tests/cargo-ui/ws-package-exclude-unknown/bin_package/src/main.rs
+++ b/tests/cargo-ui/ws-package-exclude-unknown/bin_package/src/main.rs
@@ -3,4 +3,4 @@ fn main() {}
 #[kani::proof]
 fn harness_in_bin_package() {
     assert!(1 + 1 == 2);
-}
\ No newline at end of file
+}
diff --git a/tests/cargo-ui/ws-package-exclude-unknown/lib_package/src/lib.rs b/tests/cargo-ui/ws-package-exclude-unknown/lib_package/src/lib.rs
index a6a2da70c4f9..1194f0b46451 100644
--- a/tests/cargo-ui/ws-package-exclude-unknown/lib_package/src/lib.rs
+++ b/tests/cargo-ui/ws-package-exclude-unknown/lib_package/src/lib.rs
@@ -3,4 +3,4 @@ pub fn api() {}
 #[kani::proof]
 fn harness_in_lib_package() {
     assert!(1 + 1 == 2);
-}
\ No newline at end of file
+}
diff --git a/tests/cargo-ui/ws-package-exclude/bin_package/src/main.rs b/tests/cargo-ui/ws-package-exclude/bin_package/src/main.rs
index 47e452f47dd9..48adc4c92b74 100644
--- a/tests/cargo-ui/ws-package-exclude/bin_package/src/main.rs
+++ b/tests/cargo-ui/ws-package-exclude/bin_package/src/main.rs
@@ -3,4 +3,4 @@ fn main() {}
 #[kani::proof]
 fn harness_in_bin_package() {
     assert!(1 + 1 == 2);
-}
\ No newline at end of file
+}
diff --git a/tests/cargo-ui/ws-package-exclude/lib_package/src/lib.rs b/tests/cargo-ui/ws-package-exclude/lib_package/src/lib.rs
index a6a2da70c4f9..1194f0b46451 100644
--- a/tests/cargo-ui/ws-package-exclude/lib_package/src/lib.rs
+++ b/tests/cargo-ui/ws-package-exclude/lib_package/src/lib.rs
@@ -3,4 +3,4 @@ pub fn api() {}
 #[kani::proof]
 fn harness_in_lib_package() {
     assert!(1 + 1 == 2);
-}
\ No newline at end of file
+}
diff --git a/tests/cargo-ui/ws-package-select-unknown/bin_package/src/main.rs b/tests/cargo-ui/ws-package-select-unknown/bin_package/src/main.rs
index 47e452f47dd9..48adc4c92b74 100644
--- a/tests/cargo-ui/ws-package-select-unknown/bin_package/src/main.rs
+++ b/tests/cargo-ui/ws-package-select-unknown/bin_package/src/main.rs
@@ -3,4 +3,4 @@ fn main() {}
 #[kani::proof]
 fn harness_in_bin_package() {
     assert!(1 + 1 == 2);
-}
\ No newline at end of file
+}
diff --git a/tests/cargo-ui/ws-package-select-unknown/lib_package/src/lib.rs b/tests/cargo-ui/ws-package-select-unknown/lib_package/src/lib.rs
index a6a2da70c4f9..1194f0b46451 100644
--- a/tests/cargo-ui/ws-package-select-unknown/lib_package/src/lib.rs
+++ b/tests/cargo-ui/ws-package-select-unknown/lib_package/src/lib.rs
@@ -3,4 +3,4 @@ pub fn api() {}
 #[kani::proof]
 fn harness_in_lib_package() {
     assert!(1 + 1 == 2);
-}
\ No newline at end of file
+}
diff --git a/tests/cargo-ui/ws-package-select/bin_package/src/main.rs b/tests/cargo-ui/ws-package-select/bin_package/src/main.rs
index 47e452f47dd9..48adc4c92b74 100644
--- a/tests/cargo-ui/ws-package-select/bin_package/src/main.rs
+++ b/tests/cargo-ui/ws-package-select/bin_package/src/main.rs
@@ -3,4 +3,4 @@ fn main() {}
 #[kani::proof]
 fn harness_in_bin_package() {
     assert!(1 + 1 == 2);
-}
\ No newline at end of file
+}
diff --git a/tests/cargo-ui/ws-package-select/lib_package/src/lib.rs b/tests/cargo-ui/ws-package-select/lib_package/src/lib.rs
index a6a2da70c4f9..1194f0b46451 100644
--- a/tests/cargo-ui/ws-package-select/lib_package/src/lib.rs
+++ b/tests/cargo-ui/ws-package-select/lib_package/src/lib.rs
@@ -3,4 +3,4 @@ pub fn api() {}
 #[kani::proof]
 fn harness_in_lib_package() {
     assert!(1 + 1 == 2);
-}
\ No newline at end of file
+}

From 1737ceab1e9a7133648a9d353053c68428ba567d Mon Sep 17 00:00:00 2001
From: Adrian Palacios <accorell@amazon.com>
Date: Thu, 20 Apr 2023 20:31:05 +0000
Subject: [PATCH 04/10] Add missing copyright headers

---
 tests/cargo-ui/ws-package-exclude-unknown/Cargo.toml           | 3 +++
 .../cargo-ui/ws-package-exclude-unknown/bin_package/Cargo.toml | 3 +++
 .../ws-package-exclude-unknown/bin_package/src/main.rs         | 3 +++
 .../cargo-ui/ws-package-exclude-unknown/lib_package/Cargo.toml | 3 +++
 .../cargo-ui/ws-package-exclude-unknown/lib_package/src/lib.rs | 3 +++
 tests/cargo-ui/ws-package-exclude-unknown/src/main.rs          | 3 +++
 tests/cargo-ui/ws-package-exclude/Cargo.toml                   | 3 +++
 tests/cargo-ui/ws-package-exclude/bin_package/Cargo.toml       | 3 +++
 tests/cargo-ui/ws-package-exclude/bin_package/src/main.rs      | 3 +++
 tests/cargo-ui/ws-package-exclude/lib_package/Cargo.toml       | 3 +++
 tests/cargo-ui/ws-package-exclude/lib_package/src/lib.rs       | 3 +++
 tests/cargo-ui/ws-package-exclude/src/main.rs                  | 3 +++
 tests/cargo-ui/ws-package-select-unknown/Cargo.toml            | 3 +++
 .../cargo-ui/ws-package-select-unknown/bin_package/Cargo.toml  | 3 +++
 .../cargo-ui/ws-package-select-unknown/bin_package/src/main.rs | 3 +++
 .../cargo-ui/ws-package-select-unknown/lib_package/Cargo.toml  | 3 +++
 .../cargo-ui/ws-package-select-unknown/lib_package/src/lib.rs  | 3 +++
 tests/cargo-ui/ws-package-select-unknown/src/main.rs           | 3 +++
 tests/cargo-ui/ws-package-select/Cargo.toml                    | 3 +++
 tests/cargo-ui/ws-package-select/bin_package/Cargo.toml        | 3 +++
 tests/cargo-ui/ws-package-select/bin_package/src/main.rs       | 3 +++
 tests/cargo-ui/ws-package-select/lib_package/Cargo.toml        | 3 +++
 tests/cargo-ui/ws-package-select/lib_package/src/lib.rs        | 3 +++
 tests/cargo-ui/ws-package-select/src/main.rs                   | 3 +++
 24 files changed, 72 insertions(+)

diff --git a/tests/cargo-ui/ws-package-exclude-unknown/Cargo.toml b/tests/cargo-ui/ws-package-exclude-unknown/Cargo.toml
index 8b5c5ea760fc..bcd2e5c516ca 100644
--- a/tests/cargo-ui/ws-package-exclude-unknown/Cargo.toml
+++ b/tests/cargo-ui/ws-package-exclude-unknown/Cargo.toml
@@ -1,3 +1,6 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
 [package]
 name = "ws-package-exclude"
 version = "0.1.0"
diff --git a/tests/cargo-ui/ws-package-exclude-unknown/bin_package/Cargo.toml b/tests/cargo-ui/ws-package-exclude-unknown/bin_package/Cargo.toml
index f6dc80f0babc..d59b5b5d3c38 100644
--- a/tests/cargo-ui/ws-package-exclude-unknown/bin_package/Cargo.toml
+++ b/tests/cargo-ui/ws-package-exclude-unknown/bin_package/Cargo.toml
@@ -1,3 +1,6 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
 [package]
 name = "bin_package"
 version = "0.1.0"
diff --git a/tests/cargo-ui/ws-package-exclude-unknown/bin_package/src/main.rs b/tests/cargo-ui/ws-package-exclude-unknown/bin_package/src/main.rs
index 48adc4c92b74..de180796243a 100644
--- a/tests/cargo-ui/ws-package-exclude-unknown/bin_package/src/main.rs
+++ b/tests/cargo-ui/ws-package-exclude-unknown/bin_package/src/main.rs
@@ -1,3 +1,6 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
 fn main() {}
 
 #[kani::proof]
diff --git a/tests/cargo-ui/ws-package-exclude-unknown/lib_package/Cargo.toml b/tests/cargo-ui/ws-package-exclude-unknown/lib_package/Cargo.toml
index d60143e79233..3c9e2d8eac60 100644
--- a/tests/cargo-ui/ws-package-exclude-unknown/lib_package/Cargo.toml
+++ b/tests/cargo-ui/ws-package-exclude-unknown/lib_package/Cargo.toml
@@ -1,3 +1,6 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
 [package]
 name = "lib_package"
 version = "0.1.0"
diff --git a/tests/cargo-ui/ws-package-exclude-unknown/lib_package/src/lib.rs b/tests/cargo-ui/ws-package-exclude-unknown/lib_package/src/lib.rs
index 1194f0b46451..258267b336ff 100644
--- a/tests/cargo-ui/ws-package-exclude-unknown/lib_package/src/lib.rs
+++ b/tests/cargo-ui/ws-package-exclude-unknown/lib_package/src/lib.rs
@@ -1,3 +1,6 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
 pub fn api() {}
 
 #[kani::proof]
diff --git a/tests/cargo-ui/ws-package-exclude-unknown/src/main.rs b/tests/cargo-ui/ws-package-exclude-unknown/src/main.rs
index cec32d76fc4c..6b38aa656be5 100644
--- a/tests/cargo-ui/ws-package-exclude-unknown/src/main.rs
+++ b/tests/cargo-ui/ws-package-exclude-unknown/src/main.rs
@@ -1,3 +1,6 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
 fn main() {}
 
 #[kani::proof]
diff --git a/tests/cargo-ui/ws-package-exclude/Cargo.toml b/tests/cargo-ui/ws-package-exclude/Cargo.toml
index 50f7f55aac8f..87b85731c9f3 100644
--- a/tests/cargo-ui/ws-package-exclude/Cargo.toml
+++ b/tests/cargo-ui/ws-package-exclude/Cargo.toml
@@ -1,3 +1,6 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
 [package]
 name = "ws-package-exclude"
 version = "0.1.0"
diff --git a/tests/cargo-ui/ws-package-exclude/bin_package/Cargo.toml b/tests/cargo-ui/ws-package-exclude/bin_package/Cargo.toml
index f6dc80f0babc..d59b5b5d3c38 100644
--- a/tests/cargo-ui/ws-package-exclude/bin_package/Cargo.toml
+++ b/tests/cargo-ui/ws-package-exclude/bin_package/Cargo.toml
@@ -1,3 +1,6 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
 [package]
 name = "bin_package"
 version = "0.1.0"
diff --git a/tests/cargo-ui/ws-package-exclude/bin_package/src/main.rs b/tests/cargo-ui/ws-package-exclude/bin_package/src/main.rs
index 48adc4c92b74..de180796243a 100644
--- a/tests/cargo-ui/ws-package-exclude/bin_package/src/main.rs
+++ b/tests/cargo-ui/ws-package-exclude/bin_package/src/main.rs
@@ -1,3 +1,6 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
 fn main() {}
 
 #[kani::proof]
diff --git a/tests/cargo-ui/ws-package-exclude/lib_package/Cargo.toml b/tests/cargo-ui/ws-package-exclude/lib_package/Cargo.toml
index d60143e79233..3c9e2d8eac60 100644
--- a/tests/cargo-ui/ws-package-exclude/lib_package/Cargo.toml
+++ b/tests/cargo-ui/ws-package-exclude/lib_package/Cargo.toml
@@ -1,3 +1,6 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
 [package]
 name = "lib_package"
 version = "0.1.0"
diff --git a/tests/cargo-ui/ws-package-exclude/lib_package/src/lib.rs b/tests/cargo-ui/ws-package-exclude/lib_package/src/lib.rs
index 1194f0b46451..258267b336ff 100644
--- a/tests/cargo-ui/ws-package-exclude/lib_package/src/lib.rs
+++ b/tests/cargo-ui/ws-package-exclude/lib_package/src/lib.rs
@@ -1,3 +1,6 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
 pub fn api() {}
 
 #[kani::proof]
diff --git a/tests/cargo-ui/ws-package-exclude/src/main.rs b/tests/cargo-ui/ws-package-exclude/src/main.rs
index cec32d76fc4c..6b38aa656be5 100644
--- a/tests/cargo-ui/ws-package-exclude/src/main.rs
+++ b/tests/cargo-ui/ws-package-exclude/src/main.rs
@@ -1,3 +1,6 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
 fn main() {}
 
 #[kani::proof]
diff --git a/tests/cargo-ui/ws-package-select-unknown/Cargo.toml b/tests/cargo-ui/ws-package-select-unknown/Cargo.toml
index 2c8e4822f3bf..4031b38319ed 100644
--- a/tests/cargo-ui/ws-package-select-unknown/Cargo.toml
+++ b/tests/cargo-ui/ws-package-select-unknown/Cargo.toml
@@ -1,3 +1,6 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
 [package]
 name = "ws-package-select"
 version = "0.1.0"
diff --git a/tests/cargo-ui/ws-package-select-unknown/bin_package/Cargo.toml b/tests/cargo-ui/ws-package-select-unknown/bin_package/Cargo.toml
index f6dc80f0babc..d59b5b5d3c38 100644
--- a/tests/cargo-ui/ws-package-select-unknown/bin_package/Cargo.toml
+++ b/tests/cargo-ui/ws-package-select-unknown/bin_package/Cargo.toml
@@ -1,3 +1,6 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
 [package]
 name = "bin_package"
 version = "0.1.0"
diff --git a/tests/cargo-ui/ws-package-select-unknown/bin_package/src/main.rs b/tests/cargo-ui/ws-package-select-unknown/bin_package/src/main.rs
index 48adc4c92b74..de180796243a 100644
--- a/tests/cargo-ui/ws-package-select-unknown/bin_package/src/main.rs
+++ b/tests/cargo-ui/ws-package-select-unknown/bin_package/src/main.rs
@@ -1,3 +1,6 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
 fn main() {}
 
 #[kani::proof]
diff --git a/tests/cargo-ui/ws-package-select-unknown/lib_package/Cargo.toml b/tests/cargo-ui/ws-package-select-unknown/lib_package/Cargo.toml
index d60143e79233..3c9e2d8eac60 100644
--- a/tests/cargo-ui/ws-package-select-unknown/lib_package/Cargo.toml
+++ b/tests/cargo-ui/ws-package-select-unknown/lib_package/Cargo.toml
@@ -1,3 +1,6 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
 [package]
 name = "lib_package"
 version = "0.1.0"
diff --git a/tests/cargo-ui/ws-package-select-unknown/lib_package/src/lib.rs b/tests/cargo-ui/ws-package-select-unknown/lib_package/src/lib.rs
index 1194f0b46451..258267b336ff 100644
--- a/tests/cargo-ui/ws-package-select-unknown/lib_package/src/lib.rs
+++ b/tests/cargo-ui/ws-package-select-unknown/lib_package/src/lib.rs
@@ -1,3 +1,6 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
 pub fn api() {}
 
 #[kani::proof]
diff --git a/tests/cargo-ui/ws-package-select-unknown/src/main.rs b/tests/cargo-ui/ws-package-select-unknown/src/main.rs
index cec32d76fc4c..6b38aa656be5 100644
--- a/tests/cargo-ui/ws-package-select-unknown/src/main.rs
+++ b/tests/cargo-ui/ws-package-select-unknown/src/main.rs
@@ -1,3 +1,6 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
 fn main() {}
 
 #[kani::proof]
diff --git a/tests/cargo-ui/ws-package-select/Cargo.toml b/tests/cargo-ui/ws-package-select/Cargo.toml
index a43d670c8a68..cc4319f85789 100644
--- a/tests/cargo-ui/ws-package-select/Cargo.toml
+++ b/tests/cargo-ui/ws-package-select/Cargo.toml
@@ -1,3 +1,6 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
 [package]
 name = "ws-package-select"
 version = "0.1.0"
diff --git a/tests/cargo-ui/ws-package-select/bin_package/Cargo.toml b/tests/cargo-ui/ws-package-select/bin_package/Cargo.toml
index f6dc80f0babc..d59b5b5d3c38 100644
--- a/tests/cargo-ui/ws-package-select/bin_package/Cargo.toml
+++ b/tests/cargo-ui/ws-package-select/bin_package/Cargo.toml
@@ -1,3 +1,6 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
 [package]
 name = "bin_package"
 version = "0.1.0"
diff --git a/tests/cargo-ui/ws-package-select/bin_package/src/main.rs b/tests/cargo-ui/ws-package-select/bin_package/src/main.rs
index 48adc4c92b74..de180796243a 100644
--- a/tests/cargo-ui/ws-package-select/bin_package/src/main.rs
+++ b/tests/cargo-ui/ws-package-select/bin_package/src/main.rs
@@ -1,3 +1,6 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
 fn main() {}
 
 #[kani::proof]
diff --git a/tests/cargo-ui/ws-package-select/lib_package/Cargo.toml b/tests/cargo-ui/ws-package-select/lib_package/Cargo.toml
index d60143e79233..3c9e2d8eac60 100644
--- a/tests/cargo-ui/ws-package-select/lib_package/Cargo.toml
+++ b/tests/cargo-ui/ws-package-select/lib_package/Cargo.toml
@@ -1,3 +1,6 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
 [package]
 name = "lib_package"
 version = "0.1.0"
diff --git a/tests/cargo-ui/ws-package-select/lib_package/src/lib.rs b/tests/cargo-ui/ws-package-select/lib_package/src/lib.rs
index 1194f0b46451..258267b336ff 100644
--- a/tests/cargo-ui/ws-package-select/lib_package/src/lib.rs
+++ b/tests/cargo-ui/ws-package-select/lib_package/src/lib.rs
@@ -1,3 +1,6 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
 pub fn api() {}
 
 #[kani::proof]
diff --git a/tests/cargo-ui/ws-package-select/src/main.rs b/tests/cargo-ui/ws-package-select/src/main.rs
index cec32d76fc4c..6b38aa656be5 100644
--- a/tests/cargo-ui/ws-package-select/src/main.rs
+++ b/tests/cargo-ui/ws-package-select/src/main.rs
@@ -1,3 +1,6 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
 fn main() {}
 
 #[kani::proof]

From 7f8e38c4790faa5031559746cfa99b9f731a164c Mon Sep 17 00:00:00 2001
From: Adrian Palacios <accorell@amazon.com>
Date: Thu, 20 Apr 2023 20:42:37 +0000
Subject: [PATCH 05/10] Add descriptions to tests

---
 tests/cargo-ui/ws-package-exclude-unknown/Cargo.toml | 3 +++
 tests/cargo-ui/ws-package-exclude/Cargo.toml         | 3 +++
 tests/cargo-ui/ws-package-select-unknown/Cargo.toml  | 3 +++
 tests/cargo-ui/ws-package-select/Cargo.toml          | 3 +++
 4 files changed, 12 insertions(+)

diff --git a/tests/cargo-ui/ws-package-exclude-unknown/Cargo.toml b/tests/cargo-ui/ws-package-exclude-unknown/Cargo.toml
index bcd2e5c516ca..4ab747093447 100644
--- a/tests/cargo-ui/ws-package-exclude-unknown/Cargo.toml
+++ b/tests/cargo-ui/ws-package-exclude-unknown/Cargo.toml
@@ -1,6 +1,9 @@
 # Copyright Kani Contributors
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
+# This workspace test checks that the `--exclude` option prints a user-friendly
+# error when the package isn't found in the workspace.
+
 [package]
 name = "ws-package-exclude"
 version = "0.1.0"
diff --git a/tests/cargo-ui/ws-package-exclude/Cargo.toml b/tests/cargo-ui/ws-package-exclude/Cargo.toml
index 87b85731c9f3..50485b6c5cc2 100644
--- a/tests/cargo-ui/ws-package-exclude/Cargo.toml
+++ b/tests/cargo-ui/ws-package-exclude/Cargo.toml
@@ -1,6 +1,9 @@
 # Copyright Kani Contributors
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
+# This workspace test checks that the `--exclude` option removes the
+# `ws-package-exclude` package from the packages to verify.
+
 [package]
 name = "ws-package-exclude"
 version = "0.1.0"
diff --git a/tests/cargo-ui/ws-package-select-unknown/Cargo.toml b/tests/cargo-ui/ws-package-select-unknown/Cargo.toml
index 4031b38319ed..4346808d7352 100644
--- a/tests/cargo-ui/ws-package-select-unknown/Cargo.toml
+++ b/tests/cargo-ui/ws-package-select-unknown/Cargo.toml
@@ -1,6 +1,9 @@
 # Copyright Kani Contributors
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
+# This workspace test checks that the `--package` option prints a user-friendly
+# error when the package isn't found in the workspace.
+
 [package]
 name = "ws-package-select"
 version = "0.1.0"
diff --git a/tests/cargo-ui/ws-package-select/Cargo.toml b/tests/cargo-ui/ws-package-select/Cargo.toml
index cc4319f85789..254ba801b0bc 100644
--- a/tests/cargo-ui/ws-package-select/Cargo.toml
+++ b/tests/cargo-ui/ws-package-select/Cargo.toml
@@ -1,6 +1,9 @@
 # Copyright Kani Contributors
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
+# This workspace test checks that the `--package` option only includes the
+# `lib_package` and `bin_package` packages as the packages to verify.
+
 [package]
 name = "ws-package-select"
 version = "0.1.0"

From 75580f5fd8712acfa571c6f0ac24fc9d295054c4 Mon Sep 17 00:00:00 2001
From: Adrian Palacios <accorell@amazon.com>
Date: Thu, 20 Apr 2023 21:43:21 +0000
Subject: [PATCH 06/10] Require `--workspace`, and other minor fixes

---
 kani-driver/src/args.rs       | 4 ++--
 kani-driver/src/call_cargo.rs | 7 +------
 2 files changed, 3 insertions(+), 8 deletions(-)

diff --git a/kani-driver/src/args.rs b/kani-driver/src/args.rs
index a5a495564467..41f6e6b39d6d 100644
--- a/kani-driver/src/args.rs
+++ b/kani-driver/src/args.rs
@@ -320,8 +320,8 @@ pub struct CargoArgs {
     #[arg(long, short, conflicts_with("workspace"), num_args(1..))]
     pub package: Vec<String>,
 
-    /// Run Kani on the specified packages.
-    #[arg(long, short, conflicts_with("package"), num_args(1..))]
+    /// Exclude the specified packages
+    #[arg(long, short, requires("workspace"), conflicts_with("package"), num_args(1..))]
     pub exclude: Vec<String>,
 }
 
diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs
index a748128049dd..44223c4595f4 100644
--- a/kani-driver/src/call_cargo.rs
+++ b/kani-driver/src/call_cargo.rs
@@ -103,13 +103,8 @@ impl KaniSession {
         let mut pkg_args: Vec<String> = vec![];
         pkg_args.extend(["--".to_string(), self.reachability_arg()]);
 
-        let packages_to_verify = packages_to_verify(&self.args, &metadata);
-        if let Err(package_error) = packages_to_verify {
-            bail!(package_error)
-        };
-
         let mut found_target = false;
-        let packages = packages_to_verify.unwrap();
+        let packages = packages_to_verify(&self.args, &metadata)?;
         let mut artifacts = vec![];
         let mut failed_targets = vec![];
         for package in packages {

From a0de474a9cc02114a922affb72f4b6477c5ecdab Mon Sep 17 00:00:00 2001
From: Adrian Palacios <accorell@amazon.com>
Date: Thu, 20 Apr 2023 21:45:07 +0000
Subject: [PATCH 07/10] Add missing `expected` files

---
 tests/cargo-ui/ws-package-exclude-unknown/expected | 1 +
 tests/cargo-ui/ws-package-exclude/expected         | 3 +++
 tests/cargo-ui/ws-package-select-unknown/expected  | 1 +
 tests/cargo-ui/ws-package-select/expected          | 3 +++
 4 files changed, 8 insertions(+)
 create mode 100644 tests/cargo-ui/ws-package-exclude-unknown/expected
 create mode 100644 tests/cargo-ui/ws-package-exclude/expected
 create mode 100644 tests/cargo-ui/ws-package-select-unknown/expected
 create mode 100644 tests/cargo-ui/ws-package-select/expected

diff --git a/tests/cargo-ui/ws-package-exclude-unknown/expected b/tests/cargo-ui/ws-package-exclude-unknown/expected
new file mode 100644
index 000000000000..1473676bc28e
--- /dev/null
+++ b/tests/cargo-ui/ws-package-exclude-unknown/expected
@@ -0,0 +1 @@
+error: couldn't find package `unknown_package`
diff --git a/tests/cargo-ui/ws-package-exclude/expected b/tests/cargo-ui/ws-package-exclude/expected
new file mode 100644
index 000000000000..6f2886ae30fa
--- /dev/null
+++ b/tests/cargo-ui/ws-package-exclude/expected
@@ -0,0 +1,3 @@
+Checking harness harness_in_bin_package...
+Checking harness harness_in_lib_package...
+Complete - 2 successfully verified harnesses, 0 failures, 2 total.
diff --git a/tests/cargo-ui/ws-package-select-unknown/expected b/tests/cargo-ui/ws-package-select-unknown/expected
new file mode 100644
index 000000000000..1473676bc28e
--- /dev/null
+++ b/tests/cargo-ui/ws-package-select-unknown/expected
@@ -0,0 +1 @@
+error: couldn't find package `unknown_package`
diff --git a/tests/cargo-ui/ws-package-select/expected b/tests/cargo-ui/ws-package-select/expected
new file mode 100644
index 000000000000..6f2886ae30fa
--- /dev/null
+++ b/tests/cargo-ui/ws-package-select/expected
@@ -0,0 +1,3 @@
+Checking harness harness_in_bin_package...
+Checking harness harness_in_lib_package...
+Complete - 2 successfully verified harnesses, 0 failures, 2 total.

From 78acf19b20ee30f00e02961a89ae3e669d2d7cd8 Mon Sep 17 00:00:00 2001
From: Adrian Palacios <accorell@amazon.com>
Date: Thu, 20 Apr 2023 21:47:42 +0000
Subject: [PATCH 08/10] Pass `--workspace` to `--exclude`-related tests

---
 tests/cargo-ui/ws-package-exclude-unknown/Cargo.toml | 1 +
 tests/cargo-ui/ws-package-exclude/Cargo.toml         | 1 +
 2 files changed, 2 insertions(+)

diff --git a/tests/cargo-ui/ws-package-exclude-unknown/Cargo.toml b/tests/cargo-ui/ws-package-exclude-unknown/Cargo.toml
index 4ab747093447..b9f22dea8d69 100644
--- a/tests/cargo-ui/ws-package-exclude-unknown/Cargo.toml
+++ b/tests/cargo-ui/ws-package-exclude-unknown/Cargo.toml
@@ -13,4 +13,5 @@ edition = "2021"
 members = ["lib_package", "bin_package"]
 
 [workspace.metadata.kani.flags]
+workspace = true
 exclude = ["unknown_package"]
diff --git a/tests/cargo-ui/ws-package-exclude/Cargo.toml b/tests/cargo-ui/ws-package-exclude/Cargo.toml
index 50485b6c5cc2..d82bdd2efb9a 100644
--- a/tests/cargo-ui/ws-package-exclude/Cargo.toml
+++ b/tests/cargo-ui/ws-package-exclude/Cargo.toml
@@ -13,4 +13,5 @@ edition = "2021"
 members = ["lib_package", "bin_package"]
 
 [workspace.metadata.kani.flags]
+workspace = true
 exclude = ["ws-package-exclude"]

From 7ced745e5ef41f102f1c906f0776c72a722d79a8 Mon Sep 17 00:00:00 2001
From: Adrian Palacios <accorell@amazon.com>
Date: Thu, 20 Apr 2023 22:38:08 +0000
Subject: [PATCH 09/10] Borrow, not clone. Strategically change assertions in
 tests.

---
 kani-driver/src/call_cargo.rs                         | 6 +++---
 tests/cargo-ui/ws-package-exclude-unknown/src/main.rs | 2 +-
 tests/cargo-ui/ws-package-select/src/main.rs          | 2 +-
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs
index 44223c4595f4..469fd0698b18 100644
--- a/kani-driver/src/call_cargo.rs
+++ b/kani-driver/src/call_cargo.rs
@@ -262,7 +262,7 @@ fn print_msg(diagnostic: &Diagnostic, use_rendered: bool) -> Result<()> {
 }
 
 /// Check that all package names are present in the workspace, otherwise return which aren't.
-fn validate_package_names(package_names: Vec<String>, packages: Vec<Package>) -> Result<()> {
+fn validate_package_names(package_names: &Vec<String>, packages: &Vec<Package>) -> Result<()> {
     let package_list: Vec<String> = packages.iter().map(|pkg| pkg.name.clone()).collect();
     let unknown_packages: Vec<&String> =
         package_names.iter().filter(|pkg_name| !package_list.contains(pkg_name)).collect();
@@ -295,14 +295,14 @@ fn validate_package_names(package_names: Vec<String>, packages: Vec<Package>) ->
 fn packages_to_verify<'b>(args: &KaniArgs, metadata: &'b Metadata) -> Result<Vec<&'b Package>> {
     debug!(package_selection=?args.cargo.package, package_exclusion=?args.cargo.exclude, workspace=args.cargo.workspace, "packages_to_verify args");
     let packages = if !args.cargo.package.is_empty() {
-        validate_package_names(args.cargo.package.clone(), metadata.packages.clone())?;
+        validate_package_names(&args.cargo.package, &metadata.packages)?;
         args.cargo
             .package
             .iter()
             .map(|pkg_name| metadata.packages.iter().find(|pkg| pkg.name == *pkg_name).unwrap())
             .collect()
     } else if !args.cargo.exclude.is_empty() {
-        validate_package_names(args.cargo.exclude.clone(), metadata.packages.clone())?;
+        validate_package_names(&args.cargo.exclude, &metadata.packages)?;
         metadata.packages.iter().filter(|pkg| !args.cargo.exclude.contains(&pkg.name)).collect()
     } else {
         match (args.cargo.workspace, metadata.root_package()) {
diff --git a/tests/cargo-ui/ws-package-exclude-unknown/src/main.rs b/tests/cargo-ui/ws-package-exclude-unknown/src/main.rs
index 6b38aa656be5..2b98f4a53c6e 100644
--- a/tests/cargo-ui/ws-package-exclude-unknown/src/main.rs
+++ b/tests/cargo-ui/ws-package-exclude-unknown/src/main.rs
@@ -5,5 +5,5 @@ fn main() {}
 
 #[kani::proof]
 fn harness_in_ws_package() {
-    assert!(1 + 1 == 2);
+    assert!(1 + 1 == 3);
 }
diff --git a/tests/cargo-ui/ws-package-select/src/main.rs b/tests/cargo-ui/ws-package-select/src/main.rs
index 6b38aa656be5..2b98f4a53c6e 100644
--- a/tests/cargo-ui/ws-package-select/src/main.rs
+++ b/tests/cargo-ui/ws-package-select/src/main.rs
@@ -5,5 +5,5 @@ fn main() {}
 
 #[kani::proof]
 fn harness_in_ws_package() {
-    assert!(1 + 1 == 2);
+    assert!(1 + 1 == 3);
 }

From 54f1c4be6b78c2fd8d05aee5aebf8cb45e5770ef Mon Sep 17 00:00:00 2001
From: Adrian Palacios <accorell@amazon.com>
Date: Fri, 21 Apr 2023 13:59:35 +0000
Subject: [PATCH 10/10] Fix `clippy` error: Pass slices, not vectors

---
 kani-driver/src/call_cargo.rs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs
index 469fd0698b18..cddb01e71b50 100644
--- a/kani-driver/src/call_cargo.rs
+++ b/kani-driver/src/call_cargo.rs
@@ -262,7 +262,7 @@ fn print_msg(diagnostic: &Diagnostic, use_rendered: bool) -> Result<()> {
 }
 
 /// Check that all package names are present in the workspace, otherwise return which aren't.
-fn validate_package_names(package_names: &Vec<String>, packages: &Vec<Package>) -> Result<()> {
+fn validate_package_names(package_names: &[String], packages: &[Package]) -> Result<()> {
     let package_list: Vec<String> = packages.iter().map(|pkg| pkg.name.clone()).collect();
     let unknown_packages: Vec<&String> =
         package_names.iter().filter(|pkg_name| !package_list.contains(pkg_name)).collect();