Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Mini-RFC: Assess/scan structure #2053

Open
tedinski opened this issue Dec 30, 2022 · 0 comments
Open

Mini-RFC: Assess/scan structure #2053

tedinski opened this issue Dec 30, 2022 · 0 comments
Labels
[C] Internal Tracks some internal work. I.e.: Users should not be affected.

Comments

@tedinski
Copy link
Contributor

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.

@tedinski tedinski added the [C] Internal Tracks some internal work. I.e.: Users should not be affected. label Dec 30, 2022
@tedinski tedinski added this to the Create Kani Assess tool milestone Jan 3, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
[C] Internal Tracks some internal work. I.e.: Users should not be affected.
Projects
None yet
Development

No branches or pull requests

1 participant