Skip to content

kani-driver argument parsing needs restructuring #1831

@tedinski

Description

@tedinski

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
  • 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.
  • Assess currently takes "prepended flags" (like cargo kani --flag assess) and should not actually permit this

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

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions