Skip to content

Kani is unable to build some crates due to package naming #2104

@tedinski

Description

@tedinski

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

No one assigned

    Labels

    [C] BugThis is a bug. Something isn't working.[F] CrashKani crashed

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions