generated from amazon-archives/__template_Apache-2.0
-
Notifications
You must be signed in to change notification settings - Fork 130
Closed
Labels
[C] BugThis is a bug. Something isn't working.This is a bug. Something isn't working.[F] CrashKani crashedKani crashed
Description
Here's an example:
git clone https://github.com/serde-rs/json
cd json
cargo kani
This results in:
error: There are multiple `serde_json` packages in your project, and the specification `serde_json` is ambiguous.
Please re-run this command with `-p <spec>` where `<spec>` is one of the following:
file:///home/ubuntu/top-100-experiment/json#serde_json@1.0.91
https://github.com/rust-lang/crates.io-index#serde_json@1.0.91
Error: cargo exited with status exit status: 101
The problem is that we use cargo_metadata to examine which packages should be built, then pass each down with -p
. But that is ambiguous (apparently!) For example:
cargo build -p serde_json
gives the same error.
We can build the specific package with the suggested fix:
cargo build -p file:///home/ubuntu/top-100-experiment/json#serde_json@1.0.91
But not with kani:
cargo kani -p file:///home/ubuntu/top-100-experiment/json#serde_json@1.0.91
thread 'main' panicked at 'Cannot find package 'file:///home/ubuntu/top-100-experiment/json#serde_json@1.0.91'', kani-driver/src/call_cargo.rs:203:22
This is because our code tries to interpret package specs as if they were just package names.
The ideal fix would be to pass these arguments like -p
transparently down through to cargo build
without interpreting them.
As a bonus, this would parallelize builds of multiple packages and targets again.
Metadata
Metadata
Assignees
Labels
[C] BugThis is a bug. Something isn't working.This is a bug. Something isn't working.[F] CrashKani crashedKani crashed