[Breaking Changes] Remove unstable list feature and default memory checks

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<String> {
             match option {
-                "jobs" => Some("0.63.0".to_string()),
                 _ => None,
             }
         }
@@ -473,81 +487,39 @@ 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,
 }
 
 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,

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<String> {
         match self {
-            UnstableFeature::List => Some("0.63.0".to_string()),
             _ => None,
         }
     }