generated from amazon-archives/__template_Apache-2.0
-
Notifications
You must be signed in to change notification settings - Fork 130
Open
Labels
[C] InternalTracks some internal work. I.e.: Users should not be affected.Tracks some internal work. I.e.: Users should not be affected.
Description
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
orkani
but appear in both: for example, the above do nothing forkani
-
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
inkani-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 multiplestructs
instead of having justargs
.) - We badly need a "bless"-like UI test suite, to test all the help options to
kani
andcargo-kani
. - Assess currently takes "prepended flags" (like
cargo kani --flag assess
) and should not actually permit this
celinval
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.