diff --git a/kani-driver/src/args/autoharness_args.rs b/kani-driver/src/args/autoharness_args.rs index 8b7b66c4cd7c..6d329627bd13 100644 --- a/kani-driver/src/args/autoharness_args.rs +++ b/kani-driver/src/args/autoharness_args.rs @@ -31,7 +31,7 @@ pub struct CommonAutoharnessArgs { #[arg(long = "exclude-pattern", num_args(1), value_name = "PATTERN")] pub exclude_pattern: Vec, - /// Run the `list` subcommand after generating the automatic harnesses. Requires -Z list. Note that this option implies --only-codegen. + /// Run the `list` subcommand after generating the automatic harnesses. Note that this option implies --only-codegen. #[arg(long)] pub list: bool, @@ -85,15 +85,6 @@ impl ValidateArgs for CargoAutoharnessArgs { )); } - if self.common_autoharness_args.list - && !self.verify_opts.common_args.unstable_features.contains(UnstableFeature::List) - { - return Err(Error::raw( - ErrorKind::MissingRequiredArgument, - format!("The `list` feature is unstable and requires -Z {}", UnstableFeature::List), - )); - } - if self.common_autoharness_args.list && self.common_autoharness_args.format == Format::Pretty && self.verify_opts.common_args.quiet @@ -133,15 +124,6 @@ impl ValidateArgs for StandaloneAutoharnessArgs { )); } - if self.common_autoharness_args.list - && !self.verify_opts.common_args.unstable_features.contains(UnstableFeature::List) - { - return Err(Error::raw( - ErrorKind::MissingRequiredArgument, - format!("The `list` feature is unstable and requires -Z {}", UnstableFeature::List), - )); - } - if self.common_autoharness_args.list && self.common_autoharness_args.format == Format::Pretty && self.verify_opts.common_args.quiet diff --git a/kani-driver/src/args/common.rs b/kani-driver/src/args/common.rs index 709de6439fe9..340e30ca4d29 100644 --- a/kani-driver/src/args/common.rs +++ b/kani-driver/src/args/common.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT //! Define arguments that should be common to all subcommands in Kani. -use crate::args::ValidateArgs; +use crate::args::{ValidateArgs, print_stabilized_feature_warning}; use clap::{error::Error, error::ErrorKind}; pub use kani_metadata::{EnabledUnstableFeatures, UnstableFeature}; @@ -40,6 +40,21 @@ impl ValidateArgs for CommonArgs { "The `--dry-run` option is obsolete. Use --verbose instead.", )); } + if self.enable_unstable { + return Err(Error::raw( + ErrorKind::ValueValidation, + "The `--enable-unstable` option is obsolete. Enable the appropriate unstable feature(s) with `-Z {feature}` instead.", + )); + } + + // Warn if a deprecated unstable feature is enabled. + for feature in self.unstable_features.iter() { + let stabilization_version = feature.stabilization_version(); + if let Some(version) = stabilization_version { + print_stabilized_feature_warning(self, *feature, &version); + } + } + Ok(()) } } @@ -52,22 +67,13 @@ impl CommonArgs { required: UnstableFeature, ) -> Result<(), Error> { if enabled && !self.unstable_features.contains(required) { - let z_feature = format!("-Z {required}"); - if self.enable_unstable { - return Err(Error::raw( - ErrorKind::ValueValidation, - format!( - "The `--enable-unstable` option is obsolete. Use `{z_feature}` instead.", - ), - )); - } else { - return Err(Error::raw( - ErrorKind::MissingRequiredArgument, - format!( - "The `{argument}` argument is unstable and requires `{z_feature}` to be used.", - ), - )); - } + return Err(Error::raw( + ErrorKind::MissingRequiredArgument, + format!( + "The `--{argument}` option is unstable and requires `{}` to be used.", + required.as_argument_string() + ), + )); } Ok(()) } diff --git a/kani-driver/src/args/list_args.rs b/kani-driver/src/args/list_args.rs index 1d84f5706812..f01dd1484b5c 100644 --- a/kani-driver/src/args/list_args.rs +++ b/kani-driver/src/args/list_args.rs @@ -6,7 +6,6 @@ use std::path::PathBuf; use crate::args::{CommonArgs, ValidateArgs, validate_std_path}; use clap::{Error, Parser, ValueEnum, error::ErrorKind}; -use kani_metadata::UnstableFeature; /// List information relevant to verification #[derive(Debug, Parser)] @@ -57,12 +56,6 @@ pub enum Format { impl ValidateArgs for CargoListArgs { fn validate(&self) -> Result<(), Error> { self.common_args.validate()?; - if !self.common_args.unstable_features.contains(UnstableFeature::List) { - return Err(Error::raw( - ErrorKind::MissingRequiredArgument, - "The `list` subcommand is unstable and requires -Z list", - )); - } if self.format == Format::Pretty && self.common_args.quiet { return Err(Error::raw( @@ -78,12 +71,6 @@ impl ValidateArgs for CargoListArgs { impl ValidateArgs for StandaloneListArgs { fn validate(&self) -> Result<(), Error> { self.common_args.validate()?; - if !self.common_args.unstable_features.contains(UnstableFeature::List) { - return Err(Error::raw( - ErrorKind::MissingRequiredArgument, - "The `list` subcommand is unstable and requires -Z list", - )); - } if self.format == Format::Pretty && self.common_args.quiet { return Err(Error::raw( diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index f75995804ca2..13a4175a6d99 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -53,11 +53,40 @@ pub fn print_obsolete(verbosity: &CommonArgs, option: &str) { } #[allow(dead_code)] -pub fn print_deprecated(verbosity: &CommonArgs, option: &str, alternative: &str) { +pub fn print_deprecated(verbosity: &CommonArgs, option: &str, version: &str, alternative: &str) { if !verbosity.quiet { warning(&format!( - "The `{option}` option is deprecated. This option will be removed soon. \ - Consider using `{alternative}` instead" + "The `{option}` option has been deprecated since {version} and will be removed soon. \ + Consider {alternative} instead" + )) + } +} + +/// First step in two-phase stabilization. +/// When an unstable option is first stabilized, print this warning that `-Z unstable-options` has no effect. +/// This warning should last for one release only; in the next Kani release, remove it. +pub fn print_stabilized_option_warning(verbosity: &CommonArgs, option: &str, version: &str) { + if !verbosity.quiet { + warning(&format!( + "The `--{option}` option has been stable since {version} and no longer requires {} to enable. \ + Remove it unless it is needed for another unstable option.", + UnstableFeature::UnstableOptions.as_argument_string(), + )) + } +} + +/// First step in two-phase stabilization. +/// When an unstable feature is first stabilized, print this warning that `-Z {feature}` has no effect. +/// This warning should last for one release only; in the next Kani release, remove it. +pub fn print_stabilized_feature_warning( + verbosity: &CommonArgs, + feature: UnstableFeature, + version: &str, +) { + if !verbosity.quiet { + warning(&format!( + "The `{feature}` feature has been stable since {version} and no longer requires {} to enable", + feature.as_argument_string() )) } } @@ -185,6 +214,7 @@ pub enum CargoKaniSubcommand { // Common arguments for invoking Kani for verification purpose. This gets put into KaniContext, // whereas anything above is "local" to "main"'s control flow. +// When adding an argument to this struct, make sure that it's in alphabetical order as displayed to the user when running --help. #[derive(Debug, clap::Args)] #[clap(next_help_heading = "Verification Options")] pub struct VerificationArgs { @@ -376,7 +406,6 @@ impl VerificationArgs { pub fn restrict_vtable(&self) -> bool { self.common_args.unstable_features.contains(UnstableFeature::RestrictVtable) && !self.no_restrict_vtable - // if we flip the default, this will become: !self.no_restrict_vtable } /// Assertion reachability checks should be disabled @@ -393,6 +422,24 @@ impl VerificationArgs { } } + /// Given an argument, warn if UnstableFeature::UnstableOptions is enabled. + /// This is for cases where the option was previously unstable but has since been stabilized. + pub fn check_unnecessary_unstable_option(&self, enabled: bool, option: &str) { + fn stabilization_version(option: &str) -> Option { + match option { + "jobs" => Some("0.63.0".to_string()), + _ => None, + } + } + let stabilization_version = stabilization_version(option); + if let Some(version) = stabilization_version + && enabled + && self.common_args.unstable_features.contains(UnstableFeature::UnstableOptions) + { + print_stabilized_option_warning(&self.common_args, option, &version) + } + } + /// Computes how many threads should be used to verify harnesses. pub fn jobs(&self) -> Option { match self.jobs { @@ -435,35 +482,35 @@ pub struct CheckArgs { // Rust argument parsers (/clap) don't have the convenient '--flag' and '--no-flag' boolean pairs, so approximate // We're put both here then create helper functions to "intepret" /// Turn on all default checks - #[arg(long)] + #[arg(long, hide = true)] pub default_checks: bool, /// Turn off all default checks #[arg(long)] pub no_default_checks: bool, /// Turn on default memory safety checks - #[arg(long)] + #[arg(long, hide = true)] pub memory_safety_checks: bool, /// Turn off default memory safety checks #[arg(long)] pub no_memory_safety_checks: bool, /// Turn on default overflow checks - #[arg(long)] + #[arg(long, hide = true)] pub overflow_checks: bool, /// Turn off default overflow checks #[arg(long)] pub no_overflow_checks: bool, /// Turn on undefined function checks - #[arg(long)] + #[arg(long, hide = true)] pub undefined_function_checks: bool, /// Turn off undefined function checks #[arg(long)] pub no_undefined_function_checks: bool, /// Turn on default unwinding checks - #[arg(long)] + #[arg(long, hide = true)] pub unwinding_checks: bool, /// Turn off default unwinding checks #[arg(long)] @@ -484,6 +531,30 @@ impl CheckArgs { pub fn unwinding_on(&self) -> bool { !self.no_default_checks && !self.no_unwinding_checks || self.unwinding_checks } + pub fn print_deprecated(&self, verbosity: &CommonArgs) { + let deprecation_version = "0.63.0"; + let alternative = "omitting the argument, since this is already the default behavior"; + if self.default_checks { + print_deprecated(verbosity, "--default-checks", deprecation_version, alternative); + } + if self.memory_safety_checks { + print_deprecated(verbosity, "--memory-safety-checks", deprecation_version, alternative); + } + if self.overflow_checks { + print_deprecated(verbosity, "--overflow-checks", deprecation_version, alternative); + } + if self.undefined_function_checks { + print_deprecated( + verbosity, + "--undefined-function-checks", + deprecation_version, + alternative, + ); + } + if self.unwinding_checks { + print_deprecated(verbosity, "--unwinding-checks", deprecation_version, alternative); + } + } } /// Utility function to error out on arguments that are invalid Cargo specific. @@ -580,239 +651,222 @@ impl ValidateArgs for CargoKaniArgs { impl ValidateArgs for VerificationArgs { fn validate(&self) -> Result<(), Error> { self.common_args.validate()?; - let extra_unwind = - self.cbmc_args.iter().any(|s| s.to_str().unwrap().starts_with("--unwind")); - let natives_unwind = self.default_unwind.is_some() || self.unwind.is_some(); - if self.randomize_layout.is_some() && self.concrete_playback.is_some() { - let random_seed = if let Some(seed) = self.randomize_layout.unwrap() { - format!(" -Z layout-seed={seed}") - } else { - String::new() - }; + // check_unstable() calls: for each unstable option, check that the requisite unstable feature is provided. + let unstable = || -> Result<(), Error> { + self.common_args.check_unstable( + self.concrete_playback.is_some(), + "concrete-playback", + UnstableFeature::ConcretePlayback, + )?; + + self.common_args.check_unstable( + !self.c_lib.is_empty(), + "c-lib", + UnstableFeature::CFfi, + )?; + + self.common_args.check_unstable( + self.gen_c, + "gen-c", + UnstableFeature::UnstableOptions, + )?; + + self.common_args.check_unstable( + !self.cbmc_args.is_empty(), + "cbmc-args", + UnstableFeature::UnstableOptions, + )?; + + self.common_args.check_unstable( + self.no_codegen, + "no-codegen", + UnstableFeature::UnstableOptions, + )?; + + self.common_args.check_unstable( + self.extra_pointer_checks, + "extra-pointer-checks", + UnstableFeature::UnstableOptions, + )?; + + self.common_args.check_unstable( + self.ignore_global_asm, + "ignore-asm", + UnstableFeature::UnstableOptions, + )?; + + self.common_args.check_unstable( + self.run_sanity_checks, + "run-sanity-checks", + UnstableFeature::UnstableOptions, + )?; + + self.common_args.check_unstable( + self.no_slice_formula, + "no-slice-formula", + UnstableFeature::UnstableOptions, + )?; + + self.common_args.check_unstable( + self.synthesize_loop_contracts, + "synthesize-loop-contracts", + UnstableFeature::UnstableOptions, + )?; + + self.common_args.check_unstable( + self.no_restrict_vtable, + "no-restrict-vtable", + UnstableFeature::RestrictVtable, + )?; + + self.common_args.check_unstable( + self.coverage, + "coverage", + UnstableFeature::SourceCoverage, + )?; + self.common_args.check_unstable( + self.output_into_files, + "output-into-files", + UnstableFeature::UnstableOptions, + )?; + self.common_args.check_unstable( + self.print_llbc, + "print-llbc", + UnstableFeature::Lean, + )?; + self.common_args.check_unstable( + self.harness_timeout.is_some(), + "harness-timeout", + UnstableFeature::UnstableOptions, + )?; + self.common_args.check_unstable( + self.no_assert_contracts, + "no-assert", + UnstableFeature::FunctionContracts, + )?; - println!( - "Using concrete playback with --randomize-layout.\n\ - The produced tests will have to be played with the same rustc arguments:\n\ - -Z randomize-layout{random_seed}" - ); - } + Ok(()) + }; - if self.write_json_symtab { - return Err(Error::raw( - ErrorKind::ValueValidation, - "The `--write-json-symtab` option is obsolete.", - )); - } + // Check for argument conflicts. + let conflicting_options = || -> Result<(), Error> { + let extra_unwind = + self.cbmc_args.iter().any(|s| s.to_str().unwrap().starts_with("--unwind")); + let natives_unwind = self.default_unwind.is_some() || self.unwind.is_some(); - // TODO: these conflicting flags reflect what's necessary to pass current tests unmodified. - // We should consider improving the error messages slightly in a later pull request. - if natives_unwind && extra_unwind { - return Err(Error::raw( - ErrorKind::ArgumentConflict, - "Conflicting flags: unwind flags provided to kani and in --cbmc-args.", - )); - } - if self.cbmc_args.contains(&OsString::from("--function")) { - return Err(Error::raw( - ErrorKind::ArgumentConflict, - "Invalid flag: --function is not supported in Kani.", - )); - } - if self.common_args.quiet && self.concrete_playback == Some(ConcretePlaybackMode::Print) { - return Err(Error::raw( - ErrorKind::ArgumentConflict, - "Conflicting options: --concrete-playback=print and --quiet.", - )); - } - if self.concrete_playback.is_some() && self.output_format == OutputFormat::Old { - return Err(Error::raw( - ErrorKind::ArgumentConflict, - "Conflicting options: --concrete-playback isn't compatible with \ + // TODO: these conflicting flags reflect what's necessary to pass current tests unmodified. + // We should consider improving the error messages slightly in a later pull request. + if natives_unwind && extra_unwind { + return Err(Error::raw( + ErrorKind::ArgumentConflict, + "Conflicting flags: unwind flags provided to kani and in --cbmc-args.", + )); + } + if self.cbmc_args.contains(&OsString::from("--function")) { + return Err(Error::raw( + ErrorKind::ArgumentConflict, + "Invalid flag: --function is not supported in Kani.", + )); + } + if self.common_args.quiet && self.concrete_playback == Some(ConcretePlaybackMode::Print) + { + return Err(Error::raw( + ErrorKind::ArgumentConflict, + "Conflicting options: --concrete-playback=print and --quiet.", + )); + } + if self.concrete_playback.is_some() && self.output_format == OutputFormat::Old { + return Err(Error::raw( + ErrorKind::ArgumentConflict, + "Conflicting options: --concrete-playback isn't compatible with \ --output-format=old.", - )); - } - if self.concrete_playback.is_some() && self.jobs() != Some(1) { - // Concrete playback currently embeds a lot of assumptions about the order in which harnesses get called. - return Err(Error::raw( - ErrorKind::ArgumentConflict, - "Conflicting options: --concrete-playback isn't compatible with --jobs.", - )); - } - if self.jobs.is_some() && self.output_format != OutputFormat::Terse { - // More verbose output formats make it hard to interpret output right now when run in parallel. - // This can be removed when we change up how results are printed. - return Err(Error::raw( - ErrorKind::ArgumentConflict, - "Conflicting options: --jobs requires `--output-format=terse`", - )); - } - if let Some(out_dir) = &self.target_dir - && out_dir.exists() - && !out_dir.is_dir() - { - return Err(Error::raw( - ErrorKind::InvalidValue, - format!( - "Invalid argument: `--target-dir` argument `{}` is not a directory", - out_dir.display() - ), - )); - } - - self.common_args.check_unstable( - self.concrete_playback.is_some(), - "--concrete-playback", - UnstableFeature::ConcretePlayback, - )?; - - self.common_args.check_unstable( - !self.c_lib.is_empty(), - "--c-lib", - UnstableFeature::CFfi, - )?; - - self.common_args.check_unstable(self.gen_c, "--gen-c", UnstableFeature::UnstableOptions)?; - - self.common_args.check_unstable( - !self.cbmc_args.is_empty(), - "--cbmc-args", - UnstableFeature::UnstableOptions, - )?; - - self.common_args.check_unstable( - self.no_codegen, - "--no-codegen", - UnstableFeature::UnstableOptions, - )?; - - self.common_args.check_unstable( - self.jobs.is_some(), - "--jobs", - UnstableFeature::UnstableOptions, - )?; - - self.common_args.check_unstable( - self.extra_pointer_checks, - "--extra-pointer-checks", - UnstableFeature::UnstableOptions, - )?; - - self.common_args.check_unstable( - self.ignore_global_asm, - "--ignore-global-asm", - UnstableFeature::UnstableOptions, - )?; - - self.common_args.check_unstable( - self.run_sanity_checks, - "--run-sanity-checks", - UnstableFeature::UnstableOptions, - )?; - - self.common_args.check_unstable( - self.no_slice_formula, - "--no-slice-formula", - UnstableFeature::UnstableOptions, - )?; - - self.common_args.check_unstable( - self.synthesize_loop_contracts, - "--synthesize-loop-contracts", - UnstableFeature::UnstableOptions, - )?; + )); + } + if self.concrete_playback.is_some() && self.jobs() != Some(1) { + // Concrete playback currently embeds a lot of assumptions about the order in which harnesses get called. + return Err(Error::raw( + ErrorKind::ArgumentConflict, + "Conflicting options: --concrete-playback isn't compatible with --jobs.", + )); + } + if self.jobs.is_some() && self.output_format != OutputFormat::Terse { + // More verbose output formats make it hard to interpret output right now when run in parallel. + // This can be removed when we change up how results are printed. + return Err(Error::raw( + ErrorKind::ArgumentConflict, + "Conflicting options: --jobs requires `--output-format=terse`", + )); + } + // TODO: error out for other CBMC-backend-specific arguments + if self.common_args.unstable_features.contains(UnstableFeature::Lean) + && !self.cbmc_args.is_empty() + { + return Err(Error::raw( + ErrorKind::ArgumentConflict, + format!( + "Conflicting options: --cbmc-args cannot be used with {}.", + UnstableFeature::Lean.as_argument_string() + ), + )); + } - if self.restrict_vtable { - let z_feature = "-Z restrict-vtable"; - return Err(Error::raw( - ErrorKind::ValueValidation, - format!("The `--restrict-vtable` option is obsolete. Use `{z_feature}` instead.",), - )); - } + Ok(()) + }; - self.common_args.check_unstable( - self.no_restrict_vtable, - "--no-restrict-vtable", - UnstableFeature::RestrictVtable, - )?; + // Check for any deprecated/obsolete options, or providing an unstable flag that has since been stabilized. + let deprecated_stabilized_obsolete = || -> Result<(), Error> { + self.checks.print_deprecated(&self.common_args); + self.check_unnecessary_unstable_option(self.jobs.is_some(), "jobs"); - if !self.c_lib.is_empty() - && !self.common_args.unstable_features.contains(UnstableFeature::CFfi) - { - let z_feature = "-Z c-ffi"; - if self.common_args.enable_unstable { + if self.write_json_symtab { return Err(Error::raw( ErrorKind::ValueValidation, - format!( - "The `--enable-unstable` option is obsolete. Use `{z_feature}` instead.", - ), + "The `--write-json-symtab` option is obsolete.", )); - } else { + } + + if self.restrict_vtable { return Err(Error::raw( - ErrorKind::MissingRequiredArgument, + ErrorKind::ValueValidation, format!( - "The `--c-lib` argument is unstable and requires `{z_feature}` to enable \ - unstable C-FFI support." + "The restrict-vtable option is obsolete. Use `{}` instead.", + UnstableFeature::RestrictVtable.as_argument_string() ), )); } - } - if self.coverage - && !self.common_args.unstable_features.contains(UnstableFeature::SourceCoverage) - { - return Err(Error::raw( - ErrorKind::MissingRequiredArgument, - "The `--coverage` argument is unstable and requires `-Z \ - source-coverage` to be used.", - )); - } + Ok(()) + }; - if self.output_into_files - && !self.common_args.unstable_features.contains(UnstableFeature::UnstableOptions) - { - return Err(Error::raw( - ErrorKind::MissingRequiredArgument, - "The `--output-into-files` argument is unstable and requires `-Z unstable-options` to enable \ - unstable options support.", - )); - } + unstable()?; + conflicting_options()?; + deprecated_stabilized_obsolete()?; - if self.print_llbc && !self.common_args.unstable_features.contains(UnstableFeature::Lean) { - return Err(Error::raw( - ErrorKind::MissingRequiredArgument, - "The `--print-llbc` argument is unstable and requires `-Z lean` to be used.", - )); - } + // Bespoke validations that don't fit into any of the categories above. + if self.randomize_layout.is_some() && self.concrete_playback.is_some() { + let random_seed = if let Some(seed) = self.randomize_layout.unwrap() { + format!(" -Z layout-seed={seed}") + } else { + String::new() + }; - // TODO: error out for other CBMC-backend-specific arguments - if self.common_args.unstable_features.contains(UnstableFeature::Lean) - && !self.cbmc_args.is_empty() - { - return Err(Error::raw( - ErrorKind::ArgumentConflict, - "The `--cbmc-args` argument cannot be used with -Z lean.", - )); + println!( + "Using concrete playback with --randomize-layout.\n\ + The produced tests will have to be played with the same rustc arguments:\n\ + -Z randomize-layout{random_seed}" + ); } - if self.harness_timeout.is_some() - && !self.common_args.unstable_features.contains(UnstableFeature::UnstableOptions) + if let Some(out_dir) = &self.target_dir + && out_dir.exists() + && !out_dir.is_dir() { return Err(Error::raw( - ErrorKind::MissingRequiredArgument, - format!( - "The `--harness-timeout` argument is unstable and requires `-Z {}` to be used.", - UnstableFeature::UnstableOptions - ), - )); - } - - if !self.is_function_contracts_enabled() && self.no_assert_contracts { - return Err(Error::raw( - ErrorKind::MissingRequiredArgument, + ErrorKind::InvalidValue, format!( - "The `--no-assert-contracts` option requires `-Z {}`.", - UnstableFeature::FunctionContracts + "Invalid argument: `--target-dir` argument `{}` is not a directory", + out_dir.display() ), )); } diff --git a/kani_metadata/src/unstable.rs b/kani_metadata/src/unstable.rs index 65fd0c9a0716..ba4ff7a911f6 100644 --- a/kani_metadata/src/unstable.rs +++ b/kani_metadata/src/unstable.rs @@ -38,7 +38,7 @@ //! //! ### Reusing //! -//! You can turn an [`UnstableFeature`] back into it's command line +//! You can turn an [`UnstableFeature`] back into its command line //! representation. This should be done with //! [`EnabledUnstableFeatures::as_arguments`], which returns an iterator that, //! when passed to e.g. [`std::process::Command::args`] will enable those @@ -115,6 +115,20 @@ impl UnstableFeature { pub fn as_argument(&self) -> [&str; 2] { ["-Z", self.as_ref()] } + + /// Serialize this feature into a format ideal for error messages. + pub fn as_argument_string(&self) -> String { + self.as_argument().join(" ") + } + + /// If this unstable feature has been stabilized, return the version it was stabilized in. + /// Use this function to produce warnings that the unstable flag is no longer necessary. + pub fn stabilization_version(&self) -> Option { + match self { + UnstableFeature::List => Some("0.63.0".to_string()), + _ => None, + } + } } /// An opaque collection of unstable features that is enabled on this session. @@ -143,6 +157,10 @@ impl EnabledUnstableFeatures { self.enabled_unstable_features.contains(&feature) } + pub fn iter(&self) -> impl Iterator { + self.enabled_unstable_features.iter() + } + /// Enable an additional unstable feature. /// Note that this enables an unstable feature that the user did not pass on the command line, so this function should be called with caution. /// At time of writing, the only use is to enable -Z function-contracts and -Z loop-contracts when the autoharness subcommand is running. diff --git a/tests/script-based-pre/cargo_autoharness_list/list.sh b/tests/script-based-pre/cargo_autoharness_list/list.sh index bf02eeb0276b..c240c9e72e2e 100755 --- a/tests/script-based-pre/cargo_autoharness_list/list.sh +++ b/tests/script-based-pre/cargo_autoharness_list/list.sh @@ -2,4 +2,4 @@ # Copyright Kani Contributors # SPDX-License-Identifier: Apache-2.0 OR MIT -cargo kani autoharness -Z autoharness --list -Z list +cargo kani autoharness -Z autoharness --list diff --git a/tests/script-based-pre/cargo_list_json/list.sh b/tests/script-based-pre/cargo_list_json/list.sh index a9865f5e6b5d..a90d2c54c4d7 100755 --- a/tests/script-based-pre/cargo_list_json/list.sh +++ b/tests/script-based-pre/cargo_list_json/list.sh @@ -6,7 +6,7 @@ # Note that the list.expected file omits the value for "kani-version" # to avoid having to update the test every time we bump versions. -output=$(kani list -Z list -Z function-contracts src/lib.rs --format json) +output=$(cargo kani list -Z function-contracts --format json) # Check that Kani prints the absolute path to kani-list.json absolute_path="$(cd "$(dirname "kani-list.json")" && pwd -P && cd - > /dev/null)/$(basename "kani-list.json")" diff --git a/tests/script-based-pre/cargo_list_md/list.expected b/tests/script-based-pre/cargo_list_md/list.expected index fcaf72a14d00..73d805eb3964 100644 --- a/tests/script-based-pre/cargo_list_md/list.expected +++ b/tests/script-based-pre/cargo_list_md/list.expected @@ -1,16 +1,15 @@ - Contracts: -| | Crate | Function | Contract Harnesses (#[kani::proof_for_contract]) | -| ----- | ----- | ----------------------------- | -------------------------------------------------------------- | -| | lib | example::implementation::bar | example::verify::check_bar | -| | lib | example::implementation::foo | example::verify::check_foo_u32, example::verify::check_foo_u64 | -| | lib | example::implementation::func | example::verify::check_func | -| | lib | example::prep::parse | NONE | -| Total | | 4 | 4 | +| | Crate | Function | Contract Harnesses (#[kani::proof_for_contract]) | +| ----- | ---------- | ----------------------------- | -------------------------------------------------------------- | +| | cargo_list | example::implementation::bar | example::verify::check_bar | +| | cargo_list | example::implementation::foo | example::verify::check_foo_u32, example::verify::check_foo_u64 | +| | cargo_list | example::implementation::func | example::verify::check_func | +| | cargo_list | example::prep::parse | NONE | +| Total | | 4 | 4 | Standard Harnesses (#[kani::proof]): -| | Crate | Harness | -| ----- | ----- | ------------------------------------------------- | -| | lib | standard_harnesses::example::verify::check_modify | -| | lib | standard_harnesses::example::verify::check_new | -| Total | | 2 | +| | Crate | Harness | +| ----- | ---------- | ------------------------------------------------- | +| | cargo_list | standard_harnesses::example::verify::check_modify | +| | cargo_list | standard_harnesses::example::verify::check_new | +| Total | | 2 | diff --git a/tests/script-based-pre/cargo_list_md/list.sh b/tests/script-based-pre/cargo_list_md/list.sh index e35c4835c42e..56c8709159fc 100755 --- a/tests/script-based-pre/cargo_list_md/list.sh +++ b/tests/script-based-pre/cargo_list_md/list.sh @@ -6,7 +6,7 @@ # Note that the list.expected file omits the value for "kani-version" # to avoid having to update the test every time we bump versions. -output=$(kani list -Z list -Z function-contracts src/lib.rs --format markdown) +output=$(cargo kani list -Z function-contracts --format markdown) # Check that Kani prints the absolute path to kani-list.md absolute_path="$(cd "$(dirname "kani-list.md")" && pwd -P && cd - > /dev/null)/$(basename "kani-list.md")" diff --git a/tests/script-based-pre/kani_list_json/list.sh b/tests/script-based-pre/kani_list_json/list.sh index a70938ffcea9..8b1eb1678948 100755 --- a/tests/script-based-pre/kani_list_json/list.sh +++ b/tests/script-based-pre/kani_list_json/list.sh @@ -6,7 +6,7 @@ # Note that the list.expected file omits the value for "kani-version" # to avoid having to update the test every time we bump versions. -output=$(kani list -Z list -Z function-contracts src/lib.rs --format json) +output=$(kani list -Z function-contracts src/lib.rs --format json) # Check that Kani prints the absolute path to kani-list.json absolute_path="$(cd "$(dirname "kani-list.json")" && pwd -P && cd - > /dev/null)/$(basename "kani-list.json")" diff --git a/tests/script-based-pre/kani_list_md/list.sh b/tests/script-based-pre/kani_list_md/list.sh index e35c4835c42e..fa40394f975c 100755 --- a/tests/script-based-pre/kani_list_md/list.sh +++ b/tests/script-based-pre/kani_list_md/list.sh @@ -6,7 +6,7 @@ # Note that the list.expected file omits the value for "kani-version" # to avoid having to update the test every time we bump versions. -output=$(kani list -Z list -Z function-contracts src/lib.rs --format markdown) +output=$(kani list -Z function-contracts src/lib.rs --format markdown) # Check that Kani prints the absolute path to kani-list.md absolute_path="$(cd "$(dirname "kani-list.md")" && pwd -P && cd - > /dev/null)/$(basename "kani-list.md")" diff --git a/tests/ui/multiple-harnesses/stop_at_single_fail/fail_fast_test_parallel.rs b/tests/ui/multiple-harnesses/stop_at_single_fail/fail_fast_test_parallel.rs index db2535777a26..adeb1122ebdd 100644 --- a/tests/ui/multiple-harnesses/stop_at_single_fail/fail_fast_test_parallel.rs +++ b/tests/ui/multiple-harnesses/stop_at_single_fail/fail_fast_test_parallel.rs @@ -1,6 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --fail-fast -Z unstable-options --jobs 4 --output-format=terse +// kani-flags: --fail-fast --jobs 4 --output-format=terse //! Ensure that the verification process stops as soon as one of the harnesses fails. //! This test runs on 4 parallel threads. Stops verification as soon as a harness on any of the threads fails.