From 1acf62d3f731ab3f8f0c8ef2ecd22ae85c0f6e39 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Fri, 11 Aug 2023 17:22:31 -0700
Subject: [PATCH 1/6] Enable `-Z stubbing` error out instead of ignore stub

Enable `-Z stubbing`, deprecate `--enable-stubbing`, and emit an error
if the user tries to verify a harness that has stubs without explicitly
enabling stubs. This used to be a warning before which was easy to miss.
It was also hard to debug when the harness would take a while to run.
---
 kani-driver/src/args/mod.rs                   | 12 +++-
 kani-driver/src/call_single_file.rs           |  2 +-
 kani-driver/src/harness_runner.rs             | 61 +++++++++----------
 .../expected/function-stubbing-error/expected |  2 +
 .../main.rs                                   |  3 +-
 .../function-stubbing-warning/expected        |  5 --
 tests/kani/Stubbing/enum_method.rs            |  2 +-
 tests/kani/Stubbing/fixme_issue_1953.rs       |  2 +-
 tests/kani/Stubbing/foreign_functions.rs      |  2 +-
 tests/kani/Stubbing/glob_cycle.rs             |  2 +-
 tests/kani/Stubbing/glob_path.rs              |  2 +-
 tests/kani/Stubbing/method_generic_type.rs    |  2 +-
 tests/kani/Stubbing/multiple_harnesses.rs     |  2 +-
 tests/kani/Stubbing/partial_harness_name.rs   |  2 +-
 tests/kani/Stubbing/private_function.rs       |  2 +-
 tests/kani/Stubbing/public_function.rs        |  2 +-
 tests/kani/Stubbing/qualifiers.rs             |  2 +-
 .../Stubbing/resolve_superseded_glob_use.rs   |  2 +-
 tests/kani/Stubbing/resolve_use.rs            |  2 +-
 tests/kani/Stubbing/resolve_use_as.rs         |  2 +-
 tests/kani/Stubbing/resolve_use_glob.rs       |  2 +-
 tests/kani/Stubbing/std_fs_read.rs            |  2 +-
 tests/kani/Stubbing/struct_method.rs          |  2 +-
 tests/kani/Stubbing/stub_harnesses.rs         |  2 +-
 tests/kani/Stubbing/use_std_fs_read.rs        |  2 +-
 .../Stubbing/validate_mismatched_traits.rs    |  2 +-
 tests/ui/stub-attribute/attribute.rs          |  2 +-
 27 files changed, 66 insertions(+), 61 deletions(-)
 create mode 100644 tests/expected/function-stubbing-error/expected
 rename tests/expected/{function-stubbing-warning => function-stubbing-error}/main.rs (68%)
 delete mode 100644 tests/expected/function-stubbing-warning/expected

diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs
index bc927559ecb5..76c5a1184ed5 100644
--- a/kani-driver/src/args/mod.rs
+++ b/kani-driver/src/args/mod.rs
@@ -299,7 +299,7 @@ pub struct VerificationArgs {
         requires("enable_unstable"),
         conflicts_with("concrete_playback")
     )]
-    pub enable_stubbing: bool,
+    enable_stubbing: bool,
 
     /// Enable Kani coverage output alongside verification result
     #[arg(long, hide_short_help = true)]
@@ -345,6 +345,12 @@ impl VerificationArgs {
             Some(Some(x)) => Some(x), // -j=x
         }
     }
+
+    /// Is experimental stubing enabled?
+    pub fn is_stubbing_enabled(&self) -> bool {
+        self.enable_stubbing
+            || self.common_args.unstable_features.contains(&UnstableFeatures::Stubbing)
+    }
 }
 
 #[derive(Copy, Clone, Debug, PartialEq, Eq, ValueEnum)]
@@ -617,6 +623,10 @@ impl ValidateArgs for VerificationArgs {
             }
         }
 
