Incorrect Error Reporting when Verifying Project containing Cargo Workspace

[Patrick-6]

Having a Rust project with a workspace and a subcrate, i.e., in Cargo.toml:

[workspace]
members = ["subcrate"]

Running verification with the Cargo.toml of the workspace in focus works as expected, but clicking Verify with Prusti when a file of the subcrate is in focus, will lead to incorrect error reporting by Prusti-Assistant:

Error when running from Cargo.toml:

lib.rs subcrate\src
[Prusti Verification Error] ...

Incorrect error when running on lib.rs directly:

lib.rs subcrate\subcrate\src
[Prusti Verification Error] ...

Clicking on the error will attempt to open the file subcrate/subcrate/src/lib.rs, which doesn't exist.

Running Cargo-Prusti from a terminal gives the same error message when running it from the outer or inner crate, which might be the cause for the problem in Prusti-Assistant:

error: [Prusti: verification error] the asserted expression might not hold
 --> subcrate/src/lib.rs:4:20
  |
4 |     prusti_assert!(x == 10);
  |                    ^^^^^^^
  |

[fpoli]

To fix this, we would need to obtain from cargo the root path of the workspace, so that we can use it in place of rootPath on the following line:

prusti-assistant/src/diagnostics.ts

Line 177 in e990a88

primaryFilePath = path.join(rootPath, primaryCallSiteSpans[0].file_name);

For example: cargo metadata --no-deps --offline outputs a JSON with a workspace_root key that seems to be exactly what we need.

[fpoli]

Even better, it would be nice to have rust-lang/cargo#9887