Finish deprecating --enable-unstable, --restrict-vtable, and --write-json-symtab
#4110
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
added 4 commits
May 27, 2025 10:21
this is just temporary; a subsequent PR will deprecate other options and revert this change
carolynzech
force-pushed
the
deprecation-error
branch
from
0db1a13 to
28040ba
Compare
Merged
thanhnguyen-aws
approved these changes
May 28, 2025
zhassan-aws
approved these changes
Jun 2, 2025
github-merge-queue bot
pushed a commit
that referenced
this pull request
Jun 4, 2025
1. Group options by category. We already have structs in the source code to do this (e.g. `CommonArgs`), so I just followed that structure. The goal is to make it easier for users to tell what the options do--I don't think it's currently clear that some of these arguments are for Cargo, for example. Open to bikeshedding on the section names--I think "Common Options" is a bit vague but couldn't think of anything better. 2. For each category, put its entries in alphabetical order. New output from `cargo kani -h` below. Note that #4110 will hide some of these options. ``` cmzech@80a9971b5e20 playground % cargo kani -h Verify a Rust crate. For more information, see https://github.com/model-checking/kani Usage: cargo-kani [OPTIONS] [COMMAND] Commands: autoharness Create and run harnesses automatically for eligible functions. Implies -Z function-contracts and -Z loop-contracts. See https://model-checking.github.io/kani/reference/experimental/autoharness.html for documentation list List contracts and harnesses playback Execute concrete playback testcases of a local package help Print this message or the help of the given subcommand(s) Options: -h, --help Print help (see more with '--help') -V, --version Print version Verification Options: --cbmc-args [<CBMC_ARGS>...] Pass through directly to CBMC; must be the last flag. This feature is unstable and it requires `-Z unstable-options` to be used --concrete-playback <CONCRETE_PLAYBACK> Generate concrete playback unit test. If value supplied is 'print', Kani prints the unit test to stdout. If value supplied is 'inplace', Kani automatically adds the unit test to your source code. This option does not work with `--output-format old` [possible values: print, inplace] --default-unwind <DEFAULT_UNWIND> Specify the value used for loop unwinding in CBMC --exact When specified, the harness filter will only match the exact fully qualified name of a harness --fail-fast Stop the verification process as soon as one of the harnesses fails --force-build Force Kani to rebuild all packages before the verification --harness <HARNESS_FILTER> If specified, only run harnesses that match this filter. This option can be provided multiple times, which will run all tests matching any of the filters. If used with --exact, the harness filter will only match the exact fully qualified name of a harness --harness-timeout <HARNESS_TIMEOUT> Timeout for each harness with optional suffix ('s': seconds, 'm': minutes, 'h': hours). Default is seconds. This option is experimental and requires `-Z unstable-options` to be used --no-assertion-reach-checks Turn off assertion reachability checks --output-format <OUTPUT_FORMAT> Toggle between different styles of output [default: regular] [possible values: regular, terse, old] --randomize-layout [<RANDOMIZE_LAYOUT>] Randomize the layout of structures. This option can help catching code that relies on a specific layout chosen by the compiler that is not guaranteed to be stable in the future. If a value is given, it will be used as the seed for randomization See the `-Z randomize-layout` and `-Z layout-seed` arguments of the rust compiler --solver <SOLVER> Specify the CBMC solver to use. Overrides the harness `solver` attribute. If no solver is specified (with --solver or harness attribute), Kani will use CaDiCaL [possible values: cadical, kissat, minisat, bin=<SAT_SOLVER_BINARY>] --target-dir <TARGET_DIR> Directory for all generated artifacts --tests Enable test function verification. Only use this option when the entry point is a test function --unwind <UNWIND> Specify the value used for loop unwinding for the specified harness in CBMC Memory Checks: --default-checks Turn on all default checks --no-default-checks Turn off all default checks --memory-safety-checks Turn on default memory safety checks --no-memory-safety-checks Turn off default memory safety checks --overflow-checks Turn on default overflow checks --no-overflow-checks Turn off default overflow checks --undefined-function-checks Turn on undefined function checks --no-undefined-function-checks Turn off undefined function checks --unwinding-checks Turn on default unwinding checks --no-unwinding-checks Turn off default unwinding checks Common Options: --debug Produce full debug information -q, --quiet Produces no output, just an exit code and requested artifacts; overrides --verbose -v, --verbose Output processing stages and commands, along with minor debug information -Z, --unstable <UNSTABLE_FEATURE> [possible values: async-lib, autoharness, concrete-playback, c-ffi, float-lib, function-contracts, gen-c, ghost-state, lean, list, loop-contracts, mem-predicates, restrict-vtable, source-coverage, stubbing, uninit-checks, unstable-options, valid-value-checks] Cargo Common Options: --all-features Activate all package features -e, --exclude <EXCLUDE>... Exclude the specified packages -F, --features <FEATURES> Comma separated list of package features to activate --manifest-path <PATH> Path to Cargo.toml --no-default-features Do not activate the `default` feature -p, --package <PACKAGE>... Run Kani on the specified packages (see `cargo help pkgid` for the accepted format) --workspace Build all packages in the workspace Cargo Target Options: --bin <BIN> Check only the specified binary target --bins Check all binaries --lib Check only the package's library unit tests ``` Resolves #1951 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
github-merge-queue bot
pushed a commit
that referenced
this pull request
Jun 9, 2025
These are the automatically-generated release notes: ``` ## What's Changed * Toolchain upgrade to nightly-2025-05-04 by @thanhnguyen-aws in #4059 * Automatic toolchain upgrade to nightly-2025-05-05 by @github-actions in #4060 * Automatic toolchain upgrade to nightly-2025-05-06 by @github-actions in #4061 * Enable target features: x87 and sse2 by @thanhnguyen-aws in #4062 * Fix the bug: Loop contracts are not composable with function contracts by @thanhnguyen-aws in #3979 * Automatic cargo update to 2025-05-12 by @github-actions in #4066 * Bump tests/perf/s2n-quic from `6aa9975` to `5f323b7` by @dependabot in #4068 * Fix stabilization instructions in RFC intro by @carolynzech in #4067 * Add support for quantifiers by @qinheping in #3993 * Toolchain upgrade to nightly-2025-05-07 by @thanhnguyen-aws in #4070 * Automatic toolchain upgrade to nightly-2025-05-08 by @github-actions in #4071 * Automatic toolchain upgrade to nightly-2025-05-09 by @github-actions in #4072 * Automatic toolchain upgrade to nightly-2025-05-10 by @github-actions in #4073 * Clippy/Stylistic Fixes by @carolynzech in #4074 * Upgrade toolchain to 2025-05-14 by @zhassan-aws in #4076 * Autoharness argument validation: only error on `--quiet` if `--list` was passed by @carolynzech in #4069 * Upgrade Rust toolchain to 2025-05-16 by @zhassan-aws in #4080 * Automatic toolchain upgrade to nightly-2025-05-17 by @github-actions in #4081 * Add setup scripts for Ubuntu 20.04 by @zhassan-aws in #4082 * Automatic toolchain upgrade to nightly-2025-05-18 by @github-actions in #4083 * Automatic cargo update to 2025-05-19 by @github-actions in #4086 * Automatic toolchain upgrade to nightly-2025-05-19 by @github-actions in #4085 * Automatic toolchain upgrade to nightly-2025-05-20 by @github-actions in #4091 * Bump tests/perf/s2n-quic from `5f323b7` to `22434aa` by @dependabot in #4089 * Fix the error that Kani panics when there is no external parameter in quantifier's closure. by @thanhnguyen-aws in #4088 * Update toolchain to 2025-05-22 by @carolynzech in #4098 * Use our toolchain when invoking `cargo metadata` by @carolynzech in #4090 * Automatic toolchain upgrade to nightly-2025-05-23 by @github-actions in #4099 * Automatic toolchain upgrade to nightly-2025-05-24 by @github-actions in #4101 * Automatic toolchain upgrade to nightly-2025-05-25 by @github-actions in #4102 * Fix a bug codegening `SwitchInt`s with only an otherwise branch by @bkirwi in #4095 * Automatic toolchain upgrade to nightly-2025-05-26 by @github-actions in #4104 * Automatic cargo update to 2025-05-26 by @github-actions in #4105 * Bump tests/perf/s2n-quic from `22434aa` to `550afb3` by @dependabot in #4106 * Automatic toolchain upgrade to nightly-2025-05-27 by @github-actions in #4107 * Update `kani::mem` pointer validity documentation by @carolynzech in #4092 * Add support for edition 2018 crates using assert! (Fixes #3717) by @sintemal in #4096 * Automatic toolchain upgrade to nightly-2025-05-28 by @github-actions in #4113 * Automatic toolchain upgrade to nightly-2025-05-29 by @github-actions in #4115 * Automatic toolchain upgrade to nightly-2025-05-30 by @github-actions in #4118 * Handle generic defaults in BoundedArbitrary derives by @zhassan-aws in #4117 * Automatic cargo update to 2025-06-02 by @github-actions in #4121 * Bump tests/perf/s2n-quic from `550afb3` to `8f54b57` by @dependabot in #4122 * Upgrade Rust toolchain to 2025-06-02 by @zhassan-aws in #4123 * Automatic toolchain upgrade to nightly-2025-06-03 by @github-actions in #4125 * Finish deprecating `--enable-unstable`, `--restrict-vtable`, and `--write-json-symtab` by @carolynzech in #4110 * `ty_mangled_name`: only use non-mangled name if `-Zcffi` is enabled. by @carolynzech in #4114 * Improve Help Menu by @carolynzech in #4109 * Start stabilizing `--jobs` and `list`; deprecate default memory checks by @carolynzech in #4108 * Refactor simd_bitmask to reduce the number of iterations by @zhassan-aws in #4129 * Set target features depending on the target architecture by @zhassan-aws in #4127 * Bump some versions suggested by cargo-outdated by @zhassan-aws in #4131 * Improve linking error output for `#[no_std]` crates by @AlexanderPortland in #4126 * Fix the git log command in the toolchain update script by @zhassan-aws in #4139 * Gate quantifiers behind an experimental feature by @thanhnguyen-aws in #4141 * Automatic cargo update to 2025-06-09 by @github-actions in #4145 ## New Contributors * @bkirwi made their first contribution in #4095 * @sintemal made their first contribution in #4096 * @AlexanderPortland made their first contribution in #4126 **Full Changelog**: kani-0.62.0...kani-0.63.0 ``` By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Carolyn Zech <[email protected]>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Make
--enable-unstable,--restrict-vtable, and--write-json-symtabhard errors.Resolves #3068
Towards #2279
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.