Include manifest-path when checking if packages are in the workspace (#…

…3819)

With this PR, we include `--manifest-path` in `to_package_ids` function
as part of the command.

Resolves #3816

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: Zyad Hassan <[email protected]>

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)]

tests/script-based-pre/cargo_manifest_test/add/Cargo.toml

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

tests/script-based-pre/cargo_manifest_test/add/src/main.rs

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

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

tests/script-based-pre/cargo_manifest_test/manifest_test.expected

@@ -0,0 +1 @@
+Complete - 1 successfully verified harnesses, 0 failures, 1 total.

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 present.
+
+cargo kani --manifest-path=add/Cargo.toml --package add --debug