Skip to content

Mini-RFC: Assess/scan structure #2053

@tedinski

Description

@tedinski

The current structure of assess (#2029) looks like this:

  1. There is a basic assess (cargo kani assess) that functions a bit like cargo kani or cargo build in what it builds and analyzes.
  2. There is a more general scan (cargo kani assess scan) that does a more explicit search for package to run assess on.

There are a few problems with this structure:

  1. The existence of scan is frequently seen as just a metrics-gathering tool, not as something customer facing, despite its potential there.
  2. "Scan" actually has the opportunity to do a bit better than regular assess (on a workspace), because it can tolerate compiler crashes by skipping over the crashing package and proceeding with the rest.
  3. Zyad points out that "scan" could take a list of directories to scan, not just the current directory.

As an alternative, we could:

  1. Make "scan" the default behavior, and eliminate this subcommand.
  2. The actual single-package "assess" will become cargo kani assess --manifest-path /path/to/Cargo.toml
  3. Assess, when not given a specific manifest, could also take a list of directories to scan. This should make it easier to "subset" a workspace too, for instance cargo kani assess kani-driver/. (Or we could use a flag for this.)

This structure might be better for customers and make the behavior clearer.

Metadata

Metadata

Assignees

No one assigned

    Labels

    [C] InternalTracks some internal work. I.e.: Users should not be affected.

    Type

    No type

    Projects

    No projects

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions