kani
kani copied to clipboard
`kani-driver` argument parsing needs restructuring
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-kaniorkanibut appear in both: for example, the above do nothing forkani - [x]
assesshas 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.tomlinstead of trying to treat them as flags - [ ] The arguments/configuration should be more decoupled from
KaniSessioninkani-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 multiplestructsinstead of having justargs.) - [ ] We badly need a "bless"-like UI test suite, to test all the help options to
kaniandcargo-kani. - [x] Assess currently takes "prepended flags" (like
cargo kani --flag assess) and should not actually permit this
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.
I checked off the assess items assuming that we are deprecating assess per #4111