From 96297969b3e7c4641a44377b490b782d822c065a Mon Sep 17 00:00:00 2001
From: Qinheping Hu <qinhh@amazon.com>
Date: Thu, 9 Jan 2025 16:09:45 -0600
Subject: [PATCH 1/3] Include manifest-path when checking if packages are in
 the workspace

---
 kani-driver/src/call_cargo.rs | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs
index 8677d312ad66..0bc716115989 100644
--- a/kani-driver/src/call_cargo.rs
+++ b/kani-driver/src/call_cargo.rs
@@ -371,6 +371,10 @@ crate-type = ["lib"]
             .map(|pkg| {
                 let mut cmd = setup_cargo_command()?;
                 cmd.arg("pkgid");
+                if let Some(path) = &self.args.cargo.manifest_path {
+                    cmd.arg("--manifest-path");
+                    cmd.arg(path);
+                }
                 cmd.arg(pkg);
                 // For some reason clippy cannot see that we are invoking wait() in the next line.
                 #[allow(clippy::zombie_processes)]

From cbab6880124a6dc5fb8ab17186c93becedde1aa4 Mon Sep 17 00:00:00 2001
From: Qinheping Hu <qinhh@amazon.com>
Date: Thu, 9 Jan 2025 19:21:54 -0600
Subject: [PATCH 2/3] Add a test

---
 tests/script-based-pre/cargo_manifest_test/add/Cargo.toml | 6 ++++++
 .../script-based-pre/cargo_manifest_test/add/src/main.rs  | 4 ++++
 tests/script-based-pre/cargo_manifest_test/config.yml     | 4 ++++
 .../cargo_manifest_test/manifest_test.expected            | 1 +
 .../script-based-pre/cargo_manifest_test/manifest_test.sh | 8 ++++++++
 5 files changed, 23 insertions(+)
 create mode 100644 tests/script-based-pre/cargo_manifest_test/add/Cargo.toml
 create mode 100644 tests/script-based-pre/cargo_manifest_test/add/src/main.rs
 create mode 100644 tests/script-based-pre/cargo_manifest_test/config.yml
 create mode 100644 tests/script-based-pre/cargo_manifest_test/manifest_test.expected
 create mode 100755 tests/script-based-pre/cargo_manifest_test/manifest_test.sh

diff --git a/tests/script-based-pre/cargo_manifest_test/add/Cargo.toml b/tests/script-based-pre/cargo_manifest_test/add/Cargo.toml
new file mode 100644
index 000000000000..f68ac5bd4734
--- /dev/null
+++ b/tests/script-based-pre/cargo_manifest_test/add/Cargo.toml
@@ -0,0 +1,6 @@
+[package]
+name = "add"
+version = "0.1.0"
+edition = "2021"
+
+[dependencies]
diff --git a/tests/script-based-pre/cargo_manifest_test/add/src/main.rs b/tests/script-based-pre/cargo_manifest_test/add/src/main.rs
new file mode 100644
index 000000000000..3c1ff20e0c4b
--- /dev/null
+++ b/tests/script-based-pre/cargo_manifest_test/add/src/main.rs
@@ -0,0 +1,4 @@
+#[kani::proof]
+fn main() {
+    1 + 1;
+}
diff --git a/tests/script-based-pre/cargo_manifest_test/config.yml b/tests/script-based-pre/cargo_manifest_test/config.yml
new file mode 100644
index 000000000000..671282d8be61
--- /dev/null
+++ b/tests/script-based-pre/cargo_manifest_test/config.yml
@@ -0,0 +1,4 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: manifest_test.sh
+expected: manifest_test.expected
diff --git a/tests/script-based-pre/cargo_manifest_test/manifest_test.expected b/tests/script-based-pre/cargo_manifest_test/manifest_test.expected
new file mode 100644
index 000000000000..01a90d50b557
--- /dev/null
+++ b/tests/script-based-pre/cargo_manifest_test/manifest_test.expected
@@ -0,0 +1 @@
+Complete - 1 successfully verified harnesses, 0 failures, 1 total.
diff --git a/tests/script-based-pre/cargo_manifest_test/manifest_test.sh b/tests/script-based-pre/cargo_manifest_test/manifest_test.sh
new file mode 100755
index 000000000000..d64229b35459
--- /dev/null
+++ b/tests/script-based-pre/cargo_manifest_test/manifest_test.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+# Test if Kani can correctly check if package in the workspace when
+# manifest-path presents.
+
+cargo kani --manifest-path=add/Cargo.toml --package add --debug

From ce4c8aab61c816cdbec4ac3e1cf8287484117599 Mon Sep 17 00:00:00 2001
From: Qinheping Hu <qinhh@amazon.com>
Date: Thu, 9 Jan 2025 19:24:20 -0600
Subject: [PATCH 3/3] Add copyright

---
 tests/script-based-pre/cargo_manifest_test/add/Cargo.toml  | 3 +++
 tests/script-based-pre/cargo_manifest_test/add/src/main.rs | 3 +++
 2 files changed, 6 insertions(+)

diff --git a/tests/script-based-pre/cargo_manifest_test/add/Cargo.toml b/tests/script-based-pre/cargo_manifest_test/add/Cargo.toml
index f68ac5bd4734..d5bc7d52c7c3 100644
--- a/tests/script-based-pre/cargo_manifest_test/add/Cargo.toml
+++ b/tests/script-based-pre/cargo_manifest_test/add/Cargo.toml
@@ -1,3 +1,6 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
 [package]
 name = "add"
 version = "0.1.0"
diff --git a/tests/script-based-pre/cargo_manifest_test/add/src/main.rs b/tests/script-based-pre/cargo_manifest_test/add/src/main.rs
index 3c1ff20e0c4b..672cb20a7e4d 100644
--- a/tests/script-based-pre/cargo_manifest_test/add/src/main.rs
+++ b/tests/script-based-pre/cargo_manifest_test/add/src/main.rs
@@ -1,3 +1,6 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
 #[kani::proof]
 fn main() {
     1 + 1;