Kani doesn't consider cargo arguments when finding the packages in a workspace

[carolynzech]

I tried this code: parent.zip

using the following command line invocation:

cargo kani --manifest-path=manifest-test/add/Cargo.toml --package add --debug

with Kani version: 0.57

I expected to see this happen: verification of the harness succeeds.

Instead, this happened:

cargo kani --manifest-path=manifest-test/add/Cargo.toml --package add --debug
Kani Rust Verifier 0.57.0 (cargo plugin)
kani_driver::call_cargo: packages_to_verify args package_selection=["add"] package_exclusion=[] workspace=false
[Kani] Running: `/Users/cmzech/.kani/kani-0.57.0/toolchain/bin/cargo pkgid add`
error: could not find `Cargo.toml` in `/Users/cmzech/parent` or any parent directory
2025-01-07T20:19:51.627821Z DEBUG kani_driver: main_failure error=Failed to retrieve information for `add`
error: Failed to retrieve information for `add`

With Kani v0.56, verification succeeds.

The solution is to update the to_package_ids function introduced in #3593 to include --manifest-path (and any other provided cargo arguments) as part of the command, i.e.:

fn to_package_ids<'a>(..) {
 let mut cmd = setup_cargo_command()?;
 cmd.arg("pkgid");
 cmd.arg(pkg);
 // include --manifest-path if provided
... }