kani icon indicating copy to clipboard operation
kani copied to clipboard

`kani-driver` argument parsing needs restructuring

Open tedinski opened this issue 3 years ago • 2 comments

Assess further compounded an already existing issue that we'll need to address before it gets too much worse.

Here are a few known issues, in no particular order:

  • [ ] Several kinds of options should be grouped together better: for example, --workspace --package --target-dir --all-features
  • [ ] Several flags only apply to cargo-kani or kani but appear in both: for example, the above do nothing for kani
  • [x] assess has a hack to add both a subcommand and --assess; this is solely to make it run in the test suite and the flag should be removed.
  • [ ] We should put together a specific set of supported options in Cargo.toml instead of trying to treat them as flags
  • [ ] The arguments/configuration should be more decoupled from KaniSession in kani-driver. (I'm not sure this means complete separation: we don't want pointlessly duplicate boilerplate, but we might try to break the configuration down into multiple structs instead of having just args.)
  • [ ] We badly need a "bless"-like UI test suite, to test all the help options to kani and cargo-kani.
  • [x] Assess currently takes "prepended flags" (like cargo kani --flag assess) and should not actually permit this

tedinski avatar Nov 01 '22 18:11 tedinski

Regarding the last topic:

[ ] Assess currently takes "prepended flags" (like cargo kani --flag assess) and should not actually permit this

we could use https://docs.rs/clap/latest/clap/struct.Command.html#method.args_conflicts_with_subcommands.

celinval avatar May 17 '23 19:05 celinval

I checked off the assess items assuming that we are deprecating assess per #4111

carolynzech avatar May 27 '25 22:05 carolynzech