diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 52f621c2f027..ea957f7d6ec7 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -416,12 +416,26 @@ impl VerificationArgs { } } - /// Given an argument, warn if UnstableFeature::UnstableOptions is enabled. + /// Given the string representation of an option, warn if it's enabled while + /// UnstableFeature::UnstableOptions is also enabled. /// This is for cases where the option was previously unstable but has since been stabilized. + /// Example invocation: self.check_unnecessary_unstable_option(self.jobs.is_some(), "jobs"); + #[allow(dead_code)] pub fn check_unnecessary_unstable_option(&self, enabled: bool, option: &str) { + // Note that the body of this function is subject to change; an option + // will only be here if it has been stabilized *recently*, such that we should still warn about unstable-options. + // So a body of just `None` is fine, since that just means that no unstable options are currently in that in-between period. + // Example of an appropriate body: + // ```rust + // match option { + // "jobs" => Some("0.63.0".to_string()), + // _ => None, + // } + // ``` + // for the unstable jobs option, which was stabilized in version 0.63. + #[allow(clippy::match_single_binding)] fn stabilization_version(option: &str) -> Option { match option { - "jobs" => Some("0.63.0".to_string()), _ => None, } } @@ -473,39 +487,22 @@ pub enum OutputFormat { #[derive(Debug, clap::Args)] #[clap(next_help_heading = "Memory Checks")] 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, 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, 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, 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, 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, hide = true)] - pub unwinding_checks: bool, /// Turn off default unwinding checks #[arg(long)] pub no_unwinding_checks: bool, @@ -513,41 +510,16 @@ pub struct CheckArgs { impl CheckArgs { pub fn memory_safety_on(&self) -> bool { - !self.no_default_checks && !self.no_memory_safety_checks || self.memory_safety_checks + !self.no_default_checks && !self.no_memory_safety_checks } pub fn overflow_on(&self) -> bool { - !self.no_default_checks && !self.no_overflow_checks || self.overflow_checks + !self.no_default_checks && !self.no_overflow_checks } pub fn undefined_function_on(&self) -> bool { !self.no_default_checks && !self.no_undefined_function_checks - || self.undefined_function_checks } 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); - } + !self.no_default_checks && !self.no_unwinding_checks } } @@ -807,9 +779,6 @@ impl ValidateArgs for VerificationArgs { // 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.write_json_symtab { return Err(Error::raw( ErrorKind::ValueValidation, diff --git a/kani_metadata/src/unstable.rs b/kani_metadata/src/unstable.rs index a332b9973bb8..9a639d3bc58c 100644 --- a/kani_metadata/src/unstable.rs +++ b/kani_metadata/src/unstable.rs @@ -85,8 +85,6 @@ pub enum UnstableFeature { GhostState, /// Enabled Lean backend (Aeneas/LLBC) Lean, - /// The list subcommand [RFC 13](https://model-checking.github.io/kani/rfc/rfcs/0013-list.html) - List, /// Enable loop contracts [RFC 12](https://model-checking.github.io/kani/rfc/rfcs/0012-loop-contracts.html) LoopContracts, /// Memory predicate APIs. @@ -125,9 +123,19 @@ impl UnstableFeature { /// 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. + /// Note that the body of this function is subject to change; a feature will only be here if it has been deprecated, but not yet removed. + /// So a body of just `None` is fine, since that just means that no unstable features are currently in that in-between period. + /// Example of an appropriate body: + /// ```ignore + /// match self { + /// UnstableFeature::List => Some("0.63.0".to_string()), + /// _ => None, + /// } + /// ``` + /// for the unstable list feature, which was stabilized in version 0.63 and removed permanently in v0.66. + #[allow(clippy::match_single_binding)] pub fn stabilization_version(&self) -> Option { match self { - UnstableFeature::List => Some("0.63.0".to_string()), _ => None, } }