+        if self.enable_stubbing {
+            print_deprecated(&self.common_args, "--enable-stubbing", "-Z stubbing");
+        }
+
         if self.concrete_playback.is_some()
             && !self.common_args.unstable_features.contains(&UnstableFeatures::ConcretePlayback)
         {
diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs
index 1522071fdefd..30cdf88db835 100644
--- a/kani-driver/src/call_single_file.rs
+++ b/kani-driver/src/call_single_file.rs
@@ -92,7 +92,7 @@ impl KaniSession {
             flags.push("--write-json-symtab".into());
         }
 
-        if self.args.enable_stubbing {
+        if self.args.is_stubbing_enabled() {
             flags.push("--enable-stubbing".into());
         }
 
diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs
index fa1aef3d763a..1e7fc7744878 100644
--- a/kani-driver/src/harness_runner.rs
+++ b/kani-driver/src/harness_runner.rs
@@ -4,14 +4,13 @@
 use anyhow::{bail, Result};
 use kani_metadata::{ArtifactType, HarnessMetadata};
 use rayon::prelude::*;
-use std::cmp::Ordering;
 use std::path::Path;
 
 use crate::args::OutputFormat;
 use crate::call_cbmc::{VerificationResult, VerificationStatus};
 use crate::project::Project;
 use crate::session::KaniSession;
-use crate::util::{error, warning};
+use crate::util::error;
 
 /// A HarnessRunner is responsible for checking all proof harnesses. The data in this structure represents
 /// "background information" that the controlling driver (e.g. cargo-kani or kani) computed.
@@ -38,6 +37,8 @@ impl<'sess, 'pr> HarnessRunner<'sess, 'pr> {
         &self,
         harnesses: &'pr [&HarnessMetadata],
     ) -> Result<Vec<HarnessResult<'pr>>> {
+        self.check_stubbing(harnesses)?;
+
         let sorted_harnesses = crate::metadata::sort_harnesses_by_loc(harnesses);
 
         let pool = {
@@ -70,6 +71,33 @@ impl<'sess, 'pr> HarnessRunner<'sess, 'pr> {
 
         Ok(results)
     }
+
+    /// Return an error if the user is trying to verify a harness with stubs without enabling the
+    /// experimental feature.
+    fn check_stubbing(&self, harnesses: &[&HarnessMetadata]) -> Result<()> {
+        if !self.sess.args.is_stubbing_enabled() {
+            let with_stubs: Vec<_> = harnesses
+                .iter()
+                .filter_map(|harness| {
+                    (!harness.attributes.stubs.is_empty()).then_some(harness.pretty_name.as_str())
+                })
+                .collect();
+            match with_stubs.as_slice() {
+                [] => { /* do nothing */ }
+                [harness] => bail!(
+                    "Harness `{}` contains stubs which are unstable.\n\
+                    To enable stubbing, pass options `-Z stubbing`",
+                    harness
+                ),
+                harnesses => bail!(
+                    "Harness `{}` contains stubs which are unstable.\n\
+                    To enable stubbing, pass options `-Z stubbing`",
+                    harnesses.join("`, `")
+                ),
+            }
+        }
+        Ok(())
+    }
 }
 
 impl KaniSession {
@@ -108,33 +136,6 @@ impl KaniSession {
         }
     }
 
-    /// Prints a warning at the end of the verification if harness contained a stub but stubs were
-    /// not enabled.
-    fn stubbing_statuses(&self, results: &[HarnessResult]) {
-        if !self.args.enable_stubbing {
-            let ignored_stubs: Vec<_> = results
-                .iter()
-                .filter_map(|result| {
-                    (!result.harness.attributes.stubs.is_empty())
-                        .then_some(result.harness.pretty_name.as_str())
-                })
-                .collect();
-            match ignored_stubs.len().cmp(&1) {
-                Ordering::Equal => warning(&format!(
-                    "harness `{}` contained stubs which were ignored.\n\
-                    To enable stubbing, pass options `--enable-unstable --enable-stubbing`",
-                    ignored_stubs[0]
-                )),
-                Ordering::Greater => warning(&format!(
-                    "harnesses `{}` contained stubs which were ignored.\n\
-                    To enable stubbing, pass options `--enable-unstable --enable-stubbing`",
-                    ignored_stubs.join("`, `")
-                )),
-                Ordering::Less => {}
-            }
-        }
-    }
-
     /// Concludes a session by printing a summary report and exiting the process with an
     /// error code (if applicable).
     ///
@@ -195,8 +196,6 @@ impl KaniSession {
             }
         }
 
-        self.stubbing_statuses(results);
-
         if failing > 0 {
             // Failure exit code without additional error message
             drop(self);
diff --git a/tests/expected/function-stubbing-error/expected b/tests/expected/function-stubbing-error/expected
new file mode 100644
index 000000000000..5670ab37c1d1
--- /dev/null
+++ b/tests/expected/function-stubbing-error/expected
@@ -0,0 +1,2 @@
+error: Harness `main` contains stubs which are unstable.
+To enable stubbing, pass options `-Z stubbing`
diff --git a/tests/expected/function-stubbing-warning/main.rs b/tests/expected/function-stubbing-error/main.rs
similarity index 68%
rename from tests/expected/function-stubbing-warning/main.rs
rename to tests/expected/function-stubbing-error/main.rs
index 4305f4d398be..4b206bfaee44 100644
--- a/tests/expected/function-stubbing-warning/main.rs
+++ b/tests/expected/function-stubbing-error/main.rs
@@ -3,8 +3,7 @@
 //
 // kani-flags: --harness main
 //
-//! This tests whether we issue a warning if a stub is specified for a harness
-//! but stubbing is not enabled.
+//! This tests whether we abort if a stub is specified for a harness but stubbing is not enabled.
 
 fn foo() -> u32 {
     0
diff --git a/tests/expected/function-stubbing-warning/expected b/tests/expected/function-stubbing-warning/expected
deleted file mode 100644
index 5a5f9f608542..000000000000
--- a/tests/expected/function-stubbing-warning/expected
+++ /dev/null
@@ -1,5 +0,0 @@
-Checking harness main...
-Failed Checks: assertion failed: foo() == 42
-
-warning: harness `main` contained stubs which were ignored.\
-To enable stubbing, pass options `--enable-unstable --enable-stubbing`
diff --git a/tests/kani/Stubbing/enum_method.rs b/tests/kani/Stubbing/enum_method.rs
index a5cf43d214a0..ac1c5351b976 100644
--- a/tests/kani/Stubbing/enum_method.rs
+++ b/tests/kani/Stubbing/enum_method.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-// kani-flags: --harness main --enable-unstable --enable-stubbing
+// kani-flags: --harness main -Z stubbing
 //
 //! This tests stubbing for methods in local enums.
 
diff --git a/tests/kani/Stubbing/fixme_issue_1953.rs b/tests/kani/Stubbing/fixme_issue_1953.rs
index 1f319a0a0e91..55df2d4dc835 100644
--- a/tests/kani/Stubbing/fixme_issue_1953.rs
+++ b/tests/kani/Stubbing/fixme_issue_1953.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-// kani-flags: --enable-unstable --enable-stubbing --harness main
+// kani-flags: -Z stubbing --harness main
 //
 // We currently require a stub and the original/function method to have the same
 // names for generic parameters; instead, we should allow for renaming.
diff --git a/tests/kani/Stubbing/foreign_functions.rs b/tests/kani/Stubbing/foreign_functions.rs
index 8c2ff0812905..07306b1cdf6b 100644
--- a/tests/kani/Stubbing/foreign_functions.rs
+++ b/tests/kani/Stubbing/foreign_functions.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-// kani-flags: --enable-unstable --enable-stubbing
+// kani-flags: -Z stubbing
 //
 //! Check support for stubbing out foreign functions.
 
diff --git a/tests/kani/Stubbing/glob_cycle.rs b/tests/kani/Stubbing/glob_cycle.rs
index 42600809c7bf..54aa066f1622 100644
--- a/tests/kani/Stubbing/glob_cycle.rs
+++ b/tests/kani/Stubbing/glob_cycle.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-// kani-flags: --harness check_stub --enable-unstable --enable-stubbing
+// kani-flags: --harness check_stub -Z stubbing
 //! Test that stub can solve glob cycles.
 
 pub mod mod_a {
diff --git a/tests/kani/Stubbing/glob_path.rs b/tests/kani/Stubbing/glob_path.rs
index 17a9e7ed4264..72ec8a07d980 100644
--- a/tests/kani/Stubbing/glob_path.rs
+++ b/tests/kani/Stubbing/glob_path.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-// kani-flags: --harness check_stub --enable-unstable --enable-stubbing
+// kani-flags: --harness check_stub -Z stubbing
 //! Test that stub can solve glob cycles even when the path expands the cycle.
 
 pub mod mod_a {
diff --git a/tests/kani/Stubbing/method_generic_type.rs b/tests/kani/Stubbing/method_generic_type.rs
index 55bad2c72715..804c2c5c7f5e 100644
--- a/tests/kani/Stubbing/method_generic_type.rs
+++ b/tests/kani/Stubbing/method_generic_type.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-// kani-flags: --harness main --enable-unstable --enable-stubbing
+// kani-flags: --harness main -Z stubbing
 //
 //! This tests stubbing for methods of a local type that has generic parameters.
 
diff --git a/tests/kani/Stubbing/multiple_harnesses.rs b/tests/kani/Stubbing/multiple_harnesses.rs
index 59d4199b601f..ac20b53e515e 100644
--- a/tests/kani/Stubbing/multiple_harnesses.rs
+++ b/tests/kani/Stubbing/multiple_harnesses.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-// kani-flags: --enable-unstable --enable-stubbing
+// kani-flags: -Z stubbing
 //! Check that Kani can handle a different combination of stubs in
 //! the same crate.
 
diff --git a/tests/kani/Stubbing/partial_harness_name.rs b/tests/kani/Stubbing/partial_harness_name.rs
index c08de8c226d9..eae475154d1d 100644
--- a/tests/kani/Stubbing/partial_harness_name.rs
+++ b/tests/kani/Stubbing/partial_harness_name.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-// kani-flags: --harness mod2::harness --enable-unstable --enable-stubbing
+// kani-flags: --harness mod2::harness -Z stubbing
 //
 //! This tests whether we correctly find harnesses during stubbing that are
 //! specified with a partially qualified name.
diff --git a/tests/kani/Stubbing/private_function.rs b/tests/kani/Stubbing/private_function.rs
index d112731444c7..818c94c51623 100644
--- a/tests/kani/Stubbing/private_function.rs
+++ b/tests/kani/Stubbing/private_function.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-// kani-flags: --harness main --enable-unstable --enable-stubbing
+// kani-flags: --harness main -Z stubbing
 //
 //! This tests stubbing for private local functions.
 
diff --git a/tests/kani/Stubbing/public_function.rs b/tests/kani/Stubbing/public_function.rs
index 85a25e7d48e8..8257081241b5 100644
--- a/tests/kani/Stubbing/public_function.rs
+++ b/tests/kani/Stubbing/public_function.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-// kani-flags: --harness main --enable-unstable --enable-stubbing
+// kani-flags: --harness main -Z stubbing
 //
 //! This tests stubbing for public local functions.
 
diff --git a/tests/kani/Stubbing/qualifiers.rs b/tests/kani/Stubbing/qualifiers.rs
index b9b4aac560a0..06cee979883b 100644
--- a/tests/kani/Stubbing/qualifiers.rs
+++ b/tests/kani/Stubbing/qualifiers.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-// kani-flags: --harness harness --enable-unstable --enable-stubbing
+// kani-flags: --harness harness -Z stubbing
 //
 //! This tests resolving stubs with the path qualifiers `self`, `super`, and
 //! `crate`.
diff --git a/tests/kani/Stubbing/resolve_superseded_glob_use.rs b/tests/kani/Stubbing/resolve_superseded_glob_use.rs
index 83f1b3527a0c..e639437133f4 100644
--- a/tests/kani/Stubbing/resolve_superseded_glob_use.rs
+++ b/tests/kani/Stubbing/resolve_superseded_glob_use.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-// kani-flags: --harness harness --enable-unstable --enable-stubbing
+// kani-flags: --harness harness -Z stubbing
 //
 //! Tests to make sure that, when we are resolving paths in `kani::stub`
 //! attributes, we prioritize those that do not come from glob imports.
diff --git a/tests/kani/Stubbing/resolve_use.rs b/tests/kani/Stubbing/resolve_use.rs
index 9bd25bc90bb5..ac1f6f7325f8 100644
--- a/tests/kani/Stubbing/resolve_use.rs
+++ b/tests/kani/Stubbing/resolve_use.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-// kani-flags: --harness my_mod::harness --enable-unstable --enable-stubbing
+// kani-flags: --harness my_mod::harness -Z stubbing
 //
 //! This tests whether we take into account simple local uses (`use XXX;`) when
 //! resolving paths in `kani::stub` attributes.
diff --git a/tests/kani/Stubbing/resolve_use_as.rs b/tests/kani/Stubbing/resolve_use_as.rs
index b661636fae7e..790e26e575e9 100644
--- a/tests/kani/Stubbing/resolve_use_as.rs
+++ b/tests/kani/Stubbing/resolve_use_as.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-// kani-flags: --harness my_mod::harness --enable-unstable --enable-stubbing
+// kani-flags: --harness my_mod::harness -Z stubbing
 //
 //! This tests whether we take into account simple local use-as statements (`use
 //! XXX as YYY;`) when resolving paths in `kani::stub` attributes.
diff --git a/tests/kani/Stubbing/resolve_use_glob.rs b/tests/kani/Stubbing/resolve_use_glob.rs
index f9092e9f1a55..a5e85ce7e10c 100644
--- a/tests/kani/Stubbing/resolve_use_glob.rs
+++ b/tests/kani/Stubbing/resolve_use_glob.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-// kani-flags: --harness my_mod::harness --enable-unstable --enable-stubbing
+// kani-flags: --harness my_mod::harness -Z stubbing
 //
 //! This tests whether we take into account local use-glob statements (`use
 //! XXX::*;`) when resolving paths in `kani::stub` attributes.
diff --git a/tests/kani/Stubbing/std_fs_read.rs b/tests/kani/Stubbing/std_fs_read.rs
index 397487a3a5b4..fa9d55c06813 100644
--- a/tests/kani/Stubbing/std_fs_read.rs
+++ b/tests/kani/Stubbing/std_fs_read.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-// kani-flags: --harness harness --enable-unstable --enable-stubbing
+// kani-flags: --harness harness -Z stubbing
 //
 //! This tests stubbing `std` functions like `std::fs::read`.
 
diff --git a/tests/kani/Stubbing/struct_method.rs b/tests/kani/Stubbing/struct_method.rs
index b939bf7b417a..0270941ef705 100644
--- a/tests/kani/Stubbing/struct_method.rs
+++ b/tests/kani/Stubbing/struct_method.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-// kani-flags: --harness main --enable-unstable --enable-stubbing
+// kani-flags: --harness main -Z stubbing
 //
 //! This tests stubbing for methods in local structs.
 
diff --git a/tests/kani/Stubbing/stub_harnesses.rs b/tests/kani/Stubbing/stub_harnesses.rs
index f83dc309277e..b7969f74d03d 100644
--- a/tests/kani/Stubbing/stub_harnesses.rs
+++ b/tests/kani/Stubbing/stub_harnesses.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-// kani-flags: --harness check --enable-unstable --enable-stubbing
+// kani-flags: --harness check -Z stubbing
 //
 //! This tests whether we provide a user friendly error if more than one harness has stubs
 
diff --git a/tests/kani/Stubbing/use_std_fs_read.rs b/tests/kani/Stubbing/use_std_fs_read.rs
index e174e49e93a9..8beee26bbbf3 100644
--- a/tests/kani/Stubbing/use_std_fs_read.rs
+++ b/tests/kani/Stubbing/use_std_fs_read.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-// kani-flags: --harness harness --enable-unstable --enable-stubbing
+// kani-flags: --harness harness -Z stubbing
 //
 //! This tests whether we can correctly account for `use` statements with `std`
 //! functions like `std::fs::read` when resolving paths in `kani::stub`
diff --git a/tests/kani/Stubbing/validate_mismatched_traits.rs b/tests/kani/Stubbing/validate_mismatched_traits.rs
index 32d49593bc18..f575e2bb6fa3 100644
--- a/tests/kani/Stubbing/validate_mismatched_traits.rs
+++ b/tests/kani/Stubbing/validate_mismatched_traits.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-// kani-flags: --harness harness --enable-unstable --enable-stubbing
+// kani-flags: --harness harness -Z stubbing
 //
 //! This tests that we allow trait mismatches between the stub and the original
 //! function/method so long as they do not lead to a trait method call being
diff --git a/tests/ui/stub-attribute/attribute.rs b/tests/ui/stub-attribute/attribute.rs
index 2e3b81fb09ea..749c8fc4e2ce 100644
--- a/tests/ui/stub-attribute/attribute.rs
+++ b/tests/ui/stub-attribute/attribute.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-//
+// kani-flags: -Z enable-stubbing
 //! Checks that the `kani::stub` attribute is accepted
 
 fn foo() {}

From 79e056e7406a740151b0d6e2b21f709b4f9158a6 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Fri, 11 Aug 2023 18:48:06 -0700
Subject: [PATCH 2/6] Update attribute.rs

---
 tests/ui/stub-attribute/attribute.rs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/ui/stub-attribute/attribute.rs b/tests/ui/stub-attribute/attribute.rs
index 749c8fc4e2ce..19fdf5b5b05b 100644
--- a/tests/ui/stub-attribute/attribute.rs
+++ b/tests/ui/stub-attribute/attribute.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Z enable-stubbing
+// kani-flags: -Z stubbing
 //! Checks that the `kani::stub` attribute is accepted
 
 fn foo() {}

From 490321ed15cc6717acb22f68e3ad868675e10e67 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Mon, 14 Aug 2023 13:43:07 -0700
Subject: [PATCH 3/6] Use unstable table to enable stubbing

Replace the deprecated `enable-unstable` table.
---
 tests/cargo-kani/stubbing-do-not-resolve/Cargo.toml          | 4 ++--
 .../stubbing-double-extern-path/harness/Cargo.toml           | 5 +++--
 tests/cargo-kani/stubbing-extern-path/Cargo.toml             | 4 ++--
 tests/cargo-kani/stubbing-foreign-method/Cargo.toml          | 4 ++--
 .../cargo-kani/stubbing-private-foreign-function/Cargo.toml  | 4 ++--
 tests/cargo-kani/stubbing-public-foreign-function/Cargo.toml | 4 ++--
 tests/cargo-kani/stubbing-resolve-extern-crate-as/Cargo.toml | 4 ++--
 tests/cargo-kani/stubbing-use-as-foreign/Cargo.toml          | 4 ++--
 tests/cargo-kani/stubbing-use-foreign/Cargo.toml             | 4 ++--
 tests/cargo-kani/stubbing-use-glob-foreign/Cargo.toml        | 4 ++--
 tests/cargo-kani/stubbing-use-in-foreign/Cargo.toml          | 4 ++--
 tests/cargo-kani/stubbing-validate-random/Cargo.toml         | 4 ++--
 tests/cargo-kani/stubbing-ws-packages/Cargo.toml             | 5 ++---
 tests/cargo-ui/function-stubbing-trait-mismatch/Cargo.toml   | 4 ++--
 tests/cargo-ui/stubbing-flag/Cargo.toml                      | 3 ++-
 15 files changed, 31 insertions(+), 30 deletions(-)

diff --git a/tests/cargo-kani/stubbing-do-not-resolve/Cargo.toml b/tests/cargo-kani/stubbing-do-not-resolve/Cargo.toml
index 85da4b7dc7e8..2b0e6273f0ae 100644
--- a/tests/cargo-kani/stubbing-do-not-resolve/Cargo.toml
+++ b/tests/cargo-kani/stubbing-do-not-resolve/Cargo.toml
@@ -11,5 +11,5 @@ edition = "2021"
 other_crate1 = { path = "other_crate1" }
 other_crate2 = { path = "other_crate2" }
 
-[package.metadata.kani]
-flags = { enable-unstable=true, enable-stubbing=true }
\ No newline at end of file
+[package.metadata.kani.unstable]
+stubbing = true
diff --git a/tests/cargo-kani/stubbing-double-extern-path/harness/Cargo.toml b/tests/cargo-kani/stubbing-double-extern-path/harness/Cargo.toml
index 4d26da916be8..cb4aedadd582 100644
--- a/tests/cargo-kani/stubbing-double-extern-path/harness/Cargo.toml
+++ b/tests/cargo-kani/stubbing-double-extern-path/harness/Cargo.toml
@@ -11,6 +11,7 @@ description = "Should test invoking double extern but found cycle issue"
 crate_b = { path = "../crate_b" }
 
 [package.metadata.kani.flags]
-enable-unstable = true
-enable-stubbing = true
 harness = ["check_inverted"]
+
+[package.metadata.kani.unstable]
+stubbing = true
diff --git a/tests/cargo-kani/stubbing-extern-path/Cargo.toml b/tests/cargo-kani/stubbing-extern-path/Cargo.toml
index 58ee1c579e5f..5b9e08f1d8c0 100644
--- a/tests/cargo-kani/stubbing-extern-path/Cargo.toml
+++ b/tests/cargo-kani/stubbing-extern-path/Cargo.toml
@@ -8,5 +8,5 @@ edition = "2021"
 [dependencies]
 other_crate = { path = "other_crate" }
 
-[package.metadata.kani]
-flags = { enable-unstable=true, enable-stubbing=true }
+[package.metadata.kani.unstable]
+stubbing = true
diff --git a/tests/cargo-kani/stubbing-foreign-method/Cargo.toml b/tests/cargo-kani/stubbing-foreign-method/Cargo.toml
index 3faa6d269800..54d2e3636d8e 100644
--- a/tests/cargo-kani/stubbing-foreign-method/Cargo.toml
+++ b/tests/cargo-kani/stubbing-foreign-method/Cargo.toml
@@ -8,5 +8,5 @@ edition = "2021"
 [dependencies]
 other_crate = { path = "other_crate" }
 
-[package.metadata.kani]
-flags = { enable-unstable=true, enable-stubbing=true }
\ No newline at end of file
+[package.metadata.kani.unstable]
+stubbing = true
diff --git a/tests/cargo-kani/stubbing-private-foreign-function/Cargo.toml b/tests/cargo-kani/stubbing-private-foreign-function/Cargo.toml
index 3faa6d269800..54d2e3636d8e 100644
--- a/tests/cargo-kani/stubbing-private-foreign-function/Cargo.toml
+++ b/tests/cargo-kani/stubbing-private-foreign-function/Cargo.toml
@@ -8,5 +8,5 @@ edition = "2021"
 [dependencies]
 other_crate = { path = "other_crate" }
 
-[package.metadata.kani]
-flags = { enable-unstable=true, enable-stubbing=true }
\ No newline at end of file
+[package.metadata.kani.unstable]
+stubbing = true
diff --git a/tests/cargo-kani/stubbing-public-foreign-function/Cargo.toml b/tests/cargo-kani/stubbing-public-foreign-function/Cargo.toml
index 3faa6d269800..54d2e3636d8e 100644
--- a/tests/cargo-kani/stubbing-public-foreign-function/Cargo.toml
+++ b/tests/cargo-kani/stubbing-public-foreign-function/Cargo.toml
@@ -8,5 +8,5 @@ edition = "2021"
 [dependencies]
 other_crate = { path = "other_crate" }
 
-[package.metadata.kani]
-flags = { enable-unstable=true, enable-stubbing=true }
\ No newline at end of file
+[package.metadata.kani.unstable]
+stubbing = true
diff --git a/tests/cargo-kani/stubbing-resolve-extern-crate-as/Cargo.toml b/tests/cargo-kani/stubbing-resolve-extern-crate-as/Cargo.toml
index 9a6a8e7cc903..b8fc26c97066 100644
--- a/tests/cargo-kani/stubbing-resolve-extern-crate-as/Cargo.toml
+++ b/tests/cargo-kani/stubbing-resolve-extern-crate-as/Cargo.toml
@@ -10,5 +10,5 @@ edition = "2021"
 [dependencies]
 other_crate = { path = "other_crate" }
 
-[package.metadata.kani]
-flags = { enable-unstable=true, enable-stubbing=true }
\ No newline at end of file
+[package.metadata.kani.unstable]
+stubbing = true
diff --git a/tests/cargo-kani/stubbing-use-as-foreign/Cargo.toml b/tests/cargo-kani/stubbing-use-as-foreign/Cargo.toml
index 6fb8f5632fac..d02d62cce077 100644
--- a/tests/cargo-kani/stubbing-use-as-foreign/Cargo.toml
+++ b/tests/cargo-kani/stubbing-use-as-foreign/Cargo.toml
@@ -8,5 +8,5 @@ edition = "2021"
 [dependencies]
 other_crate = { path = "other_crate" }
 
-[package.metadata.kani]
-flags = { enable-unstable=true, enable-stubbing=true }
\ No newline at end of file
+[package.metadata.kani.unstable]
+stubbing = true
diff --git a/tests/cargo-kani/stubbing-use-foreign/Cargo.toml b/tests/cargo-kani/stubbing-use-foreign/Cargo.toml
index 6c930116aeab..8eafd54bf89f 100644
--- a/tests/cargo-kani/stubbing-use-foreign/Cargo.toml
+++ b/tests/cargo-kani/stubbing-use-foreign/Cargo.toml
@@ -8,5 +8,5 @@ edition = "2021"
 [dependencies]
 other_crate = { path = "other_crate" }
 
-[package.metadata.kani]
-flags = { enable-unstable=true, enable-stubbing=true }
\ No newline at end of file
+[package.metadata.kani.unstable]
+stubbing = true
diff --git a/tests/cargo-kani/stubbing-use-glob-foreign/Cargo.toml b/tests/cargo-kani/stubbing-use-glob-foreign/Cargo.toml
index f6ea8cc1b0a4..cd59013a726e 100644
--- a/tests/cargo-kani/stubbing-use-glob-foreign/Cargo.toml
+++ b/tests/cargo-kani/stubbing-use-glob-foreign/Cargo.toml
@@ -8,5 +8,5 @@ edition = "2021"
 [dependencies]
 other_crate = { path = "other_crate" }
 
-[package.metadata.kani]
-flags = { enable-unstable=true, enable-stubbing=true }
\ No newline at end of file
+[package.metadata.kani.unstable]
+stubbing = true
diff --git a/tests/cargo-kani/stubbing-use-in-foreign/Cargo.toml b/tests/cargo-kani/stubbing-use-in-foreign/Cargo.toml
index 4dcda9d3aa5d..ec2f3797ee4d 100644
--- a/tests/cargo-kani/stubbing-use-in-foreign/Cargo.toml
+++ b/tests/cargo-kani/stubbing-use-in-foreign/Cargo.toml
@@ -8,5 +8,5 @@ edition = "2021"
 [dependencies]
 other_crate = { path = "other_crate" }
 
-[package.metadata.kani]
-flags = { enable-unstable=true, enable-stubbing=true }
\ No newline at end of file
+[package.metadata.kani.unstable]
+stubbing = true
diff --git a/tests/cargo-kani/stubbing-validate-random/Cargo.toml b/tests/cargo-kani/stubbing-validate-random/Cargo.toml
index 099cc3d4d5b9..ef03456dd1aa 100644
--- a/tests/cargo-kani/stubbing-validate-random/Cargo.toml
+++ b/tests/cargo-kani/stubbing-validate-random/Cargo.toml
@@ -8,5 +8,5 @@ edition = "2021"
 [dependencies]
 rand = "0.8.5"
 
-[package.metadata.kani]
-flags = { enable-unstable=true, enable-stubbing=true }
+[package.metadata.kani.unstable]
+stubbing = true
diff --git a/tests/cargo-kani/stubbing-ws-packages/Cargo.toml b/tests/cargo-kani/stubbing-ws-packages/Cargo.toml
index 2ff3f16833d4..a2169dbc134e 100644
--- a/tests/cargo-kani/stubbing-ws-packages/Cargo.toml
+++ b/tests/cargo-kani/stubbing-ws-packages/Cargo.toml
@@ -5,6 +5,5 @@
 [workspace]
 members = ["dependency", "top"]
 
-[workspace.metadata.kani.flags]
-enable-unstable=true
-enable-stubbing=true
+[workspace.metadata.kani.unstable]
+stubbing=true
diff --git a/tests/cargo-ui/function-stubbing-trait-mismatch/Cargo.toml b/tests/cargo-ui/function-stubbing-trait-mismatch/Cargo.toml
index 7562cf1eb7a3..8e8095e249e7 100644
--- a/tests/cargo-ui/function-stubbing-trait-mismatch/Cargo.toml
+++ b/tests/cargo-ui/function-stubbing-trait-mismatch/Cargo.toml
@@ -7,5 +7,5 @@ edition = "2021"
 
 [dependencies]
 
-[package.metadata.kani]
-flags = { enable-unstable=true, enable-stubbing=true }
\ No newline at end of file
+[package.metadata.kani.unstable]
+stubbing = true
diff --git a/tests/cargo-ui/stubbing-flag/Cargo.toml b/tests/cargo-ui/stubbing-flag/Cargo.toml
index f94fba420728..66541c9f3ba5 100644
--- a/tests/cargo-ui/stubbing-flag/Cargo.toml
+++ b/tests/cargo-ui/stubbing-flag/Cargo.toml
@@ -8,4 +8,5 @@ edition = "2021"
 [dependencies]
 
 [package.metadata.kani]
-flags = { enable-unstable=true, enable-stubbing=true, harness="main" }
+flags = { harness="main" }
+unstable = { stubbing=true }

From 82c41587c548e9e2d0c42351fc356d9ab9143137 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Thu, 17 Aug 2023 12:20:46 -0700
Subject: [PATCH 4/6] Improve error message

---
 kani-driver/src/harness_runner.rs               | 4 ++--
 tests/expected/function-stubbing-error/expected | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs
index 1e7fc7744878..e842e0e16cc5 100644
--- a/kani-driver/src/harness_runner.rs
+++ b/kani-driver/src/harness_runner.rs
@@ -85,12 +85,12 @@ impl<'sess, 'pr> HarnessRunner<'sess, 'pr> {
             match with_stubs.as_slice() {
                 [] => { /* do nothing */ }
                 [harness] => bail!(
-                    "Harness `{}` contains stubs which are unstable.\n\
+                    "Use of unstable feature 'stubbing' in harness `{}`.\n\
                     To enable stubbing, pass options `-Z stubbing`",
                     harness
                 ),
                 harnesses => bail!(
-                    "Harness `{}` contains stubs which are unstable.\n\
+                    "Use of unstable feature 'stubbing' in harnesses `{}`.\n\
                     To enable stubbing, pass options `-Z stubbing`",
                     harnesses.join("`, `")
                 ),
diff --git a/tests/expected/function-stubbing-error/expected b/tests/expected/function-stubbing-error/expected
index 5670ab37c1d1..fa53e06c1fad 100644
--- a/tests/expected/function-stubbing-error/expected
+++ b/tests/expected/function-stubbing-error/expected
@@ -1,2 +1,2 @@
-error: Harness `main` contains stubs which are unstable.
+error: Use of unstable feature 'stubbing' in harness `main`.
 To enable stubbing, pass options `-Z stubbing`

From fe7ada6f59965c3fcef9fa2c001a1bed7c58ad65 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Mon, 21 Aug 2023 12:20:57 -0700
Subject: [PATCH 5/6] Apply suggestions from code review

Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>
---
 kani-driver/src/args/mod.rs                     | 2 +-
 kani-driver/src/harness_runner.rs               | 4 ++--
 tests/expected/function-stubbing-error/expected | 2 +-
 3 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs
index 76c5a1184ed5..8be6bceab921 100644
--- a/kani-driver/src/args/mod.rs
+++ b/kani-driver/src/args/mod.rs
@@ -346,7 +346,7 @@ impl VerificationArgs {
         }
     }
 
-    /// Is experimental stubing enabled?
+    /// Is experimental stubbing enabled?
     pub fn is_stubbing_enabled(&self) -> bool {
         self.enable_stubbing
             || self.common_args.unstable_features.contains(&UnstableFeatures::Stubbing)
diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs
index e842e0e16cc5..2cd8bb7cbd70 100644
--- a/kani-driver/src/harness_runner.rs
+++ b/kani-driver/src/harness_runner.rs
@@ -86,12 +86,12 @@ impl<'sess, 'pr> HarnessRunner<'sess, 'pr> {
                 [] => { /* do nothing */ }
                 [harness] => bail!(
                     "Use of unstable feature 'stubbing' in harness `{}`.\n\
-                    To enable stubbing, pass options `-Z stubbing`",
+                    To enable stubbing, pass option `-Z stubbing`",
                     harness
                 ),
                 harnesses => bail!(
                     "Use of unstable feature 'stubbing' in harnesses `{}`.\n\
-                    To enable stubbing, pass options `-Z stubbing`",
+                    To enable stubbing, pass option `-Z stubbing`",
                     harnesses.join("`, `")
                 ),
             }
diff --git a/tests/expected/function-stubbing-error/expected b/tests/expected/function-stubbing-error/expected
index fa53e06c1fad..6adf1ad27631 100644
--- a/tests/expected/function-stubbing-error/expected
+++ b/tests/expected/function-stubbing-error/expected
@@ -1,2 +1,2 @@
 error: Use of unstable feature 'stubbing' in harness `main`.
-To enable stubbing, pass options `-Z stubbing`
+To enable stubbing, pass option `-Z stubbing`

From fc3641484af82734e60ce43560f7de870026bd80 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Wed, 30 Aug 2023 16:02:36 -0700
Subject: [PATCH 6/6] Add tests for deprecated option

---
 .../deprecated-enable-stable/deprecated.rs       | 16 ++++++++++++++++
 .../stubbing/deprecated-enable-stable/expected   |  2 ++
 2 files changed, 18 insertions(+)
 create mode 100644 tests/ui/stubbing/deprecated-enable-stable/deprecated.rs
 create mode 100644 tests/ui/stubbing/deprecated-enable-stable/expected

diff --git a/tests/ui/stubbing/deprecated-enable-stable/deprecated.rs b/tests/ui/stubbing/deprecated-enable-stable/deprecated.rs
new file mode 100644
index 000000000000..a5686af20a35
--- /dev/null
+++ b/tests/ui/stubbing/deprecated-enable-stable/deprecated.rs
@@ -0,0 +1,16 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: --enable-unstable --enable-stubbing
+//! Checks that the `kani::stub` attribute is accepted
+
+fn foo() {
+    unreachable!();
+}
+
+fn bar() {}
+
+#[kani::proof]
+#[kani::stub(foo, bar)]
+fn main() {
+    foo();
+}
diff --git a/tests/ui/stubbing/deprecated-enable-stable/expected b/tests/ui/stubbing/deprecated-enable-stable/expected
new file mode 100644
index 000000000000..eb05b8cf9812
--- /dev/null
+++ b/tests/ui/stubbing/deprecated-enable-stable/expected
@@ -0,0 +1,2 @@
+warning: The `--enable-stubbing` option is deprecated. This option will be removed soon. Consider using `-Z stubbing` instead
+VERIFICATION:- SUCCESSFUL