-
Notifications
You must be signed in to change notification settings - Fork 126
Closed
Labels
[C] InternalTracks some internal work. I.e.: Users should not be affected.Tracks some internal work. I.e.: Users should not be affected.
Milestone
Description
The current structure of assess (#2029) looks like this:
- There is a basic assess (
cargo kani assess
) that functions a bit likecargo kani
orcargo build
in what it builds and analyzes. - 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:
- The existence of
scan
is frequently seen as just a metrics-gathering tool, not as something customer facing, despite its potential there. - "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.
- Zyad points out that "scan" could take a list of directories to scan, not just the current directory.
As an alternative, we could:
- Make "scan" the default behavior, and eliminate this subcommand.
- The actual single-package "assess" will become
cargo kani assess --manifest-path /path/to/Cargo.toml
- 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
Labels
[C] InternalTracks some internal work. I.e.: Users should not be affected.Tracks some internal work. I.e.: Users should not be affected.